Email Gateway (Aug 22 2022 at 20:25): Email Gateway (Aug 22 2022 at 20:25):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear list,
Why Isabelle insist to parse the following:
(― ‹ @{const X} is useful as a coercion map ›)
Note that this comment is between (**), the standard behaviour for the
last 7 years is that Isabelle should not try to parse things between (**),
why it does for this situation?
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:25):From: Peter Lammich <lammich@in.tum.de>
Even worse, the parse is only partial!
For @{term}, you can have type-errors, but no syntax errors, e.g.
(*
― ‹ @{term "Suc 1 2"} ›
NO ERROR
― ‹ @{term "MyBinder x. f x"} ›
ERROR (if syntax for MyBinder is not defined)
*)
Having comments that allows one to quickly "comment out" parts of a
development that are currently not needed is a very important tool in
many developers workflows. It has already been severely restricted by
removing commenting out from inner syntax, but I was not aware that it
also ceased to work in outer syntax.
FEATURE REQUEST: Provide a proper way to "comment out" arbitrary
content, in inner and outer syntax. Proper means that Isabelle makes no
assumptions on the "commented out" content, apart from basic lexical
properties like balanced begin-comment end-comment symbols or balanced
cartouches.
Email Gateway (Aug 22 2022 at 20:25):From: Peter Lammich <lammich@in.tum.de>
WORKAROUND: Use \<cancel>\<open> ... \<close>.
Nothing seems to be parsed inside this.
However, the question remains what is the intention of (* ... *)
comments, and why do they only partially parse their content?
As I have already posted in relation to discontinuing (**)-comments for
inner syntax, I find (**)-comments much more convenient to type than
\<cancel>\<open> ... \<close>, in particular when commenting out
existing text ... I have to type "\cancel<tab>\open<tab>" at the
beginning, and "\close<tab>" at the end of the comment. These are 14
keystrokes compared to 4 keystrokes for (**). As I comment out text
quite frequently, (both in inner and outer syntax), I find this really
annoying, and have not yet got used to it.
Is there any convenient way to "comment out" and "uncomment" text with
fewer keystrokes?
Last updated: Apr 25 2024 at 20:15 UTC