Re: [isabelle] Isabelle2019-RC2: Experience report



On 14/05/2019 13:46, Peter Lammich wrote:
>   * The NEWS file does not specify any replacement for old style inner
> comments (* *). The entry for Isabelle-2018 says to use \comment or
> \cancel. However, content of \comment is interpreted as latex text,
> causing trouble with unknown antiquotations when e.g. trying to comment
> out "{1,2}@{a,b}". Moreover, \cancel used to occur in "striked out"
> style in Latex output, at least when used in outer syntax. Is this also
> the case for inner-syntax \cancel? 

Old style inner comments were not really well-defined, and treated
differently from outer comments (which are like % in LaTeX).

The purpose of the reform of formal comments was to make it all work
uniformly, e.g. see the included example.


> Can I make parts of inner syntax disappear from latex output?

Is that a new feature request for Isabelle2020?

In Isabelle2019 you can try with the low-level \<^latex> operator, but
it is a bit awkward and fragile. For example:

term ‹x\<^latex>‹%ignored @{text}
››


	Makarius
theory Test
  imports Main
begin

term \<open>x\<^latex>\<open>%ignored @{text}
\<close>\<close>

end

Attachment: document.pdf
Description: Adobe PDF document



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.