--- 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 ***
--- 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
--- 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
--- 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"
--- 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"
--- 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
--- 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))