# HG changeset patch
# User berghofe
# Date 934910640 -7200
# Node ID e077484d50d89a8297bbbe7e6da9ac242c4ee690
# Parent  3c3defaad8ae165de4e1229d295957919ffda0aa
Better handling of path for remote theory browsing information.

diff -r 3c3defaad8ae -r e077484d50d8 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue Aug 17 17:52:04 1999 +0200
+++ b/src/Pure/Isar/session.ML	Tue Aug 17 19:24:00 1999 +0200
@@ -23,6 +23,7 @@
 val session = ref ([pure]: string list);
 val session_path = ref ([]: string list);
 val session_finished = ref false;
+val rpath = ref (None : Url.T option);
 
 fun path () = ! session_path;
 
@@ -58,16 +59,17 @@
 
 val root_file = ThyLoad.ml_path "ROOT";
 
-val rpath = ref (None : Url.T option);
-
-fun use_dir reset info parent name rpath_str =
-  (init reset parent name;
-   if rpath_str = "" then () else
+fun get_rpath rpath_str =
+  (if rpath_str = "" then () else
      if is_some (!rpath) then
        error "Path for remote theory browsing information may only be set once"
      else
        rpath := Some (Url.unpack rpath_str);
-   Present.init info (path ()) name (!rpath);
+   (!rpath, rpath_str <> ""));
+
+fun use_dir reset info parent name rpath_str =
+  (init reset parent name;
+   Present.init info (path ()) name (get_rpath rpath_str);
    File.symbol_use root_file;
    finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
 
diff -r 3c3defaad8ae -r e077484d50d8 src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Tue Aug 17 17:52:04 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Tue Aug 17 19:24:00 1999 +0200
@@ -13,7 +13,7 @@
 signature BROWSER_INFO =
 sig
   include BASIC_BROWSER_INFO
-  val init: bool -> string list -> string -> Url.T option -> unit
+  val init: bool -> string list -> string -> Url.T option * bool -> unit
   val finish: unit -> unit
   val theory_source: string -> (string, 'a) Source.source -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
@@ -232,7 +232,7 @@
   else false;
 
 fun init false _ _ _ = (browser_info := empty_browser_info; session_info := None)
-  | init true path name remote_path =
+  | init true path name (remote_path, first_time) =
       let
         val parent_name = name_of_session (take (length path - 1, path));
         val session_name = name_of_session path;
@@ -256,7 +256,13 @@
           end;
         val opt_readme =
           (case prep_readme "README.html" of None => prep_readme "README" | some => some);
-        val index_text = HTML.begin_index (Url.file (Path.append Path.parent index_path), parent_name)
+
+        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_text = HTML.begin_index (index_up_lnk, parent_name)
           (Url.file index_path, session_name) (apsome Url.file opt_readme) graph_lnk;
       in
         File.mkdir (Path.append html_prefix session_path);