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>\<open>text\<close>.
In the meantime I have manually updated Isabelle + AFP, using notation
\<^cancel>\<open>text\<close> (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: \<comment>, \<^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
