Email Gateway (Aug 18 2022 at 12:54): Email Gateway (Aug 18 2022 at 12:54):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
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.
Best and thanks for any hints,
Peter
Email Gateway (Aug 18 2022 at 12:54):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Peter,
One possible workaround would be to separate your assumptions using "and":
lemma
assumes "P x" and "f x"
However, if you are using named assumptions, this may cause problems.
For example, with
assumes A: "P x" "f x"
the local theorem "A" refers to the list of both assumptions, while with
assumes A: "P x" and "f x"
the local theorem "A" refers only to "P x".
Hope this helps,
Quoting Peter Lammich <peter.lammich@uni-muenster.de>:
Email Gateway (Aug 18 2022 at 12:54):From: Peter Lammich <peter.lammich@uni-muenster.de>
Brian Huffman wrote:
I am using named assumptions in most cases, I'm afraid, so this is
no option for me, as I would have to change too many existing proofs.
Moreover, I have a large base of existing proof scripts, so any
automatic solution with
as few changes to the scripts as possible would be the best.
Many thanks for the hint,
Peter
p.s. At this point, I'm thinking about running a script over my .thy -
files to put all those assumptions
in separate lines, each. However, I think, this will make the proofs
less readable in PG.
Email Gateway (Aug 18 2022 at 12:55):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 12:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
Makarius wrote:
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
Email Gateway (Aug 18 2022 at 12:55):From: Makarius <makarius@sketis.net>
Since the overall arrangement of the document sources is done in root.tex,
which is under your control, you can just place your modification there
after the initial \usepackage commands.
Makarius
Last updated: May 03 2024 at 08:18 UTC