Re: [isabelle-dev] NEWS: discontinued old-style inner comments
On 24/09/18 08:19, Lars Hupel wrote: >> There were a few remaining uses in AFP. Notable changes are >> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources >> generated by LEM (!). I don't know how LEM is maintained: it needs to >> produce different inner comments next time, and can actually use >> \ CARTOUCHE notation uniformly for inner and outer comments -- >> also note that this needs to be LaTeX-conformant, e.g. by another nested >> cartouche or \<^verbatim>CARTOUCHE. > > The way this works is that I'll have to send them a patch. This should > hopefully be simple enough. OK, thanks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: discontinued old-style inner comments
> There were a few remaining uses in AFP. Notable changes are > AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources > generated by LEM (!). I don't know how LEM is maintained: it needs to > produce different inner comments next time, and can actually use > \ CARTOUCHE notation uniformly for inner and outer comments -- > also note that this needs to be LaTeX-conformant, e.g. by another nested > cartouche or \<^verbatim>CARTOUCHE. The way this works is that I'll have to send them a patch. This should hopefully be simple enough. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: discontinued old-style inner comments
*** General *** * Old-style inner comments (* ... *) within the term language are no longer supported (legacy feature in Isabelle2018). This refers to Isabelle/6e9df530b441. There were a few remaining uses in AFP. Notable changes are AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources generated by LEM (!). I don't know how LEM is maintained: it needs to produce different inner comments next time, and can actually use \ CARTOUCHE notation uniformly for inner and outer comments -- also note that this needs to be LaTeX-conformant, e.g. by another nested cartouche or \<^verbatim>CARTOUCHE. Now that (* ... *) is no longer part of the term language, Tobias can finish the infix syntax update project, to get rid of the slightly odd extra spaces for infixes with *. There is also a chance that this will speed up the inner parser and/or grammar updates, which happen quite often (e.g. for local syntax). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
