Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE

On Sat, 14 Nov 2015, Gottfried Barrow wrote:

1) A TeX file, full of LaTeX commands, isn't readable.

2) When a THY is marked up heavily in LaTeX, the THY isn't readable.

3) Should I go further? Isar commands, such as 'subsubsection', which are fashioned after the corresponding LaTeX commands, contribute nothing to readability, and in fact, hinder readability, just like LaTeX.

This is not criticism on my part. It's a reflection of what has been important to you, given that you prioritize according to what you want.

My goal? Eliminate all use of LaTeX from THY documents (other than a few infrequently used commands), and moreover, eliminate "verbose" Isar commands that distract from readability.

Here's a LaTeX command from ML.thy: \begin{verbatim}

A LaTeX verbatim command like that will never be in my THY. In my THY, verbatim environment markup never has to be used, except for the few places outside of a newtheorem environment, and there the syntax is reasonably subtle.

Have you tried Isabelle2016-RC0 already?

It provides many new things concerning document markup and markdown. Very few LaTeX macros are remaining. Since you are using creative add-ons to Isabelle document preparation, there is also a chance that something stops working.

Now is still a chance to work it out. Later in the release process, further changes will be less likely.


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