Re: [isabelle] Isabelle document preparation



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





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