discontinued "isabelle usedir" option -P (remote path);
authorwenzelm
Mon Mar 11 14:25:14 2013 +0100 (2013-03-11)
changeset 51398c3d02b3518c2
parent 51397 03b586ee5930
child 51399 6ac3c29a300e
discontinued "isabelle usedir" option -P (remote path);
NEWS
src/Pure/System/session.ML
src/Pure/Thy/present.ML
src/Pure/Tools/build.ML
     1.1 --- a/NEWS	Mon Mar 11 13:28:46 2013 +0100
     1.2 +++ b/NEWS	Mon Mar 11 14:25:14 2013 +0100
     1.3 @@ -61,6 +61,14 @@
     1.4        isar_shrink ~> isar_compress
     1.5  
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* Discontinued "isabelle usedir" option -P (remote path).  Note that
    1.10 +usedir is legacy and superseded by "isabelle build" since
    1.11 +Isabelle2013.
    1.12 +
    1.13 +
    1.14 +
    1.15  New in Isabelle2013 (February 2013)
    1.16  -----------------------------------
    1.17  
     2.1 --- a/src/Pure/System/session.ML	Mon Mar 11 13:28:46 2013 +0100
     2.2 +++ b/src/Pure/System/session.ML	Mon Mar 11 14:25:14 2013 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4    val welcome: unit -> string
     2.5    val finish: unit -> unit
     2.6    val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     2.7 -    string -> string -> bool * string -> string -> bool -> unit
     2.8 +    string -> string -> bool * string -> bool -> unit
     2.9    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    2.10    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    2.11      string -> bool -> string list -> string -> string -> bool * string ->
    2.12 @@ -34,7 +34,6 @@
    2.13  (* access path *)
    2.14  
    2.15  val session_path = Unsynchronized.ref ([]: string list);
    2.16 -val remote_path = Unsynchronized.ref (NONE: Url.T option);
    2.17  
    2.18  fun path () = ! session_path;
    2.19  
    2.20 @@ -100,19 +99,11 @@
    2.21        else ();
    2.22    in y end;
    2.23  
    2.24 -fun get_rpath rpath =
    2.25 -  (if rpath = "" then () else
    2.26 -     if is_some (! remote_path) then
    2.27 -       error "Path for remote theory browsing information may only be set once"
    2.28 -     else
    2.29 -       remote_path := SOME (Url.explode rpath);
    2.30 -   (! remote_path, rpath <> ""));
    2.31 -
    2.32  fun init build reset info info_path doc doc_graph doc_output doc_variants
    2.33 -    parent name doc_dump rpath verbose =
    2.34 +    parent name doc_dump verbose =
    2.35   (init_name reset parent name;
    2.36    Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
    2.37 -    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
    2.38 +    doc_variants (path ()) name doc_dump verbose
    2.39      (map Thy_Info.get_theory (Thy_Info.get_names ())));
    2.40  
    2.41  local
    2.42 @@ -132,8 +123,13 @@
    2.43          Output.physical_stderr
    2.44            "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
    2.45        val _ =
    2.46 +        if rpath = "" then ()
    2.47 +        else
    2.48 +          Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
    2.49 +
    2.50 +      val _ =
    2.51          init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
    2.52 -          doc_dump rpath verbose;
    2.53 +          doc_dump verbose;
    2.54        val res1 = (use |> with_timing item timing |> Exn.capture) root;
    2.55        val res2 = Exn.capture finish ();
    2.56      in ignore (Par_Exn.release_all [res1, res2]) end)
     3.1 --- a/src/Pure/Thy/present.ML	Mon Mar 11 13:28:46 2013 +0100
     3.2 +++ b/src/Pure/Thy/present.ML	Mon Mar 11 14:25:14 2013 +0100
     3.3 @@ -15,8 +15,7 @@
     3.4    val session_name: theory -> string
     3.5    val read_variant: string -> string * string
     3.6    val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     3.7 -    string list -> string -> bool * string -> Url.T option * bool -> bool ->
     3.8 -    theory list -> unit  (*not thread-safe!*)
     3.9 +    string list -> string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
    3.10    val finish: unit -> unit  (*not thread-safe!*)
    3.11    val init_theory: string -> unit
    3.12    val theory_source: string -> (unit -> HTML.text) -> unit
    3.13 @@ -51,8 +50,9 @@
    3.14  
    3.15  fun mk_rel_path [] ys = Path.make ys
    3.16    | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
    3.17 -  | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
    3.18 -      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
    3.19 +  | mk_rel_path (ps as x :: xs) (qs as y :: ys) =
    3.20 +      if x = y then mk_rel_path xs ys
    3.21 +      else Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
    3.22  
    3.23  fun show_path path = Path.implode (Path.append (File.pwd ()) path);
    3.24  
    3.25 @@ -62,8 +62,8 @@
    3.26  
    3.27  structure Browser_Info = Theory_Data
    3.28  (
    3.29 -  type T = {name: string, session: string list, is_local: bool};
    3.30 -  val empty = {name = "", session = [], is_local = false}: T;
    3.31 +  type T = {name: string, session: string list};
    3.32 +  val empty = {name = "", session = []}: T;
    3.33    fun extend _ = empty;
    3.34    fun merge _ = empty;
    3.35  );
    3.36 @@ -81,17 +81,14 @@
    3.37  
    3.38  
    3.39  (*retrieve graph data from initial collection of theories*)
    3.40 -fun init_graph remote_path curr_sess = rev o map (fn thy =>
    3.41 +fun init_graph curr_sess = rev o map (fn thy =>
    3.42    let
    3.43      val name = Context.theory_name thy;
    3.44 -    val {name = sess_name, session, is_local} = get_info thy;
    3.45 +    val {name = sess_name, session} = get_info thy;
    3.46      val entry =
    3.47       {name = name, ID = ID_of session name, dir = sess_name,
    3.48        path =
    3.49 -        if null session then "" else
    3.50 -        if is_some remote_path andalso not is_local then
    3.51 -          Url.implode (Url.append (the remote_path) (Url.File
    3.52 -            (Path.append (Path.make session) (html_path name))))
    3.53 +        if null session then ""
    3.54          else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
    3.55        unfold = false,
    3.56        parents = map ID_of_thy (Theory.parents_of thy),
    3.57 @@ -130,8 +127,8 @@
    3.58  
    3.59  val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
    3.60  
    3.61 -fun init_browser_info remote_path curr_sess thys = make_browser_info
    3.62 -  (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
    3.63 +fun init_browser_info curr_sess thys = make_browser_info
    3.64 +  (Symtab.empty, [], [], [], init_graph curr_sess thys);
    3.65  
    3.66  fun map_browser_info f {theories, files, tex_index, html_index, graph} =
    3.67    make_browser_info (f (theories, files, tex_index, html_index, graph));
    3.68 @@ -191,16 +188,16 @@
    3.69  type session_info =
    3.70    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    3.71      info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
    3.72 -    documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option,
    3.73 -    verbose: bool, readme: Path.T option};
    3.74 +    documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
    3.75 +    readme: Path.T option};
    3.76  
    3.77  fun make_session_info
    3.78    (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
    3.79 -    documents, doc_dump, remote_path, verbose, readme) =
    3.80 +    documents, doc_dump, verbose, readme) =
    3.81    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
    3.82      info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    3.83 -    documents = documents, doc_dump = doc_dump, remote_path = remote_path,
    3.84 -    verbose = verbose, readme = readme}: session_info;
    3.85 +    documents = documents, doc_dump = doc_dump, verbose = verbose,
    3.86 +    readme = readme}: session_info;
    3.87  
    3.88  
    3.89  (* state *)
    3.90 @@ -251,7 +248,7 @@
    3.91  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    3.92  
    3.93  fun init build info info_path doc doc_graph document_output doc_variants path name
    3.94 -    (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys =
    3.95 +    (doc_dump as (_, dump_prefix)) verbose thys =
    3.96    if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
    3.97      (browser_info := empty_browser_info; session_info := NONE)
    3.98    else
    3.99 @@ -270,10 +267,7 @@
   3.100          else doc_variants;
   3.101  
   3.102        val parent_index_path = Path.append Path.parent index_path;
   3.103 -      val index_up_lnk =
   3.104 -        if first_time then
   3.105 -          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
   3.106 -        else Url.File parent_index_path;
   3.107 +      val index_up_lnk = Url.File parent_index_path;
   3.108        val readme =
   3.109          if File.exists readme_html_path then SOME readme_html_path
   3.110          else if File.exists readme_path then SOME readme_path
   3.111 @@ -287,8 +281,8 @@
   3.112      in
   3.113        session_info :=
   3.114          SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
   3.115 -          doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
   3.116 -      browser_info := init_browser_info remote_path path thys;
   3.117 +          doc_graph, doc_output, documents, doc_dump, verbose, readme));
   3.118 +      browser_info := init_browser_info path thys;
   3.119        add_html_index (0, index_text)
   3.120      end;
   3.121  
   3.122 @@ -439,24 +433,21 @@
   3.123    session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
   3.124  
   3.125  
   3.126 -fun parent_link remote_path curr_session thy =
   3.127 +fun parent_link curr_session thy =
   3.128    let
   3.129 -    val {name = _, session, is_local} = get_info thy;
   3.130 +    val {name = _, session} = get_info thy;
   3.131      val name = Context.theory_name thy;
   3.132      val link =
   3.133        if null session then NONE
   3.134 -      else SOME
   3.135 -       (if is_some remote_path andalso not is_local then
   3.136 -         Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))
   3.137 -        else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
   3.138 +      else SOME (Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
   3.139    in (link, name) end;
   3.140  
   3.141  fun begin_theory update_time dir thy =
   3.142 -    session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   3.143 +    session_default thy (fn {name = sess_name, session, path, html_prefix, ...} =>
   3.144    let
   3.145      val name = Context.theory_name thy;
   3.146      val parents = Theory.parents_of thy;
   3.147 -    val parent_specs = map (parent_link remote_path path) parents;
   3.148 +    val parent_specs = map (parent_link path) parents;
   3.149  
   3.150      val files = [];  (* FIXME *)
   3.151      val files_html = files |> map (fn (raw_path, loadit) =>
   3.152 @@ -484,7 +475,7 @@
   3.153      add_graph_entry (update_time, entry);
   3.154      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
   3.155      add_tex_index (update_time, Latex.theory_entry name);
   3.156 -    put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
   3.157 +    put_info {name = sess_name, session = path} thy
   3.158    end);
   3.159  
   3.160  
     4.1 --- a/src/Pure/Tools/build.ML	Mon Mar 11 13:28:46 2013 +0100
     4.2 +++ b/src/Pure/Tools/build.ML	Mon Mar 11 14:25:14 2013 +0100
     4.3 @@ -136,7 +136,7 @@
     4.4            (Options.string options "document_output")
     4.5            document_variants
     4.6            parent_name name
     4.7 -          (false, "") ""
     4.8 +          (false, "")
     4.9            verbose;
    4.10  
    4.11        val last_timing = lookup_timings (fold update_timings command_timings empty_timings);