src/Pure/Thy/present.ML
changeset 42004 e06351ffb475
parent 42003 6e45dc518ebb
child 42005 78bb3ec281c2
     1.1 --- a/src/Pure/Thy/present.ML	Sun Mar 20 17:40:45 2011 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 20 18:09:32 2011 +0100
     1.3 @@ -262,16 +262,16 @@
     1.4    | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
     1.5  
     1.6  
     1.7 -(* document versions *)
     1.8 +(* document variants *)
     1.9  
    1.10 -fun read_version str =
    1.11 +fun read_variant str =
    1.12    (case space_explode "=" str of
    1.13      [name] => (name, "")
    1.14    | [name, tags] => (name, tags)
    1.15 -  | _ => error ("Malformed document version specification: " ^ quote str));
    1.16 +  | _ => error ("Malformed document variant specification: " ^ quote str));
    1.17  
    1.18 -fun read_versions strs =
    1.19 -  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
    1.20 +fun read_variants strs =
    1.21 +  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
    1.22    |> filter_out (fn (_, s) => s = "-");
    1.23  
    1.24  
    1.25 @@ -279,7 +279,7 @@
    1.26  
    1.27  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    1.28  
    1.29 -fun init build info doc doc_graph doc_versions path name doc_prefix2
    1.30 +fun init build info doc doc_graph doc_variants path name doc_prefix2
    1.31      (remote_path, first_time) verbose thys = CRITICAL (fn () =>
    1.32    if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
    1.33      (browser_info := empty_browser_info; session_info := NONE)
    1.34 @@ -296,7 +296,7 @@
    1.35            (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
    1.36              (NONE, []))
    1.37          else (SOME (Path.append html_prefix document_path, html_prefix),
    1.38 -          read_versions doc_versions);
    1.39 +          read_variants doc_variants);
    1.40  
    1.41        val parent_index_path = Path.append Path.parent index_path;
    1.42        val index_up_lnk = if first_time then