Re: [isabelle] Isabelle document preparation



Makarius wrote:
On Thu, 22 Jan 2009, Peter Lammich wrote:

I have a problem with the latex-document generated by Isabelle.
   No space is put in between inner-syntax blocks, i.e. if I have the
following:

lemma
 assumes "P x" "f x"


it will look in latex like:
 lemma
   assumes P x f x

That can be very confusing! Is there some tuning option to put some extra space, or perhaps a ";\ \ " in between such lists. The only workaround I know up to now is to put each such inner-syntax block in its own line, what makes the proofs more unreadable at editing time.

The problem here is that the document preparation system does not really understand the structure of the text -- it is basically just a mock-up, but few people have noticed in the past decade :-)

There are some possibilities nonetheless:

(1) Write your sources with extra space between adjacent propositions, i.e. assumes "P x" "f x"; this is what I usually do, unless the exdplicit 'and' solution is possible.

(2) Use a LaTeX style that does not hide the quotes. This is just a matter of definining \isachardoublequoteopen and \isachardoublequoteclose in a suitable way; see the examples in isabelle.sty

Of course you can render the quotes in any way you see fit, e.g. funny parentheses.

(3) Run perl over the generated LaTeX sources to replace adjacent {\isachardoublequoteclose} and {\isachardoublequoteopen} -- a bit fragile, but often works for individual papers, theses etc. that are prepared with special care.


	Makarius
Thank you for the hints. I had a look at the generated tex-sources tonight, and finally
did an approach that is similar to the perl-script, but using tex.
I added to the root.tex, just after the style is defined:

% Tweaks
\newcounter{TTStweak_tag}
\setcounter{TTStweak_tag}{0}
\newcommand{\setTTS}{\setcounter{TTStweak_tag}{1}}
\newcommand{\resetTTS}{\setcounter{TTStweak_tag}{0}}
\newcommand{\insertTTS}{\ifnum\value{TTStweak_tag}=1 \ \ \ \fi}

\renewcommand{\isakeyword}[1]{\resetTTS\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\renewcommand{\isachardoublequoteopen}{\insertTTS}
\renewcommand{\isachardoublequoteclose}{\setTTS}
\renewcommand{\isanewline}{\mbox{}\par\mbox{}\resetTTS}

(Where TTStweak is just some arbitrarily chosen name without any meaning).

This works for now, however I'm not a tex-expert, and I think there should be nicer ways.

Probably, I could modify the sty - file directly, however I will have to figure out where I have to place the modified
isabelle.sty file, in order not to get overwritten by the make-script.

regards,
 Peter










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