fixed add_path reset;
authorwenzelm
Tue Mar 09 12:13:58 1999 +0100 (1999-03-09)
changeset 63261b55802e2b59
parent 6325 2822885f5e02
child 6327 c6abb5884fed
fixed add_path reset;
init / finish presentation;
src/Pure/Thy/session.ML
     1.1 --- a/src/Pure/Thy/session.ML	Tue Mar 09 12:13:11 1999 +0100
     1.2 +++ b/src/Pure/Thy/session.ML	Tue Mar 09 12:13:58 1999 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4  structure Session: SESSION =
     1.5  struct
     1.6  
     1.7 +
     1.8  (* session state *)
     1.9  
    1.10  val pure = "Pure";
    1.11 @@ -26,7 +27,7 @@
    1.12  fun path () = ! session_path;
    1.13  
    1.14  fun add_path reset s =
    1.15 -  (session := ! session @ [s]; session_path := (if reset then [] else ! session));
    1.16 +  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
    1.17  
    1.18  
    1.19  (* diagnostics *)
    1.20 @@ -47,7 +48,10 @@
    1.21  
    1.22  (* finish *)
    1.23  
    1.24 -fun finish () = (ThyInfo.finalize_all (); session_finished := true);
    1.25 +fun finish () =
    1.26 +  (ThyInfo.finalize_all ();
    1.27 +    Present.finish ();
    1.28 +    session_finished := true);
    1.29  
    1.30  
    1.31  (* use_dir *)
    1.32 @@ -56,7 +60,7 @@
    1.33  
    1.34  fun use_dir reset info parent name =
    1.35    (init reset parent name;
    1.36 -    Present.init info (! session) (path ()) parent name;
    1.37 +    Present.init info (str_of (! session)) (path ()) parent name;
    1.38      Symbol.use root_file;
    1.39      finish ())
    1.40    handle _ => exit 1;