[isabelle-dev] NEWS: Isabelle sessions and build management

Makarius makarius at sketis.net
Fri Aug 3 15:35:27 CEST 2012

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:

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
more conventional document setup, using inner document/IsaMakefile to do 
the patching;

Since IsaMakefiles are becoming extinct soon, I later refined it as 

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
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
simplified custom document/build script, instead of old-style 

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.


More information about the isabelle-dev mailing list