report path instead of actual session;
authorwenzelm
Wed, 10 Mar 1999 13:17:46 +0100
changeset 6341 3b0b5890e1f1
parent 6340 7d5cbd5819a0
child 6342 13424bbc2d8b
report path instead of actual session;
src/Pure/Thy/session.ML
--- a/src/Pure/Thy/session.ML	Wed Mar 10 10:55:12 1999 +0100
+++ b/src/Pure/Thy/session.ML	Wed Mar 10 13:17:46 1999 +0100
@@ -32,10 +32,10 @@
 
 (* diagnostics *)
 
-fun str_of [id] = id
-  | str_of ids = space_implode "/" (tl ids);
+fun str_of [] = "Pure"
+  | str_of elems = space_implode "/" elems;
 
-fun welcome () = "Welcome to Isabelle/" ^ str_of (! session) ^ " (" ^ version ^ ")";
+fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
 
 
 (* init *)
@@ -59,12 +59,10 @@
 val root_file = ThyLoad.ml_path "ROOT";
 
 fun use_dir reset info parent name =
-  let val parent_session = ! session in
-    init reset parent name;
-    Present.init info parent_session (! session) (path ()) name;
+  (init reset parent name;
+    Present.init info (path ()) name;
     Symbol.use root_file;
-    finish ()
-  end handle _ => exit 1;
+    finish ()) handle _ => exit 1;
 
 
 end;