Re: [isabelle-dev] NEWS: formal comments

2018-02-06 Thread Makarius Wenzel 

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 comments in 
mind can remain unclear about it as before. (BTW, I often see outer 
comments in AFP articles that are actually meant as formal 'text' 
blocks, but apparently the authors never looked at the PDF output, where 
the informal comments are not shown at all -- just like % in LaTeX.)



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments

2018-02-06 Thread Tobias Nipkow 
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 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 discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
instead.




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments

2018-02-06 Thread Lawrence Paulson 
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 discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
> instead.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: formal comments

2018-01-26 Thread Makarius 
*** 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 (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
instead.


*** Document preparation ***

* Formal comments work uniformly in outer syntax, inner syntax (term
language), Isabelle/ML and some other embedded languages of Isabelle.
See also "Document comments" in the isar-ref manual. The following forms
are supported:

  - marginal text comment: ― ‹…›
  - canceled source: ⌦‹…›
  - raw LaTeX: \<^latex>‹…›


*** System ***

* The command-line tool "isabelle update_comments" normalizes formal
comments in outer syntax as follows: ― ‹text› (whith a single space to
approximate the appearance in document output). This is more specific
than former "isabelle update_cartouches -c": the latter tool option has
been discontinued.



This refers to Isabelle/5db077cfe1b2: it is a summary of all
comment-related updates, simplifications, and clarifications of the past
few weeks.

I have already updated the visible Isabelle universe including AFP. When
old-style inner comments (* ... *) are finally discontinued, we can
reunify infix notation for (+) vs. (*) etc. without extra spaces.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2018-01-14 Thread 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>\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.

2018-01-11 Thread Makarius 
*** 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