[isabelle] Unable to get document preparation system to work



I'm new to Isabelle, and am struggling to get the document preparation
system to work for the first time.  Here's what I tried:

$ isabelle mkroot -d test
...
$ isabelle build -D test
...

This successfully creates a dummy test/output/document.pdf file.  Now I
create the simplest possible theory file, and try to incorporate that:

$ cat > test/mytheory.thy
theory mytheory imports Main
begin
end
$ vi test/ROOT # to add mytheory
$ cat test/ROOT
session "test" = "HOL" +
  options [document = pdf, document_output = "output"]
  theories [document = false]
    (* Foo Bar *)
  theories
    mytheory (* Baz *)
  files "document/root.tex"

Now the build fails with a bizarre LaTeX error:

$ isabelle build -D test
Running test ...

test FAILED
(see also
/Users/jchl/.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-darwin/log/test)

*** [Loading MPS to PDF converter (version 2006.09.02).]
*** )
(/usr/local/texlive/2013basic/texmf-dist/tex/latex/hyperref/nameref.sty
*** (/usr/local/texlive/2013basic/texmf-dist/tex/generic/oberdiek/
gettitlestring.st
*** y)) (./root.out) (./root.out) (./root.toc) (./session.tex
(./mytheory.tex
*** Including 'isadelimtheory' comment.)
*** 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

Can anyone help me understand what (if anything) I'm doing wrong, and how I
can fix it?

Version info:
-  Isabelle2013-2: December 2013
-  pdfTeX 3.1415926-2.5-1.40.14 (TeX Live 2013)
-  OS X 10.9.1

Thanks,
James.



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