Re: [isabelle] Unable to get document preparation system to work

On Tue, 28 Jan 2014, James Lingard wrote:

*** Runaway argument?
*** ! File ended while scanning use of \next.
*** <inserted text>
***                 \par
*** l.1 \input{mytheory.tex}
*** ))
*** ! Emergency stop.
*** <*> \nonstopmode\input{root.tex}
*** !  ==> Fatal error occurred, no output PDF file produced!
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'
*** Failed to build document "/Users/jchl/test/output/document.pdf"
Unfinished session(s): test
0:00:10 elapsed time, 0:00:16 cpu time, factor 1.60

That is a latex error, so it just depends on the actual sources that are given to it. It is all in the directory "output/document" mentioned above. You can cd there and just run pdflatex directly, and look closely again what is there in the files. There is some chance that some odd control characters somehow sneaked in (maybe via "cat"), or something completely different and unexpected.

If you still don't see it, just send me the actual output/document/ content.

Some side-remarks:

  * Isabelle session names and theory names consist of capitalized words
    (separated by underscores), e.g. Foo, Bar, Baz, My_Theory.  Almost
    everything inside a theory uses lowercase names (including types, but
    excluding datatype constructors).

  * Isabelle/jEdit takes some time to start-up, but once it is running it
    is able to edit text files conveniently, including ROOT.

I have recently learned about the server mode of jEdit, which is off by default. If enabled it is easy to delegate edit tasks from the command-line to an already running jEdit application. (That might be worth a different mailing list thread.)


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