Re: [isabelle] LateXsugar broken?

On Sun, 5 Apr 2009, Christian Doczkal wrote:


Replace the "term" command by an antiquotation, eg

text{* @{term "if a then b else c"} *}


I'm afraid that is not possible.

What is the fundamental difference between rendering a term in the
theory as latex output and rendering a term in an antiquotation as latex
output? I was expecting that both use the same mechanisms.

Isabelle document preparation works primarily by presenting the original sources in a relatively smart way, such that you might think the system really understands formal notation etc, which it does not.

So if you present

  prop "A ==> B"

you will get a slightly ugly ASCII version, corresponding to what is written in the source. You need to present a "meta-source" to get full notation, e.g. like this:

text {*
  @{prop "A ==> B}

This works, because document antiquotations can present fully internalized terms by pretty printing them again, according to current print mode setup. LaTeX sugar heavily depends on this a lot.


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