# HG changeset patch
# User wenzelm
# Date 920978038 -3600
# Node ID 1b55802e2b599fb2dbe3d5d48da40049b637ddb1
# Parent  2822885f5e02515eeb953aee6ca394790d081d6d
fixed add_path reset;
init / finish presentation;

diff -r 2822885f5e02 -r 1b55802e2b59 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;