equal
deleted
inserted
replaced
5 Session management -- maintain state of logic images. |
5 Session management -- maintain state of logic images. |
6 *) |
6 *) |
7 |
7 |
8 signature SESSION = |
8 signature SESSION = |
9 sig |
9 sig |
10 val path: unit -> string list |
|
11 val welcome: unit -> string |
10 val welcome: unit -> string |
12 val use_dir: bool -> bool -> string -> string -> unit |
11 val use_dir: bool -> bool -> string -> string -> unit |
13 val finish: unit -> unit |
12 val finish: unit -> unit |
14 end; |
13 end; |
15 |
14 |
54 (* use_dir *) |
53 (* use_dir *) |
55 |
54 |
56 val root_file = ThyLoad.ml_path "ROOT"; |
55 val root_file = ThyLoad.ml_path "ROOT"; |
57 |
56 |
58 fun use_dir reset info parent name = |
57 fun use_dir reset info parent name = |
59 (init reset parent name; Symbol.use root_file; finish ()) handle _ => exit 1; |
58 (init reset parent name; |
|
59 Present.init info (! session) (path ()) parent name; |
|
60 Symbol.use root_file; |
|
61 finish ()) |
|
62 handle _ => exit 1; |
60 |
63 |
61 |
64 |
62 end; |
65 end; |