--- a/doc-src/System/Thy/Presentation.thy Sun Mar 20 17:40:45 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy Sun Mar 20 18:09:32 2011 +0100
@@ -448,7 +448,7 @@
-P PATH set path for remote theory browsing information
-Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
- -V VERSION declare alternative document VERSION
+ -V VARIANT declare alternative document VARIANT
-b build mode (output heap image, using current dir)
-d FORMAT build document as FORMAT (default false)
-f NAME use ML file NAME (default ROOT.ML)
@@ -523,16 +523,16 @@
\secref{sec:tool-latex} for more details.
\medskip The @{verbatim "-V"} option declares alternative document
- versions, consisting of name/tags pairs (cf.\ options @{verbatim
+ variants, consisting of name/tags pairs (cf.\ options @{verbatim
"-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The
standard 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 version ``@{verbatim
+ 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 versions to be processed. Any number of @{verbatim
+ the list of variants to be processed. Any number of @{verbatim
"-V"} options may be given; later declarations have precedence over
earlier ones.
--- a/doc-src/System/Thy/document/Presentation.tex Sun Mar 20 17:40:45 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Sun Mar 20 18:09:32 2011 +0100
@@ -474,7 +474,7 @@
-P PATH set path for remote theory browsing information
-Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
- -V VERSION declare alternative document VERSION
+ -V VARIANT declare alternative document VARIANT
-b build mode (output heap image, using current dir)
-d FORMAT build document as FORMAT (default false)
-f NAME use ML file NAME (default ROOT.ML)
@@ -550,12 +550,12 @@
\secref{sec:tool-latex} for more details.
\medskip The \verb|-V| option declares alternative document
- versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). The
+ variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). 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 version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
+ 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 versions to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over
+ the list of variants to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over
earlier ones.
\medskip The \verb|-g| option produces images of the theory
--- a/lib/Tools/usedir Sun Mar 20 17:40:45 2011 +0100
+++ b/lib/Tools/usedir Sun Mar 20 18:09:32 2011 +0100
@@ -21,7 +21,7 @@
echo " -P PATH set path for remote theory browsing information"
echo " -Q INT set threshold for sub-proof parallelization (default 100)"
echo " -T LEVEL multithreading: trace level (default 0)"
- echo " -V VERSION declare alternative document VERSION"
+ echo " -V VARIANT declare alternative document VARIANT"
echo " -b build mode (output heap image, using current dir)"
echo " -d FORMAT build document as FORMAT (default false)"
echo " -f NAME use ML file NAME (default ROOT.ML)"
@@ -74,7 +74,7 @@
MAXTHREADS="1"
RPATH=""
TRACETHREADS="0"
-DOCUMENT_VERSIONS=""
+DOCUMENT_VARIANTS=""
BUILD=""
DOCUMENT=false
ROOT_FILE="ROOT.ML"
@@ -122,10 +122,10 @@
TRACETHREADS="$OPTARG"
;;
V)
- if [ -z "$DOCUMENT_VERSIONS" ]; then
- DOCUMENT_VERSIONS="\"$OPTARG\""
+ if [ -z "$DOCUMENT_VARIANTS" ]; then
+ DOCUMENT_VARIANTS="\"$OPTARG\""
else
- DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
+ DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
fi
;;
b)
@@ -241,7 +241,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
-q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -250,7 +250,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/src/Pure/System/session.ML Sun Mar 20 17:40:45 2011 +0100
+++ b/src/Pure/System/session.ML Sun Mar 20 18:09:32 2011 +0100
@@ -92,12 +92,12 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
-fun use_dir item root build modes reset info doc doc_graph doc_versions parent
+fun use_dir item root build modes reset info doc doc_graph doc_variants parent
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
(init reset parent name;
- Present.init build info doc doc_graph doc_versions (path ()) name
+ Present.init build info doc doc_graph doc_variants (path ()) name
(dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
if timing then
let
--- a/src/Pure/Thy/present.ML Sun Mar 20 17:40:45 2011 +0100
+++ b/src/Pure/Thy/present.ML Sun Mar 20 18:09:32 2011 +0100
@@ -262,16 +262,16 @@
| SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
-(* document versions *)
+(* document variants *)
-fun read_version str =
+fun read_variant str =
(case space_explode "=" str of
[name] => (name, "")
| [name, tags] => (name, tags)
- | _ => error ("Malformed document version specification: " ^ quote str));
+ | _ => error ("Malformed document variant specification: " ^ quote str));
-fun read_versions strs =
- rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
+fun read_variants strs =
+ rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
|> filter_out (fn (_, s) => s = "-");
@@ -279,7 +279,7 @@
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
-fun init build info doc doc_graph doc_versions path name doc_prefix2
+fun init build info doc doc_graph doc_variants path name doc_prefix2
(remote_path, first_time) verbose thys = CRITICAL (fn () =>
if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
(browser_info := empty_browser_info; session_info := NONE)
@@ -296,7 +296,7 @@
(if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
(NONE, []))
else (SOME (Path.append html_prefix document_path, html_prefix),
- read_versions doc_versions);
+ read_variants doc_variants);
val parent_index_path = Path.append Path.parent index_path;
val index_up_lnk = if first_time then