1.1 --- a/NEWS	Tue Jul 31 14:42:03 2012 +0200
     1.2 +++ b/NEWS	Tue Jul 31 16:23:20 2012 +0200
     1.3 @@ -65,6 +65,10 @@
     1.4  * Default for \<euro> is now based on eurosym package, instead of
     1.5  slightly exotic babel/greek.
     1.6  
     1.7 +* Document variant NAME may use different LaTeX entry point
     1.8 +document/root_NAME.tex if that file exists, instead of the common
     1.9 +document/root.tex.
    1.10 +
    1.11  
    1.12  *** System ***
    1.13  

     2.1 --- a/doc-src/System/Thy/Presentation.thy	Tue Jul 31 14:42:03 2012 +0200
     2.2 +++ b/doc-src/System/Thy/Presentation.thy	Tue Jul 31 16:23:20 2012 +0200
     2.3 @@ -339,13 +339,19 @@
     2.4    document is equivalent to ``@{verbatim
     2.5    "document=theory,proof,ML"}'', which means that all theory begin/end
     2.6    commands, proof body texts, and ML code will be presented
     2.7 -  faithfully.  An alternative variant ``@{verbatim
     2.8 -  "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
     2.9 -  original text by a short place-holder.  The form ``@{text
    2.10 -  name}@{verbatim "=-"},'' means to remove document @{text name} from
    2.11 -  the list of variants to be processed.  Any number of @{verbatim
    2.12 -  "-V"} options may be given; later declarations have precedence over
    2.13 -  earlier ones.
    2.14 +  faithfully.
    2.15 +
    2.16 +  An alternative variant ``@{verbatim "outline=/proof/ML"}'' would
    2.17 +  fold proof and ML parts, replacing the original text by a short
    2.18 +  place-holder.  The form ``@{text name}@{verbatim "=-"},'' means to
    2.19 +  remove document @{text name} from the list of variants to be
    2.20 +  processed.  Any number of @{verbatim "-V"} options may be given;
    2.21 +  later declarations have precedence over earlier ones.
    2.22 +
    2.23 +  Some document variant @{text name} may use an alternative {\LaTeX}
    2.24 +  entry point called @{verbatim "document/root_"}@{text
    2.25 +  "name"}@{verbatim ".tex"} if that file exists; otherwise the common
    2.26 +  @{verbatim "document/root.tex"} is used.
    2.27  
    2.28    \medskip The @{verbatim "-g"} option produces images of the theory
    2.29    dependency graph (cf.\ \secref{sec:browse}) for inclusion in the

     3.1 --- a/doc-src/System/Thy/document/Presentation.tex	Tue Jul 31 14:42:03 2012 +0200
     3.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Tue Jul 31 16:23:20 2012 +0200
     3.3 @@ -358,10 +358,18 @@
     3.4    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
     3.5    document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
     3.6    commands, proof body texts, and ML code will be presented
     3.7 -  faithfully.  An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
     3.8 -  original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
     3.9 -  the list of variants to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
    3.10 -  earlier ones.
    3.11 +  faithfully.
    3.12 +
    3.13 +  An alternative variant ``\verb|outline=/proof/ML|'' would
    3.14 +  fold proof and ML parts, replacing the original text by a short
    3.15 +  place-holder.  The form ``\isa{name}\verb|=-|,'' means to
    3.16 +  remove document \isa{name} from the list of variants to be
    3.17 +  processed.  Any number of \verb|-V| options may be given;
    3.18 +  later declarations have precedence over earlier ones.
    3.19 +
    3.20 +  Some document variant \isa{name} may use an alternative {\LaTeX}
    3.21 +  entry point called \verb|document/root_|\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|.tex| if that file exists; otherwise the common
    3.22 +  \verb|document/root.tex| is used.
    3.23  
    3.24    \medskip The \verb|-g| option produces images of the theory
    3.25    dependency graph (cf.\ \secref{sec:browse}) for inclusion in the

     4.1 --- a/lib/Tools/document	Tue Jul 31 14:42:03 2012 +0200
     4.2 +++ b/lib/Tools/document	Tue Jul 31 16:23:20 2012 +0200
     4.3 @@ -85,7 +85,10 @@
     4.4  esac
     4.5  
     4.6  
     4.7 -# tagged region markup
     4.8 +# document variants
     4.9 +
    4.10 +ROOT_NAME="root_$NAME"
    4.11 +[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
    4.12  
    4.13  function prep_tags ()
    4.14  {
    4.15 @@ -117,10 +120,10 @@
    4.16  {
    4.17    local FMT="$1"
    4.18    [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
    4.19 -  "$ISABELLE_TOOL" latex -o sty && \
    4.20 -  "$ISABELLE_TOOL" latex -o "$FMT" && \
    4.21 -  { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
    4.22 -  { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
    4.23 +  "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
    4.24 +  "$ISABELLE_TOOL" latex -o "$FMT" "$ROOT_NAME.tex" && \
    4.25 +  { [ ! -f root.bib -a ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
    4.26 +  { [ ! -f root.idx -a ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
    4.27    "$ISABELLE_TOOL" latex -o "$FMT"
    4.28  }
    4.29  
    4.30 @@ -136,16 +139,16 @@
    4.31      RC="$?"
    4.32    elif [ "$OUTFORMAT" = pdf ]; then
    4.33      pre_latex pdf && \
    4.34 -    "$ISABELLE_TOOL" latex -o pdf
    4.35 +    "$ISABELLE_TOOL" latex -o pdf "$ROOT_NAME.tex"
    4.36      RC="$?"
    4.37    else
    4.38      pre_latex dvi && \
    4.39 -    "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
    4.40 +    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
    4.41      RC="$?"
    4.42    fi
    4.43  
    4.44 -  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
    4.45 -    cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
    4.46 +  if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
    4.47 +    cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
    4.48    fi
    4.49  
    4.50    exit "$RC"