equal
deleted
inserted
replaced
6 Session management -- maintain state of logic images. |
6 Session management -- maintain state of logic images. |
7 *) |
7 *) |
8 |
8 |
9 signature SESSION = |
9 signature SESSION = |
10 sig |
10 sig |
|
11 val name: unit -> string |
11 val welcome: unit -> string |
12 val welcome: unit -> string |
12 val use_dir: |
13 val use_dir: |
13 string list -> bool -> bool -> string -> string -> string -> string -> string -> unit |
14 string list -> bool -> bool -> string -> string -> string -> string -> string -> unit |
14 val finish: unit -> unit |
15 val finish: unit -> unit |
15 end; |
16 end; |
33 fun path () = ! session_path; |
34 fun path () = ! session_path; |
34 |
35 |
35 fun str_of [] = pure |
36 fun str_of [] = pure |
36 | str_of elems = space_implode "/" elems; |
37 | str_of elems = space_implode "/" elems; |
37 |
38 |
38 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; |
39 fun name () = "Isabelle/" ^ str_of (path ()); |
|
40 fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")"; |
39 |
41 |
40 |
42 |
41 (* add_path *) |
43 (* add_path *) |
42 |
44 |
43 fun add_path reset s = |
45 fun add_path reset s = |