# HG changeset patch
# User wenzelm
# Date 1363008314 -3600
# Node ID c3d02b3518c2afa9bedf00b2bf673bf7728b8ce6
# Parent  03b586ee5930d726ddb2b5af0b5670bbe58267cb
discontinued "isabelle usedir" option -P (remote path);

diff -r 03b586ee5930 -r c3d02b3518c2 NEWS
--- a/NEWS	Mon Mar 11 13:28:46 2013 +0100
+++ b/NEWS	Mon Mar 11 14:25:14 2013 +0100
@@ -61,6 +61,14 @@
       isar_shrink ~> isar_compress
 
 
+*** System ***
+
+* Discontinued "isabelle usedir" option -P (remote path).  Note that
+usedir is legacy and superseded by "isabelle build" since
+Isabelle2013.
+
+
+
 New in Isabelle2013 (February 2013)
 -----------------------------------
 
diff -r 03b586ee5930 -r c3d02b3518c2 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Mar 11 13:28:46 2013 +0100
+++ b/src/Pure/System/session.ML	Mon Mar 11 14:25:14 2013 +0100
@@ -12,7 +12,7 @@
   val welcome: unit -> string
   val finish: unit -> unit
   val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string -> string -> bool * string -> string -> bool -> unit
+    string -> string -> bool * string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
@@ -34,7 +34,6 @@
 (* access path *)
 
 val session_path = Unsynchronized.ref ([]: string list);
-val remote_path = Unsynchronized.ref (NONE: Url.T option);
 
 fun path () = ! session_path;
 
@@ -100,19 +99,11 @@
       else ();
   in y end;
 
-fun get_rpath rpath =
-  (if rpath = "" then () else
-     if is_some (! remote_path) then
-       error "Path for remote theory browsing information may only be set once"
-     else
-       remote_path := SOME (Url.explode rpath);
-   (! remote_path, rpath <> ""));
-
 fun init build reset info info_path doc doc_graph doc_output doc_variants
-    parent name doc_dump rpath verbose =
+    parent name doc_dump verbose =
  (init_name reset parent name;
   Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
-    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
+    doc_variants (path ()) name doc_dump verbose
     (map Thy_Info.get_theory (Thy_Info.get_names ())));
 
 local
@@ -132,8 +123,13 @@
         Output.physical_stderr
           "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
       val _ =
+        if rpath = "" then ()
+        else
+          Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
+
+      val _ =
         init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
-          doc_dump rpath verbose;
+          doc_dump verbose;
       val res1 = (use |> with_timing item timing |> Exn.capture) root;
       val res2 = Exn.capture finish ();
     in ignore (Par_Exn.release_all [res1, res2]) end)
diff -r 03b586ee5930 -r c3d02b3518c2 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Mar 11 13:28:46 2013 +0100
+++ b/src/Pure/Thy/present.ML	Mon Mar 11 14:25:14 2013 +0100
@@ -15,8 +15,7 @@
   val session_name: theory -> string
   val read_variant: string -> string * string
   val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string list -> string -> bool * string -> Url.T option * bool -> bool ->
-    theory list -> unit  (*not thread-safe!*)
+    string list -> string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit
   val theory_source: string -> (unit -> HTML.text) -> unit
@@ -51,8 +50,9 @@
 
 fun mk_rel_path [] ys = Path.make ys
   | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
-  | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
-      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
+  | mk_rel_path (ps as x :: xs) (qs as y :: ys) =
+      if x = y then mk_rel_path xs ys
+      else Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
 
 fun show_path path = Path.implode (Path.append (File.pwd ()) path);
 
@@ -62,8 +62,8 @@
 
 structure Browser_Info = Theory_Data
 (
-  type T = {name: string, session: string list, is_local: bool};
-  val empty = {name = "", session = [], is_local = false}: T;
+  type T = {name: string, session: string list};
+  val empty = {name = "", session = []}: T;
   fun extend _ = empty;
   fun merge _ = empty;
 );
@@ -81,17 +81,14 @@
 
 
 (*retrieve graph data from initial collection of theories*)
