Re: [isabelle-dev] NEWS: formal comments for inner syntax etc.
On 11/01/18 14:51, Makarius wrote:
>
> Isabelle/7360fe6bb423 is an example for a change to "prefer formal
> comments": this requires delicate work by hand, because the intended
> meaning of a comment can vary:
>
> (1) comment as plain text (with regular typesetting in the document)
> (2) comment containing formal text, e.g. @{term} or @{cartouche}
> (3) old/unwanted source text that is actually "commented-out"
>
> I am in the process the update cases (1) and (2) in all of Isabelle +
> AFP, but case (3) is still untouched. The latter might require a
> different formal notation, e.g. \<^blank>\text\.
In the meantime I have manually updated Isabelle + AFP, using notation
\<^cancel>\text\ (with fancy rendering in
Isabelle/0b691782d6e5). The document output uses a version of
"strike-through" in LaTeX, e.g. see
https://devel.isa-afp.org/browser_info/current/AFP/SPARCv8/document.pdf
page 6 (definition of "get_S").
A bit more is emerging: uniform formal comments in outer and inner
syntax: \, \<^cancel>, \<^latex> (for raw LaTeX source). When
that is done, I will post a proper NEWS announcement.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: formal comments for inner syntax etc.
*** Document preparation ***
* Embedded languages such as inner syntax and ML may contain formal
comments of the form "\ \text\". As in marginal
comments of outer
syntax, antiquotations are interpreted wrt. the presentation context of
the enclosing command.
This refers to Isabelle/e9bee1ddfe19. It means that inner and outer
syntax comments work uniformly (with the same context), and arbitrary
embedded languages benefit as well (e.g. Isabelle/ML or the "rail"
language).
Also note that there is fancy notation by the IsabelleText font:
"\ \text\" looks like "― ‹text›" in the Prover IDE.
Moreover note that the existing tool "isabelle update_cartouches -c -t"
updates outer syntax to that fancy form (and more).
Isabelle/7360fe6bb423 is an example for a change to "prefer formal
comments": this requires delicate work by hand, because the intended
meaning of a comment can vary:
(1) comment as plain text (with regular typesetting in the document)
(2) comment containing formal text, e.g. @{term} or @{cartouche}
(3) old/unwanted source text that is actually "commented-out"
I am in the process the update cases (1) and (2) in all of Isabelle +
AFP, but case (3) is still untouched. The latter might require a
different formal notation, e.g. \<^blank>\text\.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
