On Fri, 3 Aug 2012, Jasmin Christian Blanchette wrote:
For Huffman, the "fixdoc" script is not critical. It replaces 'a with
\alpha and things like that. I can live without it. But what do you mean
by "regular system functions"?
This is how I first did it:
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/d095ce0cdabf
user: wenzelm
date: Tue Jul 31 11:01:42 2012 +0200
files: .hgignore thys/Huffman/IsaMakefile
thys/Huffman/document/IsaMakefile thys/Huffman/document/fixdoc
thys/Huffman/document/isabelletags.sty thys/Huffman/fixdoc
description:
more conventional document setup, using inner document/IsaMakefile to do
the patching;
Since IsaMakefiles are becoming extinct soon, I later refined it as
follows:
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/293122866d12
tag: tip
user: wenzelm
date: Fri Aug 03 12:21:12 2012 +0200
files: thys/Huffman/ROOT thys/Huffman/document/IsaMakefile
thys/Huffman/document/build thys/Huffman/document/fixdoc thys/ROOT
description:
modernized document/build;
See also Isabelle/63ef2f0cf8bb:
user: wenzelm
date: Fri Aug 03 12:37:31 2012 +0200
files: NEWS doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Presentation.tex lib/Tools/document
description:
simplified custom document/build script, instead of old-style
document/IsaMakefile;
The latter also includes the updated documentation.
BTW, some of the perl substitions in Huffman/document/build no longer
work, because the format of the generated LaTeX has changed slightly over
the years.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
