# HG changeset patch
# User wenzelm
# Date 1343990251 -7200
# Node ID 63ef2f0cf8bb66074bc515c746b18cb9e24214c1
# Parent  5caa414ce9a24661824f3a5c90168f471f956e51
simplified custom document/build script, instead of old-style document/IsaMakefile;

diff -r 5caa414ce9a2 -r 63ef2f0cf8bb NEWS
--- a/NEWS	Fri Aug 03 09:51:28 2012 +0200
+++ b/NEWS	Fri Aug 03 12:37:31 2012 +0200
@@ -69,6 +69,9 @@
 document/root_NAME.tex if that file exists, instead of the common
 document/root.tex.
 
+* Simplified custom document/build script, instead of old-style
+document/IsaMakefile.  Minor INCOMPATIBILITY.
+
 
 *** System ***
 
diff -r 5caa414ce9a2 -r 63ef2f0cf8bb doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Fri Aug 03 09:51:28 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Fri Aug 03 12:37:31 2012 +0200
@@ -489,11 +489,13 @@
   and bibliographies (the latter assumes @{verbatim root.bib} within
   the same directory).
 
-  In more complex situations, a separate @{verbatim IsaMakefile} for
-  the document sources may be given instead.  This should provide
-  targets for any admissible document format; these have to produce
-  corresponding output files named after @{verbatim root} as well,
-  e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
+  In more complex situations, a separate @{verbatim build} script for
+  the document sources may be given.  It is invoked with command-line
+  arguments for the document format and the document variant name.
+  The script needs to produce corresponding output files, e.g.\
+  @{verbatim root.pdf} for target format @{verbatim pdf} (and default
+  default variants).  The main work can be again delegated to @{tool
+  latex}.
 
   \medskip When running the session, Isabelle copies the content of
   the original @{verbatim document} directory into its proper place
diff -r 5caa414ce9a2 -r 63ef2f0cf8bb doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Fri Aug 03 09:51:28 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex	Fri Aug 03 12:37:31 2012 +0200
@@ -500,11 +500,12 @@
   and bibliographies (the latter assumes \verb|root.bib| within
   the same directory).
 
-  In more complex situations, a separate \verb|IsaMakefile| for
-  the document sources may be given instead.  This should provide
-  targets for any admissible document format; these have to produce
-  corresponding output files named after \verb|root| as well,
-  e.g.\ \verb|root.dvi| for target format \verb|dvi|.
+  In more complex situations, a separate \verb|build| script for
+  the document sources may be given.  It is invoked with command-line
+  arguments for the document format and the document variant name.
+  The script needs to produce corresponding output files, e.g.\
+  \verb|root.pdf| for target format \verb|pdf| (and default
+  default variants).  The main work can be again delegated to \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}.
 
   \medskip When running the session, Isabelle copies the content of
   the original \verb|document| directory into its proper place
diff -r 5caa414ce9a2 -r 63ef2f0cf8bb lib/Tools/document
--- a/lib/Tools/document	Fri Aug 03 09:51:28 2012 +0200
+++ b/lib/Tools/document	Fri Aug 03 12:37:31 2012 +0200
@@ -134,8 +134,8 @@
 
   prep_tags
 
-  if [ -f IsaMakefile ]; then
-    "$ISABELLE_TOOL" make "$OUTFORMAT"
+  if [ -f build ]; then
+    ./build "$OUTFORMAT" "$NAME"
     RC="$?"
   elif [ "$OUTFORMAT" = pdf ]; then
     pre_latex pdf && \