author | wenzelm |
Sun, 23 Jul 2000 12:08:07 +0200 | |
changeset 9414 | 1463576f3968 |
parent 8807 | 0046be1769f9 |
child 10571 | fdde440a9033 |
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; |
|
9414 | 27 |
val rpath = ref (None: Url.T option); |
28 |
||
29 |
||
30 |
(* access path *) |
|
6346 | 31 |
|
32 |
fun path () = ! session_path; |
|
33 |
||
34 |
fun str_of [] = "Pure" |
|
35 |
| str_of elems = space_implode "/" elems; |
|
36 |
||
37 |
fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; |
|
38 |
||
39 |
||
9414 | 40 |
(* add_path *) |
41 |
||
42 |
fun add_path reset s = |
|
43 |
let val sess = ! session @ [s] in |
|
44 |
(case Library.duplicates sess of |
|
45 |
[] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) |
|
46 |
| dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess)) |
|
47 |
end; |
|
48 |
||
49 |
||
6346 | 50 |
(* init *) |
51 |
||
52 |
fun init reset parent name = |
|
53 |
if not (parent mem_string (! session)) orelse not (! session_finished) then |
|
54 |
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
|
55 |
else (add_path reset name; session_finished := false); |
|
56 |
||
57 |
||
58 |
(* finish *) |
|
59 |
||
60 |
fun finish () = |
|
6663 | 61 |
(ThyInfo.finish (); |
6346 | 62 |
Present.finish (); |
63 |
session_finished := true); |
|
64 |
||
65 |
||
66 |
(* use_dir *) |
|
67 |
||
68 |
val root_file = ThyLoad.ml_path "ROOT"; |
|
69 |
||
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
70 |
fun get_rpath rpath_str = |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
71 |
(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
|
72 |
if is_some (!rpath) then |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
73 |
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
|
74 |
else |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
75 |
rpath := Some (Url.unpack rpath_str); |
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
76 |
(!rpath, rpath_str <> "")); |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
7227
diff
changeset
|
77 |
|
8196 | 78 |
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
|
79 |
(init reset parent name; |
8196 | 80 |
Present.init info doc (path ()) name |
81 |
(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
|
82 |
File.symbol_use root_file; |
a8e86b8e6fd1
Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents:
6663
diff
changeset
|
83 |
finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1); |
6346 | 84 |
|
85 |
||
86 |
end; |