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

On 11/14/2015 2:18 PM, Makarius wrote:
There is already a "tag" feature that allows to wrap Isabelle document commands (like 'text') or other formal command (e.g. proof commands) in a LaTeX environment.
An example can be seen here: ...
Maybe that is already sufficient to implement all 3 points above.

I suppose I should finish what I started, which requires that I attempt to explain some of my ideas.

I attach two images which show what I did the first year in 2012, when I implemented about 9 ZFC axioms based on Obua's THY. The particular image shows work on permutative rewrite rules. T.Nipkow tipped me off about those. As to the words in the image, don't pay too much attention to that. I say more about the images below.

Thanks for the links. I opened the document. I'll use some of it to argue that we're not in sync as to our current vision of what the internals of a THY should look like.

(NOTE: At line 564 all I see special is '%mlex'. You might mean that commands are available to tie into the low-level machinery. If that's what you mean, I don't know how much that helps me. Using machinery can require getting educated about the machinery. It's much easier to get educated about things like parsing with PEG.js and Node.js, than it is to get educated about Isabelle machinery. What I say below may reflect that I didn't get your drift, but I think we're still at odds.)

First, by all appearances, you prioritize according to what want. With syntax, what's not there must reflect your own personal preferences.

Now, I state two opinions:

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.

You say, "Maybe that is already sufficient to implement all 3 points above. " No. (SEE NOTE ABOVE)

My markup "tags" are outer syntax definitions. They wrap what they're supposed to mark up, and nothing wraps the markup tags, because wrapping requires additional characters and symbols. What I have as outer syntax may also sometimes be used in textual exposition, where, of course, it's text, though still markup, but that's not wrapping, that's using tags in text. (SEE NOTE ABOVE)


Defining too many outer syntax commands is no good, so my FOOBAR was a general purpose text-text command, one use being a LaTeX equation environment. Everything is subject to further change, but I show its use, where the period represents \<cdot>, and "<" and ">" represent cartouche delimiters.

  .<x + y = z + w
          = m + y
          = q + r><eq.jkl1608>

The alignment of the '=' symbols may get lost.

I will parse that equation into a LaTeX environment, inserting end-of-lines, and whatever else is necessary. The '\<open>eq\<cdot>' is the part of the tag that tells me it's an equation environment. It's possible, given the numerous types of LaTeX equation environments, I might want 'e1', 'e2', etc. to represent other kinds of environments.

I could change 'eq' to 'q', but the '\label', 'jkl1608',is most of the clutter, so there's no reason to save one letter.

If all my syntax is defined, I can also have a term-text command, so that my formula is an active term, rather than just text.


In 2012 and 2013 I developed my funky markup language, with just a little knowledge of regular expressions. Since then, the words "parsing" and "grammars" sunk in to my conscientious. It's the result of being exposed to the talk of computer scientists, who deal in languages.

I'm trying to get back to where I was, but with much cleaner syntax. It'll take me six months to a year to get there, because I'm also trying to work on getting some number systems, vectors, and boolean logic done.

The first image is my funky markup, in the THY, which is fairly readable. The second image shows my PDF. These things involve personal preference, but I like how my PDF looks.

I've moved on, on some things, but it formed the basis of some things. I can't converge back, from the divergence. I'm too deep in. What's most important is that I actually finish something.


Attachment: 151114a_Z_thy.png
Description: PNG image

Attachment: 151114b_Z_pdf.png
Description: PNG image

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