report path instead of actual session;
authorwenzelm
Wed Mar 10 13:17:46 1999 +0100 (1999-03-10)
changeset 63413b0b5890e1f1
parent 6340 7d5cbd5819a0
child 6342 13424bbc2d8b
report path instead of actual session;
src/Pure/Thy/session.ML
     1.1 --- a/src/Pure/Thy/session.ML	Wed Mar 10 10:55:12 1999 +0100
     1.2 +++ b/src/Pure/Thy/session.ML	Wed Mar 10 13:17:46 1999 +0100
     1.3 @@ -32,10 +32,10 @@
     1.4  
     1.5  (* diagnostics *)
     1.6  
     1.7 -fun str_of [id] = id
     1.8 -  | str_of ids = space_implode "/" (tl ids);
     1.9 +fun str_of [] = "Pure"
    1.10 +  | str_of elems = space_implode "/" elems;
    1.11  
    1.12 -fun welcome () = "Welcome to Isabelle/" ^ str_of (! session) ^ " (" ^ version ^ ")";
    1.13 +fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
    1.14  
    1.15  
    1.16  (* init *)
    1.17 @@ -59,12 +59,10 @@
    1.18  val root_file = ThyLoad.ml_path "ROOT";
    1.19  
    1.20  fun use_dir reset info parent name =
    1.21 -  let val parent_session = ! session in
    1.22 -    init reset parent name;
    1.23 -    Present.init info parent_session (! session) (path ()) name;
    1.24 +  (init reset parent name;
    1.25 +    Present.init info (path ()) name;
    1.26      Symbol.use root_file;
    1.27 -    finish ()
    1.28 -  end handle _ => exit 1;
    1.29 +    finish ()) handle _ => exit 1;
    1.30  
    1.31  
    1.32  end;