equal
deleted
inserted
replaced
30 (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s])); |
30 (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s])); |
31 |
31 |
32 |
32 |
33 (* diagnostics *) |
33 (* diagnostics *) |
34 |
34 |
35 fun str_of [id] = id |
35 fun str_of [] = "Pure" |
36 | str_of ids = space_implode "/" (tl ids); |
36 | str_of elems = space_implode "/" elems; |
37 |
37 |
38 fun welcome () = "Welcome to Isabelle/" ^ str_of (! session) ^ " (" ^ version ^ ")"; |
38 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; |
39 |
39 |
40 |
40 |
41 (* init *) |
41 (* init *) |
42 |
42 |
43 fun init reset parent name = |
43 fun init reset parent name = |
57 (* use_dir *) |
57 (* use_dir *) |
58 |
58 |
59 val root_file = ThyLoad.ml_path "ROOT"; |
59 val root_file = ThyLoad.ml_path "ROOT"; |
60 |
60 |
61 fun use_dir reset info parent name = |
61 fun use_dir reset info parent name = |
62 let val parent_session = ! session in |
62 (init reset parent name; |
63 init reset parent name; |
63 Present.init info (path ()) name; |
64 Present.init info parent_session (! session) (path ()) name; |
|
65 Symbol.use root_file; |
64 Symbol.use root_file; |
66 finish () |
65 finish ()) handle _ => exit 1; |
67 end handle _ => exit 1; |
|
68 |
66 |
69 |
67 |
70 end; |
68 end; |