Re: [isabelle-dev] NEWS: formal comments

On 06.02.2018 17:31, Tobias Nipkow wrote: This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient. Informal outer comments are not going to disappear. That means that users who don't have a formal meaning of

Re: [isabelle-dev] NEWS: formal comments

This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient. Tobias On 06/02/2018 15:13, Lawrence Paulson wrote: Will there still be a way to comment out random junk? I often work with a mixture of Isabelle and

Re: [isabelle-dev] NEWS: formal comments

Will there still be a way to comment out random junk? I often work with a mixture of Isabelle and commented-out HOL Light material. Larry > On 26 Jan 2018, at 20:19, Makarius wrote: > > * Old-style inner comments (* ... *) within the term language are legacy > and will be

[isabelle-dev] NEWS: formal comments

*** General *** * Marginal comments need to be written exclusively in the new-style form "― ‹text›", old ASCII variants like "-- {* ... *}" are no longer supported. INCOMPATIBILITY, use the command-line tool "isabelle update_comments" to update existing theory files. * Old-style inner comments

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)

[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.