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



On 8/8/2012 4:40 PM, Makarius wrote:
You can also try the "TextTools" plugin of jEdit, with its action
"Toggle Range Comment":

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

That's the solution. Commenting and uncommenting with that plugin produces no error, unlike "Edit / Source / Range comment".

It doesn't take any practice at all. I assign a shortcut to it, highlight the commented or uncommented text, and toggle the commenting.

*OTHER PLUGINS*

I also found another good plugin when going to get TextTools, which is XSearch: http://plugins.jedit.org/plugins/?XSearch

I have java.util.regex with jEdit search, or gnu.regexp with XSearch.

It also allows me to put the search field in the bottom panel, so I can get rid of the normal search field at the top, with "Global Options/ jEdit / View". I include a screen shot to show my use of the three panels, like putting XSearch at the bottom, and its hypersearch results in the right panel.

Then there's always the Console plugin, where I can do something like "grep lemma %f", and it'll search on the current edit buffer. Details are in "Help / Plugins / Console" for anyone interested in more details. I attach a screen shot of grep in action through the Console plugin. People should see these things so they know what they're missing out on.

For plugins seekers, one of the most useful is the the Optional plugin, which combines the three plugin windows into one window, which are normally accessed through different menus: http://plugins.jedit.org/plugins/?Optional

*UNRELATED EXTERNAL-ISAR EMAIL COMMENT*

I got some good vocabulary from that other email.

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-August/msg00037.html

Trying to talk about Pure intelligently can be an elusive thing.

There's the "Isar source language", which makes sense of the "Isar proof language" as a "sub-language"; after all, Isar has a lot of non-proof related commands.

At some point I start accepting things axiomatically; "Let it be known, a principle developer has said that what is between 'theory' and 'end' is all Isar". But having good language makes it easier for me to process difficult ideas.

People wouldn't want to argue about it here, but I tend towards a variation of this following idea:

The  strong form of Sapir-Whorf Hypothesis proposes that language determines
thought; therefore they are identical in nature. This argument in fact implies that
thought is impossible without language.
http://www.thomastsoi.com/wp-content/downloads/The%20Relationship%20between%20Language%20and%20Thought.pdf

I never heard of the "Sapir-Whorf Hypothesis" before I did the Google search just now, but I did take a course that influenced me called "The structure of the English language", where the author of the textbook was a linguist.

I would only say that efficient and clear thought is impossible without efficient and clear language, which brings up the subject of the need for good mathematical notation as a language. Ideas that are fuzzy become clear when formalized with good language.

There's "the self-defining self-embedding game of formal languages", and so, related to that, HOL being embedded in Isar would be part of the game of embedding one language into another. If I find the right pithy phrases, I can be perfectly content keeping my thoughts at a high level, while allowing the backend prover to do its low-level magic.

Regards,
GB












Attachment: 3_panels.png
Description: PNG image

Attachment: grep_in_console.png
Description: PNG image



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