Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 08/11/2018 21:36, Lawrence Paulson wrote:
>> On 8 Nov 2018, at 20:32, Makarius wrote:
>>
>> In particular, what are the remaining uses of {* ... *}?
>
> I didn’t even know that existed.
It was used a lot with the 'section' and 'text' commands until recently.
That was actually its main motivation approx. 20 years ago: to delimit
LaTeX sources reliably.
Now the occurrence of {* ... *} in some existing sources makes them look
very old-fashioned, but "isabelle update_cartouches -t" does a thorough
job automatically.
> But I use (*...*) to enclose arbitrary text or comment material out.
Outer comment syntax will remain unchanged: its main purpose is to
comment-out material temporarily, or to write meta-comments (like % in
LaTeX).
Proper document text would normally appear within cartouches and marked
by 'text' or \.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 09/11/2018 00:03, Peter Lammich wrote:
> I sometimes see {* *} in old theory files, and find it funny to be
> reminded that this was standard only 5 years ago ... from my side there
> are no uses of this quotation remaining that I'd know of
Indeed. Do you want to apply "isabelle update_cartouches" yourself on
various AFP entries, e.g. the Automatic_Refinement stack?
> However, (* *) is still very important for informally andquickly
> commenting things out, also in inner syntax!
That is only a historic footnote. It was actually very confusing to have
the same notation (* ... *) in two different meanings:
* outer syntax: material that is not part of the formal document, but
treated like white space; exception: slightly odd meta-comments (*<*)
... (*>*)
* inner syntax: material that is not considered part of the term
language, but shown in the document source in the text style of the term
language
At some point there will more Prover IDE support to add/remove the
various formal comments (with control symbols and cartouches) that have
emerged recently. But the old inner syntax is not coming back.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 09/11/2018 00:08, gerwin.kl...@data61.csiro.au wrote: > We probably still have a few occurrences of these, but no problem > phasing them out. In principle it is just a matter of applying "isabelle update_cartouches -t", but it might require some coordination, especially on AFP. E.g. one could set a date for the "big sweep" and make one big changeset, or one could gradually update entries in an erratic manner. You can probably say better if there are problems to be expected between the "stable" and "devel" versions of AFP. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 08/11/2018 21:32, Makarius wrote:
> Over the decades we have accumulated funny quotation forms in Isabelle
> syntax that are often hard to explain to new users (also to old users).
I don't have a full overview of all the fine points yet, but the general
idea is like this:
* cartouches are the main mechanism to embed/nest languages, e.g.
outer syntax -> document source -> inner syntax -> formal comment ->
antiquotation -> ...
* retain " ... " as a way to quote names and other small bits of text;
its main use to embed inner syntax might eventually be superseded by
cartouches (which some users already do routinely)
* keep the status-quo of (* ... *) as outer comments (source text that
is not part of the document)
The following can be probably phased out right now:
* verbatim quotations {* ... *}
* alt_string `...`
Both become cartouches; this is done by "isabelle update_cartouches"
already.
Rather soon there should be more advanced maintenance tools based on
semantic PIDE markup. E.g. it would allow to replace deeply nested
quotations reliably thanks to formal markup, say as a type/term within
ML. It would also allow to replace ":" by "\" systematically, when
that is formal notation of the term language.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
> On 09.11.2018, at 22:34, Makarius wrote: > > On 09/11/2018 00:08, gerwin.kl...@data61.csiro.au wrote: >> We probably still have a few occurrences of these, but no problem >> phasing them out. > > In principle it is just a matter of applying "isabelle update_cartouches > -t", but it might require some coordination, especially on AFP. > > E.g. one could set a date for the "big sweep" and make one big > changeset, or one could gradually update entries in an erratic manner. > > You can probably say better if there are problems to be expected between > the "stable" and "devel" versions of AFP. I don’t expect too much trouble from this one. It might make sense to try out how the conversion goes a few entries first, and then, if that is satisfactory, do a big change set for the rest. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
