document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;

--- a/NEWS	Tue Jul 31 14:42:03 2012 +0200
+++ b/NEWS	Tue Jul 31 16:23:20 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 ***
 

--- a/doc-src/System/Thy/Presentation.thy	Tue Jul 31 14:42:03 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Tue Jul 31 16:23:20 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

--- a/doc-src/System/Thy/document/Presentation.tex	Tue Jul 31 14:42:03 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex	Tue Jul 31 16:23:20 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

--- a/lib/Tools/document	Tue Jul 31 14:42:03 2012 +0200
+++ b/lib/Tools/document	Tue Jul 31 16:23:20 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"