On Fri, Nov 19, 2010 at 8:58 AM, Tobias Nipkow <[email protected]> wrote: > I don't understand this: why does latex work for the release version but > not the development version? But indeed, it fails for me too.
I created an extremely simplified version of the Shivers-CFA entry (building on Isabelle/Pure instead of HOLCF) that still reproduces the latex error, and did some bisection. The origin of the problem is this revision: http://isabelle.in.tum.de/repos/isabelle/rev/b646316f8b3c basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols; The root.tex of the Shivers-CFA entry contains the following two lines: \usepackage[normalem]{ulem} \newcommand{\isactrlps}[1]{{\uline #1}} Here is the stripped-down version of the entry I used for testing: theory Computability imports Pure begin definition foo :: "'a => 'a" ("\<^ps>") where "\<^ps>f == f" end ... and here is the diff of the generated Computability.tex files, comparing revision b646316f8b3c (+) to its parent revision (-). \isanewline \isanewline \isacommand{definition}\isamarkupfalse% -\ foo\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlps {\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}\isactrlps f\ {\isacharequal}{\isacharequal}\ f{\isachardoublequoteclose}\isanewline +\ foo\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}\isaliteral{5C3C5E70733E}{}\isactrlps {\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline +\ \ {\isaliteral{22}{\isachardoublequoteopen}}\isaliteral{5C3C5E70733E}{}\isactrlps f\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline % \isadelimtheory \isanewline Finally, here are the relevant LaTeX error messages: *** (./session.tex (./Computability.tex *** ! Undefined control sequence. *** <argument> \...@spfactor *** *** l.27 ...\isaliteral{22}{\isachardoublequoteclose}} *** {\isaliteral{29}{\isacharp... *** *** ! Undefined control sequence. *** \...@word ...kip \unskip \spacefactor \...@spfactor *** \let \...@word \egroup \els... *** l.27 ...\isaliteral{22}{\isachardoublequoteclose}} *** {\isaliteral{29}{\isacharp... *** *** ! Missing number, treated as zero. *** <to be read again> *** \let *** l.27 ...\isaliteral{22}{\isachardoublequoteclose}} *** {\isaliteral{29}{\isacharp... *** *** ! Bad space factor (0). *** <to be read again> *** \let *** l.27 ...\isaliteral{22}{\isachardoublequoteclose}} *** {\isaliteral{29}{\isacharp... *** *** )) - Brian > Brian Huffman schrieb: >> On Fri, Nov 19, 2010 at 7:28 AM, Brian Huffman <[email protected]> wrote: >>> The latex document generation still doesn't work, though (at least on >>> my machine), and I don't understand the error messages that it >>> produces. Maybe it has something to do with the non-ascii unicode >>> characters in some of the files? >> >> I determined that the latex errors were due to the \uline command, >> which is defined in the "ulem" latex package. If I replace {\uline >> foo} with \underline{foo} throughout the sources, then the document >> generation works. However, I'm not sure whether the typesetting in the >> output is the same for the two commands. >> >> I assume Joachim tested the latex output before submitting the entry, >> so I wonder if my latex installation has a different version of the >> ulem package? If the document generation is sensitive to package >> versions, it might be a good idea to put a copy of ulem.sty in the >> document directory of the AFP entry. >> >> Also, it appears that the unicode apostrophes in the source files >> don't cause any latex errors, although they are silently omitted from >> the output. It would probably be a good idea to change them all to >> ordinary ascii apostrophes. >> >> - Brian > _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
