# HG changeset patch
# User wenzelm
# Date 1343757304 -7200
# Node ID 3ef76d545aafba4f19773dc7be51cf6661dc6afd
# Parent  77c416ef06fa3e48d3661427d2d25360fe4d6da3# Parent  ef374008cb7cf66334945328e36855a5bb2dc30f
merged

diff -r 77c416ef06fa -r 3ef76d545aaf NEWS
--- a/NEWS	Tue Jul 31 14:43:55 2012 +0200
+++ b/NEWS	Tue Jul 31 19:55:04 2012 +0200
@@ -65,6 +65,10 @@
 * Default for \<euro> is now based on eurosym package, instead of
 slightly exotic babel/greek.
 
+* Document variant NAME may use different LaTeX entry point
+document/root_NAME.tex if that file exists, instead of the common
+document/root.tex.
+
 
 *** System ***
 
diff -r 77c416ef06fa -r 3ef76d545aaf doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Tue Jul 31 14:43:55 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Tue Jul 31 19:55:04 2012 +0200
@@ -339,13 +339,19 @@
   document is equivalent to ``@{verbatim
   "document=theory,proof,ML"}'', which means that all theory begin/end
   commands, proof body texts, and ML code will be presented
-  faithfully.  An alternative variant ``@{verbatim
-  "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
-  original text by a short place-holder.  The form ``@{text
-  name}@{verbatim "=-"},'' means to remove document @{text name} from
-  the list of variants to be processed.  Any number of @{verbatim
-  "-V"} options may be given; later declarations have precedence over
-  earlier ones.
+  faithfully.
+
+  An alternative variant ``@{verbatim "outline=/proof/ML"}'' would
+  fold proof and ML parts, replacing the original text by a short
+  place-holder.  The form ``@{text name}@{verbatim "=-"},'' means to
+  remove document @{text name} from the list of variants to be
+  processed.  Any number of @{verbatim "-V"} options may be given;
+  later declarations have precedence over earlier ones.
+
+  Some document variant @{text name} may use an alternative {\LaTeX}
+  entry point called @{verbatim "document/root_"}@{text
+  "name"}@{verbatim ".tex"} if that file exists; otherwise the common
+  @{verbatim "document/root.tex"} is used.
 
   \medskip The @{verbatim "-g"} option produces images of the theory
   dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
diff -r 77c416ef06fa -r 3ef76d545aaf doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Tue Jul 31 14:43:55 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex	Tue Jul 31 19:55:04 2012 +0200
@@ -358,10 +358,18 @@
   variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}).  The standard
   document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
   commands, proof body texts, and ML code will be presented
-  faithfully.  An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
-  original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
-  the list of variants to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
-  earlier ones.
+  faithfully.
+
+  An alternative variant ``\verb|outline=/proof/ML|'' would
+  fold proof and ML parts, replacing the original text by a short
+  place-holder.  The form ``\isa{name}\verb|=-|,'' means to
+  remove document \isa{name} from the list of variants to be
+  processed.  Any number of \verb|-V| options may be given;
+  later declarations have precedence over earlier ones.
+
+  Some document variant \isa{name} may use an alternative {\LaTeX}
+  entry point called \verb|document/root_|\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|.tex| if that file exists; otherwise the common
+  \verb|document/root.tex| is used.
 
   \medskip The \verb|-g| option produces images of the theory
   dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
diff -r 77c416ef06fa -r 3ef76d545aaf lib/Tools/document
--- a/lib/Tools/document	Tue Jul 31 14:43:55 2012 +0200
+++ b/lib/Tools/document	Tue Jul 31 19:55:04 2012 +0200
@@ -85,7 +85,10 @@
 esac
 
 
-# tagged region markup
+# document variants
+
+ROOT_NAME="root_$NAME"
+[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
 
 function prep_tags ()
 {
@@ -117,10 +120,10 @@
 {
   local FMT="$1"
   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
-  "$ISABELLE_TOOL" latex -o sty && \
-  "$ISABELLE_TOOL" latex -o "$FMT" && \
-  { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
-  { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
+  "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
+  "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" && \
+  { [ ! -f root.bib -a ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
+  { [ ! -f root.idx -a ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
   "$ISABELLE_TOOL" latex -o "$FMT"
 }
 
@@ -136,16 +139,16 @@
     RC="$?"
   elif [ "$OUTFORMAT" = pdf ]; then
     pre_latex pdf && \
-    "$ISABELLE_TOOL" latex -o pdf
+    "$ISABELLE_TOOL" latex -o pdf "$ROOT_NAME.tex"
     RC="$?"
   else
     pre_latex dvi && \
-    "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
+    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
     RC="$?"
   fi
 
-  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
-    cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
+  if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
+    cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   fi
 
   exit "$RC"
diff -r 77c416ef06fa -r 3ef76d545aaf src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 31 14:43:55 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 31 19:55:04 2012 +0200
@@ -560,7 +560,7 @@
     "document/root.tex"
 
 session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
-  options [condition = ISABELLE_POLYML, document_graph]
+  options [document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
diff -r 77c416ef06fa -r 3ef76d545aaf src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Tue Jul 31 14:43:55 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Jul 31 19:55:04 2012 +0200
@@ -46,7 +46,7 @@
     val isar_ok = Unsynchronized.ref 0
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
-    fun str_of_res label facts {outcome, run_time, used_facts, ...} =
+    fun str_of_res label facts ({outcome, run_time, used_facts, ...}: Sledgehammer_Provers.prover_result) =
       let val facts = facts |> map (fn ((name, _), _) => name ()) in
         "  " ^ label ^ ": " ^
         (if is_none outcome then
diff -r 77c416ef06fa -r 3ef76d545aaf src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Jul 31 14:43:55 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 31 19:55:04 2012 +0200
@@ -513,7 +513,7 @@
               (output_dir + log_gz(name)).file.delete
               File.write(output_dir + log(name), out)
               echo(name + " FAILED")
-              echo("(see also " + log(name).file.toString + ")")
+              echo("(see also " + (output_dir + log(name)).file.toString + ")")
               val lines = split_lines(out)
               val tail = lines.drop(lines.length - 20 max 0)
               echo("\n" + cat_lines(tail))