1.1 --- a/NEWS Tue Jul 31 14:43:55 2012 +0200
1.2 +++ b/NEWS Tue Jul 31 19:55:04 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:43:55 2012 +0200
2.2 +++ b/doc-src/System/Thy/Presentation.thy Tue Jul 31 19:55:04 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:43:55 2012 +0200
3.2 +++ b/doc-src/System/Thy/document/Presentation.tex Tue Jul 31 19:55:04 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:43:55 2012 +0200
4.2 +++ b/lib/Tools/document Tue Jul 31 19:55:04 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"
5.1 --- a/src/HOL/ROOT Tue Jul 31 14:43:55 2012 +0200
5.2 +++ b/src/HOL/ROOT Tue Jul 31 19:55:04 2012 +0200
5.3 @@ -560,7 +560,7 @@
5.4 "document/root.tex"
5.5
5.6 session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
5.7 - options [condition = ISABELLE_POLYML, document_graph]
5.8 + options [document_graph]
5.9 theories [document = false]
5.10 "~~/src/HOL/Library/Countable"
5.11 "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
6.1 --- a/src/HOL/TPTP/mash_eval.ML Tue Jul 31 14:43:55 2012 +0200
6.2 +++ b/src/HOL/TPTP/mash_eval.ML Tue Jul 31 19:55:04 2012 +0200
6.3 @@ -46,7 +46,7 @@
6.4 val isar_ok = Unsynchronized.ref 0
6.5 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
6.6 fun index_string (j, s) = s ^ "@" ^ string_of_int j
6.7 - fun str_of_res label facts {outcome, run_time, used_facts, ...} =
6.8 + fun str_of_res label facts ({outcome, run_time, used_facts, ...}: Sledgehammer_Provers.prover_result) =
6.9 let val facts = facts |> map (fn ((name, _), _) => name ()) in
6.10 " " ^ label ^ ": " ^
6.11 (if is_none outcome then
7.1 --- a/src/Pure/System/build.scala Tue Jul 31 14:43:55 2012 +0200
7.2 +++ b/src/Pure/System/build.scala Tue Jul 31 19:55:04 2012 +0200
7.3 @@ -513,7 +513,7 @@
7.4 (output_dir + log_gz(name)).file.delete
7.5 File.write(output_dir + log(name), out)
7.6 echo(name + " FAILED")
7.7 - echo("(see also " + log(name).file.toString + ")")
7.8 + echo("(see also " + (output_dir + log(name)).file.toString + ")")
7.9 val lines = split_lines(out)
7.10 val tail = lines.drop(lines.length - 20 max 0)
7.11 echo("\n" + cat_lines(tail))