Re: [isabelle] documentation



Hi Stefania,

> $ /usr/local/Isabelle/bin/isatool usedir -v true -i true -d pdf HOL StefSession

> Running HOL-StefSession ...
> Browser info at /home/stefania/isabelle/browser_info/HOL/StefSession
> HOL-StefSession FAILED
> (see also /home/stefania/isabelle/heaps/Isabelle2008/polyml_x86-cygwin/log/HOL-S
> tefSession)
> 
> xmf/fonts/type1/bluesky/cm/cmsy10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/
> cmmi10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr10.pfb></usr/share/texmf
> /fonts/type1/bluesky/cm/cmti10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmb
> x10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmbx12.pfb></usr/share/texmf/f
> onts/type1/bluesky/cm/cmr12.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr17.
> pfb>
> Output written on root.pdf (266 pages, 859174 bytes).
> Transcript written on root.log.
> Document preparation failure in directory '/home/stefania/isabelle/browser_info/
> HOL/StefSession/document'
> *** No document: "/home/stefania/isabelle/browser_info/HOL/StefSession/document.
> pdf"

It is often difficult to extract a particular problem from the verbose
output of the tex-related processes.  Have you tried to inspect the log
file see also
/home/stefania/isabelle/heaps/Isabelle2008/polyml_x86-cygwin/log/HOL-StefSession?
 It seems that this contains important clues what actually went wrong.

> The second question i have is related with the keyword "includes"  that exists in the 2008 version but is not anymore in 2009. Does it have a replacement?

The "includes" feature was sacrificed in favour of a refined locale
implementation;  there is no one-to-one substitute.  In which context
does "inludes" appear in your theories?

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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