Re: [isabelle] Generating .tex from .thy without a proper session
On Fri, 8 Feb 2013, Joachim Breitner wrote:
I want to include some isabelle-generated LaTeX from a small fragment.
Now I’d like to figure out how to convert that to .tex, without creating
a full session and running "isabelle build" and then extracting the .tex
from the generated .tex files.
If this is feasible in Isabelle2012 or Isabelle2013 depends on how small
the fragment might be.
For example, you can print formal entities with the "latex" print mode
interactively like this:
thm (latex) exI exE
or goal states:
This is a half-forgotten and quite archaic form. I can't tell on the
spot how far it still works.
Another approximation is display_drafts, which is Present.drafts in ML.
It merely does pretty printing of Isabelle symbols, without any formal
Is there a low-level-command that goes from .thy directly to .tex,
without a session infrastructure involving ROOT and document/root.tex?
That is difficult with the full spectrum of document antiquotations etc.
The main entry point for that is Thy_Output.present_thy but that is not
easily invoked manually.
Proper document preparation is still intertwined with the session concept,
although there is conceptually no strong reason for it, just old habits.
In the past few years, I have occasionally made tiny steps to make it more
value oriented, operating on given sources more systematically. My
immediate motivation is to have document preparation within the Prover
IDE, to avoid the relatively clumsy batch build sessions.
This archive was generated by a fusion of
Pipermail (Mailman edition) and