[isabelle-dev] NEWS: formal comments for inner syntax etc.

[Makarius]

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