-fun init_graph remote_path curr_sess = rev o map (fn thy =>
+fun init_graph curr_sess = rev o map (fn thy =>
   let
     val name = Context.theory_name thy;
-    val {name = sess_name, session, is_local} = get_info thy;
+    val {name = sess_name, session} = get_info thy;
     val entry =
      {name = name, ID = ID_of session name, dir = sess_name,
       path =
-        if null session then "" else
-        if is_some remote_path andalso not is_local then
-          Url.implode (Url.append (the remote_path) (Url.File
-            (Path.append (Path.make session) (html_path name))))
+        if null session then ""
         else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
       unfold = false,
       parents = map ID_of_thy (Theory.parents_of thy),
@@ -130,8 +127,8 @@
 
 val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
 
-fun init_browser_info remote_path curr_sess thys = make_browser_info
-  (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
+fun init_browser_info curr_sess thys = make_browser_info
+  (Symtab.empty, [], [], [], init_graph curr_sess thys);
 
 fun map_browser_info f {theories, files, tex_index, html_index, graph} =
   make_browser_info (f (theories, files, tex_index, html_index, graph));
@@ -191,16 +188,16 @@
 type session_info =
   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
     info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
-    documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option,
-    verbose: bool, readme: Path.T option};
+    documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
+    readme: Path.T option};
 
 fun make_session_info
   (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
-    documents, doc_dump, remote_path, verbose, readme) =
+    documents, doc_dump, verbose, readme) =
   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
     info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
-    documents = documents, doc_dump = doc_dump, remote_path = remote_path,
-    verbose = verbose, readme = readme}: session_info;
+    documents = documents, doc_dump = doc_dump, verbose = verbose,
+    readme = readme}: session_info;
 
 
 (* state *)
@@ -251,7 +248,7 @@
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
 fun init build info info_path doc doc_graph document_output doc_variants path name
-    (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys =
+    (doc_dump as (_, dump_prefix)) verbose thys =
   if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
     (browser_info := empty_browser_info; session_info := NONE)
   else
@@ -270,10 +267,7 @@
         else doc_variants;
 
       val parent_index_path = Path.append Path.parent index_path;
-      val index_up_lnk =
-        if first_time then
-          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
-        else Url.File parent_index_path;
+      val index_up_lnk = Url.File parent_index_path;
       val readme =
         if File.exists readme_html_path then SOME readme_html_path
         else if File.exists readme_path then SOME readme_path
@@ -287,8 +281,8 @@
     in
       session_info :=
         SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
-          doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
-      browser_info := init_browser_info remote_path path thys;
+          doc_graph, doc_output, documents, doc_dump, verbose, readme));
+      browser_info := init_browser_info path thys;
       add_html_index (0, index_text)
     end;
 
@@ -439,24 +433,21 @@
   session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
 
 
-fun parent_link remote_path curr_session thy =
+fun parent_link curr_session thy =
   let
-    val {name = _, session, is_local} = get_info thy;
+    val {name = _, session} = get_info thy;
     val name = Context.theory_name thy;
     val link =
       if null session then NONE
-      else SOME
-       (if is_some remote_path andalso not is_local then
-         Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))
-        else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
+      else SOME (Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
   in (link, name) end;
 
 fun begin_theory update_time dir thy =
-    session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
+    session_default thy (fn {name = sess_name, session, path, html_prefix, ...} =>
   let
     val name = Context.theory_name thy;
     val parents = Theory.parents_of thy;
-    val parent_specs = map (parent_link remote_path path) parents;
+    val parent_specs = map (parent_link path) parents;
 
     val files = [];  (* FIXME *)
     val files_html = files |> map (fn (raw_path, loadit) =>
@@ -484,7 +475,7 @@
     add_graph_entry (update_time, entry);
     add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
     add_tex_index (update_time, Latex.theory_entry name);
-    put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
+    put_info {name = sess_name, session = path} thy
   end);
 
 
diff -r 03b586ee5930 -r c3d02b3518c2 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Mar 11 13:28:46 2013 +0100
+++ b/src/Pure/Tools/build.ML	Mon Mar 11 14:25:14 2013 +0100
@@ -136,7 +136,7 @@
           (Options.string options "document_output")
           document_variants
           parent_name name
-          (false, "") ""
+          (false, "")
           verbose;
 
       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);