# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1346185412 -3600
# Node ID 31d06b5cada480b380291073799c92f8ad719a0f
# Parent  5734ab5dd86d8a4f5aa49b769610258b3becd31b
added build for document

diff -r 5734ab5dd86d -r 31d06b5cada4 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Mon Aug 27 10:24:10 2012 +0100
+++ b/ProgTutorial/Intro.thy	Tue Aug 28 21:23:32 2012 +0100
@@ -27,7 +27,7 @@
   The best way to get to know the ML-level of Isabelle is by experimenting
   with the many code examples included in the tutorial. The code is as far as
   possible checked against the Isabelle
-  distribution.  %FIXME \footnote{\input{version}} 
+  distribution.\footnote{\input{version.tex}} 
   If something does not work, then
   please let us know. It is impossible for us to know every environment,
   operating system or editor in which Isabelle is used. If you have comments,
@@ -332,9 +332,8 @@
   with TBD.}
 
   \vfill
-  %% FIXME
-  %% This document (version \input{tip.tex}\hspace{-0.5ex}) was compiled with:\\
-  %% \input{version}\\
+  This document (version \input{tip.tex}\hspace{-0.5ex}) was compiled with:\\
+  \input{version.tex}\\
   %% \input{pversion}
 *}
 
diff -r 5734ab5dd86d -r 31d06b5cada4 ProgTutorial/document/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/document/build	Tue Aug 28 21:23:32 2012 +0100
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+hg parent --template '{date|shortdate}' > tip.tex
+
+"$ISABELLE_TOOL" version > version.tex
+
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o bbl
+makeindex -o root.stu root.str
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+mv root.pdf ../progtutorial.pdf
+
+
+#"$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"
+#$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated
+#	makeindex -o ProgTutorial/generated/root.stu ProgTutorial/generated/root.str 
\ No newline at end of file
diff -r 5734ab5dd86d -r 31d06b5cada4 ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ROOT	Tue Aug 28 21:23:32 2012 +0100
@@ -0,0 +1,37 @@
+
+session "Cookbook" in "ProgTutorial" = HOL +
+options [document = pdf, browser_info = false, document_output = ".."]
+  theories [document = false]
+    "Base"
+    "Package/Simple_Inductive_Package"
+    "~~/src/HOL/Number_Theory/Primes" 
+    "~~/src/HOL/Library/Efficient_Nat"
+    "Helper/Command/Command"
+  theories [quick_and_dirty, document = true] 
+    "Intro"
+    "First_Steps"
+    "Essential"
+    "Advanced"
+    "Parsing"
+    "Tactical"
+    "Package/Ind_Intro"
+    "Package/Ind_Prelims"
+    "Package/Ind_Interface"
+    "Package/Ind_General_Scheme"
+    "Package/Ind_Code" 
+    "Package/Ind_Extensions"
+    "Appendix"
+    "Recipes/Antiquotes"
+    "Recipes/TimeLimit"
+    "Recipes/Timing"
+    "Recipes/CallML"
+    "Recipes/ExternalSolver"
+    "Recipes/Oracle"
+    "Recipes/Sat"
+    "Recipes/USTypes"
+    "Solutions"
+  files 
+    "document/root.bib" 
+    "document/root.tex" 
+    "document/build"
+
diff -r 5734ab5dd86d -r 31d06b5cada4 progtutorial.pdf
Binary file progtutorial.pdf has changed