Email Gateway (Aug 18 2022 at 11:46): Email Gateway (Aug 18 2022 at 11:46):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I'm trying to use the isatool document preparation system in
conjunction with the LNCS LaTeX class file. When I use a normal
"article" class file, the build works fine, and produces the correct
document with no errors. When I change to \documentclass{llncs} and
try the same thing, I get 100+ fatal errors, each of which is
! Paragraph ended before \def was complete.
<to be read again>
\par
l.57
(That makes 100 errors; please try again.)
! ==> Fatal error occurred, no output PDF file produced!
Transcript written on root.log.
Now, I have found the \def command to which this error refers (l.57 is
just a blank line), and it is in the .tex file created by the
combination of the Isabelle markup and LaTeX markup in my .thy file.
Specifically, it is this line
%
\begin{isabellebody}%
\def\isabellecontext{Craignd}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
(my bold) which is right at the top of the file. Has anyone come
across this problem before when trying to combine an Isabelle build
with the LNCS class file? Or does anyone know how to fix it?
If it helps, here is the class file
Many thanks
Peter
Email Gateway (Aug 18 2022 at 11:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Peter,
I have never encountered a similar problem (using LLNCS DOCUMENT CLASS
-- version 2.14 (17-Aug-2004)).
I dont't think that the problem is in this \def -- maybe it is a strange
interference between different parts of the TeX soup. Perhaps some
changes / deletetions in the generated TeX (directory generated/) may
yield a more precise error description.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 11:46):From: Tobias Nipkow <nipkow@in.tum.de>
I am doing this all the time (incl yesterday). If I had a problem at
some point, I have forgotten. I just checked, I am using the latest
llncs.cls (which seems not to have changed in a while). I have appended
how my roo.tex starts.
Sorry not to be of more help,
Tobias
\documentclass[envcountsame]{llncs}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage[latin1]{inputenc}
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\pagestyle{plain}
\title{Linear Quantifier Elimination}
\author{Tobias Nipkow}
\authorrunning{T. Nipkow}
\institute{Institut fr Informatik, Technische Universitt Mnchen}
\date{}
\maketitle
...
\input{session}
Peter Chapman wrote:
Last updated: May 03 2024 at 01:09 UTC