Email Gateway (Aug 19 2022 at 08:13): Email Gateway (Aug 19 2022 at 08:13):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
3_panels.png
grep_in_console.png
Email Gateway (Aug 19 2022 at 08:13):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Actually, an example of the "one language embedded into another game"
would be FOL embedded in HOL. In the process of building up HOL, you get
primitive type variables, the standard logical connectives and
quantifiers, the ability to define predicates, and the enforcement of
standard FOL formula-making rules. If you get rid of that part of HOL,
then you lose FOL too.
At some point, standard dictionary definitions don't completely
translate the meaning of formal, programming languages, on the other
hand, there's many times a strong relationship.
So, I'm deciding that I shouldn't confuse the "embedded game" with the
"framework game"; frameworks can be taken down, where embeddings
generally remain embedded.
I'm back to contemplating what may be involved with the Isar and HOL
"framework game", at least until I click the send button.
Email Gateway (Aug 19 2022 at 08:34):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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_First_and_Suffix_Last.bsh
comment (star-star).bsh
Email Gateway (Aug 19 2022 at 08:34):From: Gottfried Barrow <gottfried.barrow@gmx.com>
At least part of the problem is a "(" and ")" (or other sets of
matched delimiters) not being inserted on the same line.
I do this with my modified "Add_Prefix_and_Suffix.bsh" or with "Edit /
Source / Range Comment",
(*
find_consts name:List.list.Nil
value "a # b # List.Nil"
*)
and it results in an error until I save the file or delete the block and
reinsert it.
I do this with "Add_Prefix_and_Suffix.bsh" or "Edit / Source / Line
Comment",
(find_consts name:List.list.Nil)
(value "a # b # List.Nil")
and I get no errors.
That's a workaround to commenting out code, but only if I have a macro
that will uncomment it line by line.
More details. I do this with my modified "Add_Prefix_and_Suffix.bsh",
and I get no errors:
text{*value "a # b # List.Nil"
value "a # b # List.Nil"*}
I do this, and I get errors:
text{*value "a # b # List.Nil"
value "a # b # List.Nil"
value "a # b # List.Nil"*}
So if the "text{" and "} get inserted over more than two lines, then I
get the error, and the same thing with "(" and ")".
It's never simple. Using my modified macro, this gets no error with the
blank line in between:
(*value "a # b # List.Nil"
value "a # b # List.Nil"*)
Regards,
GB
Email Gateway (Aug 19 2022 at 08:34):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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:
http://community.jedit.org/?q=filestore/browse/31
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]);
textArea.setCaretPosition(offsetBOL);
textArea.goToStartOfWhiteSpace(false);
textArea.goToEndOfWhiteSpace(true);
text = textArea.getSelectedText();
if(text == null) text = "";
if(i==0) textArea.setSelectedText("(*" + text);
if(i==(selectedLines.length - 1)) textArea.setSelectedText(text
if(buffer.isReadOnly())
Macros.error(view, "Buffer is read-only.");
else
commentOutText();
Email Gateway (Aug 19 2022 at 08:35):From: Makarius <makarius@sketis.net>
You can also try the "TextTools" plugin of jEdit, with its action
"Toggle Range Comment":
Toggle Range Comment by Robert Fletcher <rfletch6@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
Last updated: Apr 23 2024 at 08:19 UTC