Email Gateway (Aug 22 2022 at 17:43): Email Gateway (Aug 22 2022 at 17:43):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,
(* ... *) comments are now deprecated for use in inner syntax. One use
of comments in inner code is to comment out parts of a formula, e.g.
"foo <--> (* A /\ *) B /\ C". I believe that ⌦‹...› is the right
replacement here. However, when using the latter, only the ⌦ symbol is
highlighted in Isabelle/jEdit, making it hard to read the formula. In
contrast, with (* ... *) comments, the whole comment is highlighted in
red.
Is it possible to highlight the whole ⌦‹...› comment in Isabelle/jEdit?
The same remark applies to ― ‹...› (though one could argue that putting
comments in the middle of a line is bad style).
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:43):From: Dominique Unruh <unruh@ut.ee>
Hi,
related to this, it would probably also be useful if Ctrl-E Ctrl-C would
insert ⌦‹...› comments instead of the legacy comments.
(But I don't know if that is a simple or a complex thing to do.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:43):From: Lawrence Paulson <lp15@cam.ac.uk>
It's worth recalling some of the general features of the jEdit editor. These include the ability to define and modify keyboard shortcuts. Look under Plugins > Plugin Options, click on Global Options and then select Shortcuts from the list on the left.
(Another useful feature is Markers.)
Larry
Email Gateway (Aug 22 2022 at 17:43):From: Dominique Unruh <unruh@ut.ee>
It's worth recalling some of the general features of the jEdit editor.
These include the ability to define and modify keyboard shortcuts. Look
under Plugins > Plugin Options, click on Global Options and then select
Shortcuts from the list on the left.
I know. But it is beyond my jEdit knowledge to tell how to write a macro
that inserts (* *) outside term syntax, but ⌦‹...› inside the term syntax.
Best wishes,
Dominique.
(Another useful feature is Markers.)
Larry
On 30 Jul 2018, at 15:36, Dominique Unruh <unruh@ut.ee> wrote:
Hi,
related to this, it would probably also be useful if Ctrl-E Ctrl-C would
insert ⌦‹...› comments instead of the legacy comments.
(But I don't know if that is a simple or a complex thing to do.)Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:44):From: Makarius <makarius@sketis.net>
jEdit has actions line-comment and range-comment to insert comments
according to mode properties LineComment and CommentStart/CommentEnd.
In principle, line-comment could be used for new-style formal comments,
but there are hard-wired assumptions: comment-start + space, no
comment-end, where it should be comment-start ⌦‹ + comment-end › without
extra space.
I did not know about these facilities so far, and put it on the TODO
list for future refinements (after Isabelle2018), including patches of
jEdit.
Of course, one could also think of actions for cancel-comments, beyond
the standard facilities of jEdit.
Here is also a reminder of the canonical terminology:
* "jEdit": a sophisticated text editor written in Java, see
http://jedit.org
* "Prover IDE" or "PIDE": a huge technology stack with the
Isabelle/jEdit front-end facing the user, but there is already
Isabelle/VSCode slowly emerging.
When I write "jEdit", I really mean the text editor. And when I say the
"Prover IDE", I mean the huge thing with one of the usual front-ends.
Makarius
Email Gateway (Aug 22 2022 at 17:44):From: Makarius <makarius@sketis.net>
In principle, there are a lot of possibilities for variation, but it
always requires some time for experimentation, how certain nested
combinations come out visually.
RC3 is already too far towards the final version to reconsider this --
RC0 or RC1 were still possible.
At least a control-hover highlights the nested formal comment in a
clearly visible manner, but it requires the mouse.
Makarius
Email Gateway (Aug 22 2022 at 18:00):From: Peter Lammich <lammich@in.tum.de>
To re-open this thread:
I also find the missing highlighting of \^cancel comments REALLY
ANNYOING. In some use-cases, I use commenting out parts of a term a
lot, and this get's really unreadable now.
RC3 is already too far towards the final version to reconsider this
So even if it has been too late for Isabelle2018, please DO consider
proper highlighting of inner syntax comments.
For now, I'm back to using the legacy (* ... *) syntax, which, btw, is
slightly easier to type.
Email Gateway (Aug 22 2022 at 18:43):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Peter Lammich wrote:
Same here.
However, the legacy syntax has been discontinued in the development
version, so this issue will be important for the next release.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 18:44):From: Peter Lammich <lammich@in.tum.de>
So +1 from me to have the next release with a usable mechanism for ad-
hoc commenting-out of parts of inner syntax. At least for my style of
Isabelle development and proof exploration this is essential to have.
The \cancel\open ...\close syntax is slightly more annoying to type
than (* ... *) was, but would be OK if properly highlighted as
commented out.
Last updated: Apr 25 2024 at 20:15 UTC