# HG changeset patch
# User wenzelm
# Date 1300640972 -3600
# Node ID e06351ffb475825792d2f190385c0282ee0f66b4
# Parent  6e45dc518ebb513054b28d34b694ad06d5303313
tuned terminology for document variants;

diff -r 6e45dc518ebb -r e06351ffb475 doc-src/System/Thy/Presentation.thy
--- 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.
 
diff -r 6e45dc518ebb -r e06351ffb475 doc-src/System/Thy/document/Presentation.tex
--- 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
diff -r 6e45dc518ebb -r e06351ffb475 lib/Tools/usedir
--- 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 ..
diff -r 6e45dc518ebb -r e06351ffb475 src/Pure/System/session.ML
--- 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
diff -r 6e45dc518ebb -r e06351ffb475 src/Pure/Thy/present.ML
--- 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