tuned terminology for document variants;
authorwenzelm
Sun Mar 20 18:09:32 2011 +0100 (2011-03-20)
changeset 42004e06351ffb475
parent 42003 6e45dc518ebb
child 42005 78bb3ec281c2
tuned terminology for document variants;
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Presentation.tex
lib/Tools/usedir
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/doc-src/System/Thy/Presentation.thy	Sun Mar 20 17:40:45 2011 +0100
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Sun Mar 20 18:09:32 2011 +0100
     1.3 @@ -448,7 +448,7 @@
     1.4      -P PATH      set path for remote theory browsing information
     1.5      -Q INT       set threshold for sub-proof parallelization (default 50)
     1.6      -T LEVEL     multithreading: trace level (default 0)
     1.7 -    -V VERSION   declare alternative document VERSION
     1.8 +    -V VARIANT   declare alternative document VARIANT
     1.9      -b           build mode (output heap image, using current dir)
    1.10      -d FORMAT    build document as FORMAT (default false)
    1.11      -f NAME      use ML file NAME (default ROOT.ML)
    1.12 @@ -523,16 +523,16 @@
    1.13    \secref{sec:tool-latex} for more details.
    1.14  
    1.15    \medskip The @{verbatim "-V"} option declares alternative document
    1.16 -  versions, consisting of name/tags pairs (cf.\ options @{verbatim
    1.17 +  variants, consisting of name/tags pairs (cf.\ options @{verbatim
    1.18    "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool).  The
    1.19    standard document is equivalent to ``@{verbatim
    1.20    "document=theory,proof,ML"}'', which means that all theory begin/end
    1.21    commands, proof body texts, and ML code will be presented
    1.22 -  faithfully.  An alternative version ``@{verbatim
    1.23 +  faithfully.  An alternative variant ``@{verbatim
    1.24    "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
    1.25    original text by a short place-holder.  The form ``@{text
    1.26    name}@{verbatim "=-"},'' means to remove document @{text name} from
    1.27 -  the list of versions to be processed.  Any number of @{verbatim
    1.28 +  the list of variants to be processed.  Any number of @{verbatim
    1.29    "-V"} options may be given; later declarations have precedence over
    1.30    earlier ones.
    1.31  
     2.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sun Mar 20 17:40:45 2011 +0100
     2.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Sun Mar 20 18:09:32 2011 +0100
     2.3 @@ -474,7 +474,7 @@
     2.4      -P PATH      set path for remote theory browsing information
     2.5      -Q INT       set threshold for sub-proof parallelization (default 50)
     2.6      -T LEVEL     multithreading: trace level (default 0)
     2.7 -    -V VERSION   declare alternative document VERSION
     2.8 +    -V VARIANT   declare alternative document VARIANT
     2.9      -b           build mode (output heap image, using current dir)
    2.10      -d FORMAT    build document as FORMAT (default false)
    2.11      -f NAME      use ML file NAME (default ROOT.ML)
    2.12 @@ -550,12 +550,12 @@
    2.13    \secref{sec:tool-latex} for more details.
    2.14  
    2.15    \medskip The \verb|-V| option declares alternative document
    2.16 -  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
    2.17 +  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
    2.18    standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
    2.19    commands, proof body texts, and ML code will be presented
    2.20 -  faithfully.  An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
    2.21 +  faithfully.  An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
    2.22    original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
    2.23 -  the list of versions to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
    2.24 +  the list of variants to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
    2.25    earlier ones.
    2.26  
    2.27    \medskip The \verb|-g| option produces images of the theory
     3.1 --- a/lib/Tools/usedir	Sun Mar 20 17:40:45 2011 +0100
     3.2 +++ b/lib/Tools/usedir	Sun Mar 20 18:09:32 2011 +0100
     3.3 @@ -21,7 +21,7 @@
     3.4    echo "    -P PATH      set path for remote theory browsing information"
     3.5    echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
     3.6    echo "    -T LEVEL     multithreading: trace level (default 0)"
     3.7 -  echo "    -V VERSION   declare alternative document VERSION"
     3.8 +  echo "    -V VARIANT   declare alternative document VARIANT"
     3.9    echo "    -b           build mode (output heap image, using current dir)"
    3.10    echo "    -d FORMAT    build document as FORMAT (default false)"
    3.11    echo "    -f NAME      use ML file NAME (default ROOT.ML)"
    3.12 @@ -74,7 +74,7 @@
    3.13  MAXTHREADS="1"
    3.14  RPATH=""
    3.15  TRACETHREADS="0"
    3.16 -DOCUMENT_VERSIONS=""
    3.17 +DOCUMENT_VARIANTS=""
    3.18  BUILD=""
    3.19  DOCUMENT=false
    3.20  ROOT_FILE="ROOT.ML"
    3.21 @@ -122,10 +122,10 @@
    3.22          TRACETHREADS="$OPTARG"
    3.23          ;;
    3.24        V)
    3.25 -        if [ -z "$DOCUMENT_VERSIONS" ]; then
    3.26 -          DOCUMENT_VERSIONS="\"$OPTARG\""
    3.27 +        if [ -z "$DOCUMENT_VARIANTS" ]; then
    3.28 +          DOCUMENT_VARIANTS="\"$OPTARG\""
    3.29          else
    3.30 -          DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
    3.31 +          DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
    3.32          fi
    3.33          ;;
    3.34        b)
    3.35 @@ -241,7 +241,7 @@
    3.36    LOG="$LOGDIR/$ITEM"
    3.37  
    3.38    "$ISABELLE_PROCESS" \
    3.39 -    -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;" \
    3.40 +    -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;" \
    3.41      -q -w $LOGIC $NAME > "$LOG"
    3.42    RC="$?"
    3.43  else
    3.44 @@ -250,7 +250,7 @@
    3.45    LOG="$LOGDIR/$ITEM"
    3.46  
    3.47    "$ISABELLE_PROCESS" \
    3.48 -    -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();" \
    3.49 +    -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();" \
    3.50      -r -q "$LOGIC" > "$LOG"
    3.51    RC="$?"
    3.52    cd ..
     4.1 --- a/src/Pure/System/session.ML	Sun Mar 20 17:40:45 2011 +0100
     4.2 +++ b/src/Pure/System/session.ML	Sun Mar 20 18:09:32 2011 +0100
     4.3 @@ -92,12 +92,12 @@
     4.4  fun dumping (_, "") = NONE
     4.5    | dumping (cp, path) = SOME (cp, Path.explode path);
     4.6  
     4.7 -fun use_dir item root build modes reset info doc doc_graph doc_versions parent
     4.8 +fun use_dir item root build modes reset info doc doc_graph doc_variants parent
     4.9      name dump rpath level timing verbose max_threads trace_threads
    4.10      parallel_proofs parallel_proofs_threshold =
    4.11    ((fn () =>
    4.12       (init reset parent name;
    4.13 -      Present.init build info doc doc_graph doc_versions (path ()) name
    4.14 +      Present.init build info doc doc_graph doc_variants (path ()) name
    4.15          (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
    4.16        if timing then
    4.17          let
     5.1 --- a/src/Pure/Thy/present.ML	Sun Mar 20 17:40:45 2011 +0100
     5.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 20 18:09:32 2011 +0100
     5.3 @@ -262,16 +262,16 @@
     5.4    | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
     5.5  
     5.6  
     5.7 -(* document versions *)
     5.8 +(* document variants *)
     5.9  
    5.10 -fun read_version str =
    5.11 +fun read_variant str =
    5.12    (case space_explode "=" str of
    5.13      [name] => (name, "")
    5.14    | [name, tags] => (name, tags)
    5.15 -  | _ => error ("Malformed document version specification: " ^ quote str));
    5.16 +  | _ => error ("Malformed document variant specification: " ^ quote str));
    5.17  
    5.18 -fun read_versions strs =
    5.19 -  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
    5.20 +fun read_variants strs =
    5.21 +  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
    5.22    |> filter_out (fn (_, s) => s = "-");
    5.23  
    5.24  
    5.25 @@ -279,7 +279,7 @@
    5.26  
    5.27  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    5.28  
    5.29 -fun init build info doc doc_graph doc_versions path name doc_prefix2
    5.30 +fun init build info doc doc_graph doc_variants path name doc_prefix2
    5.31      (remote_path, first_time) verbose thys = CRITICAL (fn () =>
    5.32    if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
    5.33      (browser_info := empty_browser_info; session_info := NONE)
    5.34 @@ -296,7 +296,7 @@
    5.35            (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
    5.36              (NONE, []))
    5.37          else (SOME (Path.append html_prefix document_path, html_prefix),
    5.38 -          read_versions doc_versions);
    5.39 +          read_variants doc_variants);
    5.40  
    5.41        val parent_index_path = Path.append Path.parent index_path;
    5.42        val index_up_lnk = if first_time then