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

I have the macro to comment out code down to what's below. Surely all I have to do is cut what I had selected and then insert it back in. That's what I manually do to get rid of the error after commenting it out, cut and reinsert. I'm looking here to see if I can find a quick way to figure out how to do that:

Deleting the "(*" and "*)" manually to uncomment the code doesn't seem to cause problems. I'm not inclined to learn how to do it with regular expressions with jEdit, so that may have to be good enough.

void commentOutText()
    selectedLines = textArea.getSelectedLines();
    for(i = 0; i < selectedLines.length; ++i)
        offsetBOL = textArea.getLineStartOffset(selectedLines[i]);
        text = textArea.getSelectedText();
        if(text == null) text = "";
        if(i==0) textArea.setSelectedText("(*" + text);
if(i==(selectedLines.length - 1)) textArea.setSelectedText(text + "*)");

    Macros.error(view, "Buffer is read-only.");

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