[isabelle-dev] Allowed characters in theory names for document build

[Christian Weinz]

Dear all,

Isabelles pdflatex document build fails when there is a space or any of
ä, ö, ü, ß and % in a theories name. Possibly more characters are
affected.

When trying to build the pdf for the theory ä, I get

  $ (...)/bin/isabelle build -D .
  *** Bad theory name "ä" for file "ä.thy" (line 1 of "ä.thy")
  *** The error(s) above occurred for theory "ä" (line 1 of "ROOT")
  *** The error(s) above occurred in session "isabelle" (line 1 of
"ROOT")

and no output directory is created. When trying to build the pdf for
the theory "a b", I get

  $ (...)/bin/isabelle build -D .
  Running isabelle ...
  isabelle FAILED
  (see also /home/christian/.isabelle/Isabelle2016-1/heaps/polyml-
5.6_x86-linux/log/isabelle)
  *** (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg)
  *** (/usr/share/texlive/texmf-dist/tex/latex/graphics-
def/pdftex.def)))
  *** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
  *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-
hyperref.sty
  *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-
generic.sty))
  *** (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
  *** (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
  *** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
  *** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
  *** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
  *** (/usr/share/texlive/texmf-
dist/tex/latex/latexconfig/hyperref.cfg)
  *** (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
  *** 
  *** Package hyperref Message: Driver (autodetected): hpdftex.
  *** 
  *** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
  *** (/usr/share/texlive/texmf-
dist/tex/latex/oberdiek/rerunfilecheck.sty))
  *** No file root.aux.
  *** (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-
pdf.mkii
  *** [Loading MPS to PDF converter (version 2006.09.02).]
  *** ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
  *** (/usr/share/texlive/texmf-
dist/tex/generic/oberdiek/gettitlestring.sty))
  *** (./session.tex
  *** 
  *** ! LaTeX Error: File `a b.tex' not found.
  *** 
  *** Type X to quit or <RETURN> to proceed,
  *** or enter new name. (Default extension: tex)
  *** 
  *** Enter file name: 
  *** ! Emergency stop.
  *** <read *> 
  ***          
  *** l.1 \input{a b.tex}
  ***                    ^^M
  *** !  ==> Fatal error occurred, no output PDF file produced!
  *** Transcript written on root.log.
  *** Document preparation failure in directory 'output/document'
  *** 
  *** Failed to build document
"/home/christian/Programmierung/isabelle/output/document.pdf"
  Unfinished session(s): isabelle
  0:00:03 elapsed time

and the output directory is created. Inside this directory I find the
session.tex with the following content

  \input{a b.tex}
  
  %%% Local Variables:
  %%% mode: latex
  %%% TeX-master: "root"
  %%% End:

When I change the first line to

  \input{"a b.tex"}

I can manually successfully compile the pdf.

These two cases seem to have different underlying reasons. In the first
case Isabelle seems to be confused with the ä, in the second case LaTeX
seems to be confused with the filename. 

Percent signs in quoted filenames in LaTeX can be escaped by adding

  \catcode`\%=12
  \newcommand\pcnt{%}
  \catcode`\%=14

to the preample in root.tex and replacing each % with "/pcnt" in the
filenames. I don't know if that is the optimal solution.

I looked where the file session.tex is created to add the quotation and
escaping to fix the second issue, but I didn't find it.

Also, is there a way to escape the character " in theory names?

To make Isabelle and its document build feature more permissive with
filenames, what is the best way to solve these issues?

Best regards,
Christian Weinz