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:

  pr (latex)

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 content.

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 MHonArc.