fixed add_path reset;
authorwenzelm
Tue, 09 Mar 1999 12:13:58 +0100
changeset 6326 1b55802e2b59
parent 6325 2822885f5e02
child 6327 c6abb5884fed
fixed add_path reset; init / finish presentation;
src/Pure/Thy/session.ML
--- a/src/Pure/Thy/session.ML	Tue Mar 09 12:13:11 1999 +0100
+++ b/src/Pure/Thy/session.ML	Tue Mar 09 12:13:58 1999 +0100
@@ -15,6 +15,7 @@
 structure Session: SESSION =
 struct
 
+
 (* session state *)
 
 val pure = "Pure";
@@ -26,7 +27,7 @@
 fun path () = ! session_path;
 
 fun add_path reset s =
-  (session := ! session @ [s]; session_path := (if reset then [] else ! session));
+  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
 
 
 (* diagnostics *)
@@ -47,7 +48,10 @@
 
 (* finish *)
 
-fun finish () = (ThyInfo.finalize_all (); session_finished := true);
+fun finish () =
+  (ThyInfo.finalize_all ();
+    Present.finish ();
+    session_finished := true);
 
 
 (* use_dir *)
@@ -56,7 +60,7 @@
 
 fun use_dir reset info parent name =
   (init reset parent name;
-    Present.init info (! session) (path ()) parent name;
+    Present.init info (str_of (! session)) (path ()) parent name;
     Symbol.use root_file;
     finish ())
   handle _ => exit 1;