Re: [isabelle] Show more LaTeX log when there is an error

On Thu, 20 Nov 2014, Joachim Breitner wrote:

maybe my LaTeX is chattier that other people’s LaTeX, but I get:

$ isabelle build -D .
Running Cantor ...

(see also /home/jojo/.isabelle/Isabelle2014/heaps/polyml-5.5.2_x86-linux/log/Cantor)

which is quite unhelpful: The relevant lines are cut of by just 4 lines!

What I usually do here is to open the "see also" file in the editor, and do a hypersearch for "!" to find actual LaTeX errors. It is also possible to keep that file open, and rely on jEdit to reload it automatically after the next build (which can be done from Scala inside Isabelle/jEdit).

Generally, the Isabelle document preparation system is in need of some substantial reforms. Now that the old TTY loop is already removed, there are chances to re-open that topic eventually.

I would like to see LaTeX errors within the IDE, in the normal way directly in the source. This is a bit difficult, because Don Knuth has very strange ways to emit error messages. I need to study a bit more, how other LaTeX IDEs do that, presumably with newer latex options like -file-line-error.

If anybody is aware of existing solutions to extract (La)TeX errors from the log file, I am very interested to see them.


           925,332 people so far

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