[isabelle] Macro to comment and uncomment selected text so I don't get error?



Hi,

This email is about me trying to find a macro to comment out text and uncomment text, so I don't get the error where I have to reload the file. It's also a request for someone to write a new macro or modify "Add_Prefix_and_Suffix.bsh" to uncomment selected text that's commented out.

First, I thought if "(*" and "*)" are inserted fast enough, then I won't get the error, but speed of insertion is not the issue.

As a test case, I'm using:

theory test imports Complex_Main begin
value "string"
value "string"
end

I highlight lines 2 and 3, and I use the jEdit menu command "Edit / Source / Range Comment". It comments out the two lines, and I'm left with an error. I save the file, and it goes away.

If I only highlight one line and use the command, then I don't get the error.

I've modified "Isabelle2012\src\Tools\jEdit\dist\macros\Text\Add_Prefix_and_Suffix.bsh" and attached the modified macro. The difference is that my modified macro only adds the prefix to the first line and the suffix to the last line. The original macro comments out each line individually.

I can comment out lines 2 and 3 with the macro, and I get no error.

The idea is, in the future, to be able to experiment with commenting out and uncommenting text with a macro to try and figure out if there's a workaround that always works, and to see if the problem is text getting parsed that has unmatched delimiters.

My attached macro will comment out selected text. I can modify the attached macro to automatically use one of 4 different ways to comment out text, which are (*...*), --"...", --{*...*}, and text{*...*}.

If someone wants to modify the attached macro to uncomment highlighted text that's enclosed in comment delimiters, that would be useful. The macro code I modified is below the original code, which I marked "ORIGINAL START".

In general, I have some macros that insert matched delimiters to try and prevent parsing of unmatched delimiters, such as the attached "comment (star-star).bsh".

Regards,
GB




/*
 * Add_Prefix_and_Suffix.bsh - a BeanShell macro script for the
 * jEdit text editor - obtains and processes input for prefix and
 * suffix text to be inserted in selected lines in the current
 * editing buffer
 * Copyright (C) 2001 John Gellene
 * jgellene at nyc.rr.com
 * http://community.jedit.org
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
 *
 * $Id: Add_Prefix_and_Suffix.bsh 9126 2007-03-10 19:14:30Z Vampire0 $
 *
 * Notes on use:
 *
 * If no text is selected, the macro will operate on the current line.
 *
 * The caret position is part of the selected text; if the caret is at
 * the beginning of a line, the macro will operate on that line.
 *
 * The use of HistoryTextField objects allows the macro to 'remember'
 * past entries for the prefix and suffix.
 */

// beginning of Add_Prefix_and_Suffix.bsh

// import statements
import javax.swing.border.*;

