equal
deleted
inserted
replaced
20 end; |
20 end; |
21 |
21 |
22 signature CONTEXT = |
22 signature CONTEXT = |
23 sig |
23 sig |
24 include BASIC_CONTEXT |
24 include BASIC_CONTEXT |
|
25 val welcome: unit -> string |
25 val >> : (theory -> theory) -> unit |
26 val >> : (theory -> theory) -> unit |
26 end; |
27 end; |
27 |
28 |
28 structure Context: CONTEXT = |
29 structure Context: CONTEXT = |
29 struct |
30 struct |
34 val current_session = ref ([]: string list); |
35 val current_session = ref ([]: string list); |
35 |
36 |
36 fun get_session () = ! current_session; |
37 fun get_session () = ! current_session; |
37 fun add_session s = current_session := ! current_session @ [s]; |
38 fun add_session s = current_session := ! current_session @ [s]; |
38 fun reset_session () = current_session := []; |
39 fun reset_session () = current_session := []; |
|
40 |
|
41 fun welcome () = |
|
42 "Welcome to Isabelle/" ^ |
|
43 (case get_session () of [] => "Pure" | ss => space_implode "/" ss) ^ |
|
44 " (" ^ version ^ ")"; |
39 |
45 |
40 |
46 |
41 |
47 |
42 (** theory context **) |
48 (** theory context **) |
43 |
49 |