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



On Wed, 8 Aug 2012, Gottfried Barrow wrote:

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.

You can also try the "TextTools" plugin of jEdit, with its action
"Toggle Range Comment":

  Toggle Range Comment by Robert Fletcher <rfletch6 at yahoo.co.uk>

  Toggles the state of range comments in the selection. Any text currently
  commented out will become uncommented and vice-versa. If there is no
  selection the command acts on the entire line at the caret position.
  Supports all edit modes with defined range comment symbols and works
  with embedded modes such as JavaScript within HTML.

It looks not so bad at first sight, but might require some practice to work with it smoothly.


BTW, when things go amiss, one needs to keep in mind that there are two different notions of quoted regions and comments: one of jEdit (according to the token marker) and another of the prover process.

This can sometimes lead to extra confusion, due to disagreement of the syntax highlighting. I will try harder next time to make this agree, especially since the jEdit token marker for Isabelle mode is also my responsibilty.


	Makarius





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