author | wenzelm |
Sun, 25 Jun 2000 23:52:59 +0200 | |
changeset 9131 | cd17637c917f |
parent 8807 | 0046be1769f9 |
child 9414 | 1463576f3968 |
permissions | -rw-r--r-- |
6346 | 1 |
(* Title: Pure/Isar/session.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
8807 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6346 | 5 |
|
6 |
Session management -- maintain state of logic images. |
|
7 |
*) |
|
8 |
||
9 |
signature SESSION = |
|
10 |
sig |
|
11 |
val welcome: unit -> string |
|
8196 | 12 |
val use_dir: bool -> bool -> string -> string -> string -> string -> string -> unit |
6346 | 13 |
val finish: unit -> unit |
14 |
end; |
|
15 |
||
16 |
structure Session: SESSION = |
|
17 |
struct |
|
18 |
||
19 |
||
20 |
(* session state *) |
|
21 |
||
22 |
val pure = "Pure"; |
|
23 |
||
24 |
val session = ref ([pure]: string list); |
|
25 |
val session_path = ref ([]: string list); |
|
26 |
val session_finished = ref false; |
|
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
27 |
val rpath = ref (None : Url.T option); |
6346 | 28 |
|
29 |
fun path () = ! session_path; |
|
30 |
||
31 |
fun add_path reset s = |
|
32 |
(session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s])); |
|
33 |
||
34 |
||
35 |
(* diagnostics *) |
|
36 |
||
37 |
fun str_of [] = "Pure" |
|
38 |
| str_of elems = space_implode "/" elems; |
|
39 |
||
40 |
fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; |
|
41 |
||
42 |
||
43 |
(* init *) |
|
44 |
||
45 |
fun init reset parent name = |
|
46 |
if not (parent mem_string (! session)) orelse not (! session_finished) then |
|
47 |
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
|
48 |
else (add_path reset name; session_finished := false); |
|
49 |
||
50 |
||
51 |
(* finish *) |
|
52 |
||
53 |
fun finish () = |
|
6663 | 54 |
(ThyInfo.finish (); |
6346 | 55 |
Present.finish (); |
56 |
session_finished := true); |
|
57 |
||
58 |
||
59 |
(* use_dir *) |
|
60 |
||
61 |
val root_file = ThyLoad.ml_path "ROOT"; |
|
62 |
||
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
63 |
fun get_rpath rpath_str = |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
64 |
(if rpath_str = "" then () else |
7227
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
65 |
if is_some (!rpath) then |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
66 |
error "Path for remote theory browsing information may only be set once" |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
67 |
else |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
68 |
rpath := Some (Url.unpack rpath_str); |
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
69 |
(!rpath, rpath_str <> "")); |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
70 |
|
8196 | 71 |
fun use_dir reset info doc parent name dump rpath_str = |
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
72 |
(init reset parent name; |
8196 | 73 |
Present.init info doc (path ()) name |
74 |
(if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str); |
|
7227
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
75 |
File.symbol_use root_file; |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
76 |
finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1); |
6346 | 77 |
|
78 |
||
79 |
end; |