Path for remote theory browsing information is now stored in referece variable rpath.
authorberghofe
Tue, 17 Aug 1999 14:00:30 +0200
changeset 7227 a8e86b8e6fd1
parent 7226 1a4ed2eb48f3
child 7228 ddb67dcf026c
Path for remote theory browsing information is now stored in referece variable rpath.
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;