// main routine
void prefixSuffixDialog(View view)
{
	this.view = view;

    // create dialog object and set its features
    title = "Add prefix and suffix to selected lines";
    dialog = new JDialog(view, title, false);
    content = new JPanel(new BorderLayout());
    content.setBorder(new EmptyBorder(12, 12, 12, 12));
    dialog.setContentPane(content);

    // add to the dialog a panel containing the text fields for
    // entry of the prefix and suffix text
    fieldPanel = new JPanel(new GridLayout(4, 1, 0, 6));
    prefixField = new HistoryTextField("macro.add-prefix");
    prefixLabel = new JLabel("Prefix to add:");
    suffixField = new HistoryTextField("macro.add-suffix");
    suffixLabel = new JLabel("Suffix to add:");
    fieldPanel.add(prefixLabel);
    fieldPanel.add(prefixField);
    fieldPanel.add(suffixLabel);
    fieldPanel.add(suffixField);
    content.add(fieldPanel, "Center");

    // add a panel containing the buttons
    buttonPanel = new JPanel();
    buttonPanel.setLayout(new BoxLayout(buttonPanel,
        BoxLayout.X_AXIS));
    buttonPanel.setBorder(new EmptyBorder(12, 50, 0, 50));
    buttonPanel.add(Box.createGlue());
    ok = new JButton("OK");
    cancel = new JButton("Cancel");
    ok.setPreferredSize(cancel.getPreferredSize());
    dialog.getRootPane().setDefaultButton(ok);
    buttonPanel.add(ok);
    buttonPanel.add(Box.createHorizontalStrut(6));
    buttonPanel.add(cancel);
    buttonPanel.add(Box.createGlue());
    content.add(buttonPanel, "South");

    // register this method as an ActionListener for
    // the buttons and text fields
    ok.addActionListener(this);
    cancel.addActionListener(this);
    prefixField.addActionListener(this);
    suffixField.addActionListener(this);

    // locate the dialog in the center of the
    // editing pane and make it visible
    dialog.pack();
    dialog.setLocationRelativeTo(view);
    dialog.setDefaultCloseOperation(JDialog.DISPOSE_ON_CLOSE);
    dialog.setVisible(true);

    // this method will be called when a button is clicked
    // or when ENTER is pressed
    void actionPerformed(e)
    {
        if(e.getSource() != cancel)
        {
            processText();
        }
        dialog.dispose();
    }

    // this is where the work gets done to insert
    // the prefix and suffix
    void processText()
    {
        prefix = prefixField.getText();
        suffix = suffixField.getText();
        if(prefix.length() == 0 && suffix.length() == 0)
            return;
        prefixField.addCurrentToHistory();
        suffixField.addCurrentToHistory();

        // text manipulation begins here using calls
        // to jEdit methods
        selectedLines = textArea.getSelectedLines();
// ORIGINAL START //////////////////////////////////////////////////////////////
//        for(i = 0; i < selectedLines.length; ++i)
//        {
//            offsetBOL = textArea.getLineStartOffset(selectedLines[i]);
//            textArea.setCaretPosition(offsetBOL);
//            textArea.goToStartOfWhiteSpace(false);
//            textArea.goToEndOfWhiteSpace(true);
//            text = textArea.getSelectedText();
//            if(text == null) text = "";
//            textArea.setSelectedText(prefix + text + suffix);
//        }
// ORIGINAL END ////////////////////////////////////////////////////////////////
        for(i = 0; i < selectedLines.length; ++i)
        {
            offsetBOL = textArea.getLineStartOffset(selectedLines[i]);
            textArea.setCaretPosition(offsetBOL);
            textArea.goToStartOfWhiteSpace(false);
            textArea.goToEndOfWhiteSpace(true);
            text = textArea.getSelectedText();
            if(text == null) text = "";
            if(i==0) textArea.setSelectedText(prefix + text);
            if(i==(selectedLines.length - 1)) textArea.setSelectedText(text + suffix);
        }
    }
}

// this single line of code is the script's main routine
// it calls the methods and exits
if(buffer.isReadOnly())
	Macros.error(view, "Buffer is read-only.");
else
	prefixSuffixDialog(view);

/*
	Macro index data (in DocBook format)

<listitem>
    <para><filename>Add_Prefix_and_Suffix.bsh</filename></para>
    <abstract><para>
        Adds user-supplied <quote>prefix</quote> and <quote>suffix</quote>
        text to each line in a group of selected lines.
    </para></abstract>
    <para>
        Text is added after leading whitespace and before trailing whitespace.
        A dialog window receives input and <quote>remembers</quote> past entries.
    </para>
</listitem>

*/

// end Add_Prefix_and_Suffix.bsh

SearchAndReplace.setAutoWrapAround(false);
SearchAndReplace.setIgnoreCase(false);
SearchAndReplace.setRegexp(false);
SearchAndReplace.setSearchFileSet(new CurrentBufferSet());

textArea.setSelectedText("(*?*)");
SearchAndReplace.setSearchString("(*");
SearchAndReplace.setReverseSearch(true);
SearchAndReplace.find(view);

SearchAndReplace.setSearchString("?");
SearchAndReplace.setReverseSearch(false);
SearchAndReplace.find(view);



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.