# HG changeset patch
# User berghofe
# Date 934891230 -7200
# Node ID a8e86b8e6fd19a4aac63e5a4f67b7ee4d1e8136c
# Parent  1a4ed2eb48f35bb2393bc2cc69472e2ade7e5cb3
Path for remote theory browsing information is now stored in referece variable rpath.

diff -r 1a4ed2eb48f3 -r a8e86b8e6fd1 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue Aug 17 11:51:12 1999 +0200
+++ b/src/Pure/Isar/session.ML	Tue Aug 17 14:00:30 1999 +0200
@@ -58,11 +58,18 @@
 
 val root_file = ThyLoad.ml_path "ROOT";
 
-fun use_dir reset info parent name rpath =
+val rpath = ref (None : Url.T option);
+
+fun use_dir reset info parent name rpath_str =
   (init reset parent name;
-    Present.init info (path ()) name (if rpath = "" then None else Some (Url.unpack rpath));
-    File.symbol_use root_file;
-    finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
+   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);
+   File.symbol_use root_file;
+   finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
 
 
 end;