# HG changeset patch
# User wenzelm
# Date 1346165027 -7200
# Node ID 5a4bcf46615679487e81918976b4e8309cc8287e
# Parent  8be091776e9310339f9ca396b290fb0a6a3a63fe
prepare document more uniformly;
fewer latex runs, in accordance to "isabelle document";
apply fixbookmarks last to operate on final root.out;

diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Classes/document/build
--- a/doc-src/Classes/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Classes/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -14,14 +14,5 @@
 cp "$ISABELLE_HOME/doc-src/proof.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Codegen/document/build
--- a/doc-src/Codegen/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Codegen/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -21,14 +21,5 @@
   $ISABELLE_EPSTOPDF "$NAME.eps"
 done
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Functions/document/build
--- a/doc-src/Functions/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Functions/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -10,12 +10,5 @@
 cp "$ISABELLE_HOME/doc-src/isar.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/HOL/document/build
--- a/doc-src/HOL/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/HOL/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -15,14 +15,5 @@
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Intro/document/build
--- a/doc-src/Intro/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Intro/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -14,14 +14,5 @@
 cp "$ISABELLE_HOME/doc-src/proof.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/IsarImplementation/document/build
--- a/doc-src/IsarImplementation/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/IsarImplementation/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -16,14 +16,5 @@
 cp "$ISABELLE_HOME/doc-src/underscore.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/IsarRef/document/build
--- a/doc-src/IsarRef/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/IsarRef/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -18,14 +18,5 @@
 
 ./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/LaTeXsugar/document/build
--- a/doc-src/LaTeXsugar/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/LaTeXsugar/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -5,14 +5,5 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Locales/document/build
--- a/doc-src/Locales/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Locales/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -5,14 +5,5 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Logics/document/build
--- a/doc-src/Logics/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Logics/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -14,14 +14,5 @@
 cp "$ISABELLE_HOME/doc-src/proof.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Nitpick/document/build
--- a/doc-src/Nitpick/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Nitpick/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -11,14 +11,5 @@
 cp "$ISABELLE_HOME/doc-src/iman.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/ProgProve/document/build
--- a/doc-src/ProgProve/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/ProgProve/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -10,13 +10,5 @@
 
 cp "$ISABELLE_HOME/doc-src/ProgProve/MyList.thy" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/ROOT
--- a/doc-src/ROOT	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/ROOT	Tue Aug 28 16:43:47 2012 +0200
@@ -3,6 +3,7 @@
   theories [document = false] Setup
   theories Classes
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "document/build"
     "document/root.tex"
@@ -20,6 +21,7 @@
     Adaptation
     Further
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "document/adapt.tex"
     "document/architecture.tex"
@@ -31,6 +33,7 @@
   options [document_variants = "functions"]
   theories Functions
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -47,6 +50,7 @@
   options [document_variants = "intro"]
   theories
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -70,6 +74,7 @@
     Syntax
     Tactic
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -101,6 +106,7 @@
     Symbols
     ML_Tactic
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -123,6 +129,7 @@
     "~~/src/HOL/Library/OptionalSugar"
   theories Sugar
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "document/build"
     "document/mathpartir.sty"
@@ -136,6 +143,7 @@
     Examples2
     Examples3
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "document/build"
     "document/root.tex"
@@ -144,6 +152,7 @@
   options [document_variants = "logics"]
   theories
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -157,6 +166,7 @@
   options [document_variants = "logics-HOL"]
   theories
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -177,6 +187,7 @@
     If
     ZF_Isar
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../isar.sty"
     "../ttbox.sty"
@@ -190,6 +201,7 @@
   options [document_variants = "main"]
   theories Main_Doc
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "document/build"
     "document/root.tex"
@@ -198,6 +210,7 @@
   options [document_variants = "nitpick"]
   theories
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../manual.bib"
@@ -214,6 +227,7 @@
     Logic
     Isar
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "document/bang.eps"
     "document/bang.pdf"
@@ -229,6 +243,7 @@
   options [document_variants = "ref"]
   theories
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../extra.sty"
@@ -248,6 +263,7 @@
   options [document_variants = "sledgehammer"]
   theories
   files
+    "../prepare_document"
     "../pdfsetup.sty"
     "../iman.sty"
     "../manual.bib"
@@ -264,6 +280,7 @@
     Scala
     Misc
   files
+    "../prepare_document"
     "../IsarRef/document/style.sty"
     "../pdfsetup.sty"
     "../iman.sty"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Ref/document/build
--- a/doc-src/Ref/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Ref/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -14,14 +14,5 @@
 cp "$ISABELLE_HOME/doc-src/proof.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/Sledgehammer/document/build
--- a/doc-src/Sledgehammer/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/Sledgehammer/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -11,14 +11,5 @@
 cp "$ISABELLE_HOME/doc-src/iman.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/System/document/build
--- a/doc-src/System/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/System/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -16,14 +16,5 @@
 cp "$ISABELLE_HOME/doc-src/underscore.sty" .
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/TutorialI/document/build
--- a/doc-src/TutorialI/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/TutorialI/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -20,9 +20,7 @@
 
 "$ISABELLE_TOOL" latex -o "$FORMAT"
 "$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+./isa-index root
 "$ISABELLE_TOOL" latex -o "$FORMAT"
-./isa-index root
 [ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
 "$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/ZF/document/build
--- a/doc-src/ZF/document/build	Tue Aug 28 16:18:23 2012 +0200
+++ b/doc-src/ZF/document/build	Tue Aug 28 16:43:47 2012 +0200
@@ -14,14 +14,5 @@
 cp "$ISABELLE_HOME/doc-src/manual.bib" .
 cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" .
 
-"$ISABELLE_TOOL" latex -o sty
-cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_HOME/doc-src/sedindex" root
-[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
diff -r 8be091776e93 -r 5a4bcf466156 doc-src/prepare_document
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/prepare_document	Tue Aug 28 16:43:47 2012 +0200
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+
+"$ISABELLE_TOOL" latex -o sty
+cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
+
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o bbl
+[ -f root.idx ] && "$ISABELLE_HOME/doc-src/sedindex" root
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+