author | wenzelm |
Mon, 14 Jul 2008 17:51:39 +0200 | |
changeset 27573 | 10ba0d7d94e0 |
parent 27533 | 85bbd045ac3e |
child 27584 | e0cd0396945a |
permissions | -rw-r--r-- |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/isar.ML |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
4 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
5 |
The global Isabelle/Isar state and main read-eval-print loop. |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
6 |
*) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
7 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
8 |
signature ISAR = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
9 |
sig |
27530 | 10 |
val init_point: unit -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
11 |
val state: unit -> Toplevel.state |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
12 |
val exn: unit -> (exn * string) option |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
13 |
val context: unit -> Proof.context |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
14 |
val goal: unit -> thm |
27533 | 15 |
val print: unit -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
16 |
val >> : Toplevel.transition -> bool |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
17 |
val >>> : Toplevel.transition list -> unit |
27573 | 18 |
val commit_exit: unit -> unit |
27529 | 19 |
val linear_undo: int -> unit |
27524 | 20 |
val undo: int -> unit |
27530 | 21 |
val kill: unit -> unit |
22 |
val kill_proof: unit -> unit |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
23 |
val crashes: exn list ref |
26643 | 24 |
val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
25 |
val loop: unit -> unit |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
26 |
val main: unit -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
27 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
28 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
29 |
structure Isar: ISAR = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
30 |
struct |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
31 |
|
27432 | 32 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
33 |
(** individual toplevel commands **) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
34 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
35 |
(* unique identification *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
36 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
37 |
type id = string; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
38 |
val no_id : id = ""; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
39 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
40 |
fun identify tr = |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
41 |
(case Toplevel.get_id tr of |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
42 |
SOME id => (id, tr) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
43 |
| NONE => |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
44 |
let val id = "isabelle:" ^ serial_string () |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
45 |
in (id, Toplevel.put_id id tr) end); |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
46 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
47 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
48 |
(* command category *) |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
49 |
|
27524 | 50 |
datatype category = Empty | Theory | Proof | Diag | Control; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
51 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
52 |
fun category_of tr = |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
53 |
let val name = Toplevel.name_of tr in |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
54 |
if name = "" then Empty |
27524 | 55 |
else if OuterKeyword.is_theory name then Theory |
56 |
else if OuterKeyword.is_proof name then Proof |
|
57 |
else if OuterKeyword.is_diag name then Diag |
|
58 |
else Control |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
59 |
end; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
60 |
|
27524 | 61 |
val is_theory = fn Theory => true | _ => false; |
62 |
val is_proper = fn Theory => true | Proof => true | _ => false; |
|
63 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
64 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
65 |
(* datatype command *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
66 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
67 |
datatype status = |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
68 |
Initial | |
27518 | 69 |
Result of Toplevel.state * (exn * string) option; |
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
70 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
71 |
datatype command = Command of |
27501 | 72 |
{category: category, |
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
73 |
transition: Toplevel.transition, |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
74 |
status: status}; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
75 |
|
27501 | 76 |
fun make_command (category, transition, status) = |
77 |
Command {category = category, transition = transition, status = status}; |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
78 |
|
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
79 |
val empty_command = |
27518 | 80 |
make_command (Empty, Toplevel.empty, Result (Toplevel.toplevel, NONE)); |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
81 |
|
27501 | 82 |
fun map_command f (Command {category, transition, status}) = |
83 |
make_command (f (category, transition, status)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
84 |
|
27501 | 85 |
fun map_status f = map_command (fn (category, transition, status) => |
86 |
(category, transition, f status)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
87 |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
88 |
|
27501 | 89 |
(* global collection of identified commands *) |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
90 |
|
27518 | 91 |
fun err_dup id = sys_error ("Duplicate command " ^ quote id); |
92 |
fun err_undef id = sys_error ("Unknown command " ^ quote id); |
|
93 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
94 |
local |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
95 |
|
27501 | 96 |
val empty_commands = Graph.empty: command Graph.T; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
97 |
val global_commands = ref empty_commands; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
98 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
99 |
in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
100 |
|
27501 | 101 |
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f) |
27518 | 102 |
handle Graph.DUP id => err_dup id | Graph.UNDEF id => err_undef id; |
27501 | 103 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
104 |
fun init_commands () = change_commands (K empty_commands); |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
105 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
106 |
fun the_command id = |
27524 | 107 |
let val Command cmd = |
108 |
if id = no_id then empty_command |
|
109 |
else (Graph.get_node (! global_commands) id handle Graph.UNDEF _ => err_undef id) |
|
110 |
in cmd end; |
|
27518 | 111 |
|
112 |
fun prev_command id = |
|
113 |
if id = no_id then NONE |
|
114 |
else |
|
115 |
(case Graph.imm_preds (! global_commands) id handle Graph.UNDEF _ => err_undef id of |
|
116 |
[] => NONE |
|
117 |
| [prev] => SOME prev |
|
118 |
| _ => sys_error ("Non-linear command dependency " ^ quote id)); |
|
27501 | 119 |
|
120 |
end; |
|
121 |
||
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
122 |
|
27518 | 123 |
fun the_result id = |
27524 | 124 |
(case the_command id of |
125 |
{status = Result res, ...} => res |
|
126 |
| {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition)); |
|
127 |
||
128 |
val the_state = #1 o the_result; |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
129 |
|
27501 | 130 |
fun new_command prev (id, cmd) = |
131 |
change_commands (Graph.new_node (id, cmd) #> prev <> no_id ? Graph.add_edge (prev, id)); |
|
132 |
||
133 |
fun dispose_command id = change_commands (Graph.del_nodes [id]); |
|
134 |
||
135 |
fun change_command_status id f = change_commands (Graph.map_node id (map_status f)); |
|
136 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
137 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
138 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
139 |
(** TTY interaction **) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
140 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
141 |
(* global point *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
142 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
143 |
local val global_point = ref no_id in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
144 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
145 |
fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f); |
27524 | 146 |
fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point); |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
147 |
|
27501 | 148 |
end; |
149 |
||
27524 | 150 |
fun set_point id = change_point (K id); |
27530 | 151 |
fun init_point () = set_point no_id; |
27524 | 152 |
|
153 |
fun point_result () = NAMED_CRITICAL "Isar" (fn () => |
|
154 |
let val id = point () in (id, the_result id) end); |
|
27501 | 155 |
|
27518 | 156 |
fun state () = #1 (#2 (point_result ())); |
157 |
fun exn () = #2 (#2 (point_result ())); |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
158 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
159 |
fun context () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
160 |
Toplevel.context_of (state ()) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
161 |
handle Toplevel.UNDEF => error "Unknown context"; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
162 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
163 |
fun goal () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
164 |
#2 (#2 (Proof.get_goal (Toplevel.proof_of (state ())))) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
165 |
handle Toplevel.UNDEF => error "No goal present"; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
166 |
|
27533 | 167 |
fun print () = Toplevel.print_state false (state ()); |
168 |
||
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
169 |
|
27573 | 170 |
(* commit final exit *) |
171 |
||
172 |
fun commit_exit () = |
|
173 |
let val (id, (st, _)) = point_result () in |
|
174 |
(case (Toplevel.is_toplevel st, prev_command id) of |
|
175 |
(true, SOME prev) => |
|
176 |
(case Toplevel.transition true Toplevel.commit_exit (#1 (the_result prev)) of |
|
177 |
SOME (_, SOME (exn, msg)) => raise Exn.EXCEPTIONS ([exn], msg) |
|
178 |
| _ => ()) |
|
179 |
| _ => error "Expected to find finished theory") |
|
180 |
end; |
|
181 |
||
182 |
||
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
183 |
(* interactive state transformations --- NOT THREAD-SAFE! *) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
184 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
185 |
nonfix >> >>>; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
186 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
187 |
fun >> raw_tr = |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
188 |
let |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
189 |
val (id, tr) = identify raw_tr; |
27518 | 190 |
val (prev, (prev_state, _)) = point_result (); |
27524 | 191 |
val category = category_of tr; |
192 |
val _ = new_command prev (id, make_command (category, tr, Initial)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
193 |
in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
194 |
(case Toplevel.transition true tr prev_state of |
27501 | 195 |
NONE => (dispose_command id; false) |
27527 | 196 |
| SOME (result as (_, err)) => |
197 |
(change_command_status id (K (Result result)); |
|
198 |
Option.map (Toplevel.error_msg tr) err; |
|
199 |
if is_some err orelse category = Control then dispose_command id |
|
27524 | 200 |
else set_point id; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
201 |
true)) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
202 |
end; |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
203 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
204 |
fun >>> [] = () |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
205 |
| >>> (tr :: trs) = if >> tr then >>> trs else (); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
206 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
207 |
|
27530 | 208 |
(* implicit navigation wrt. proper commands *) |
27524 | 209 |
|
210 |
local |
|
211 |
||
212 |
fun err_undo () = error "Undo history exhausted"; |
|
213 |
||
214 |
fun get_prev id = the_default no_id (prev_command id); |
|
215 |
||
27530 | 216 |
fun find_category which id = |
27524 | 217 |
(case #category (the_command id) of |
218 |
Empty => err_undo () |
|
27530 | 219 |
| category => if which category then id else find_category which (get_prev id)); |
220 |
||
221 |
fun find_begin_theory id = |
|
222 |
if id = no_id then err_undo () |
|
223 |
else if is_some (Toplevel.init_of (#transition (the_command id))) then id |
|
224 |
else find_begin_theory (get_prev id); |
|
27524 | 225 |
|
27529 | 226 |
fun undo_command id = |
27530 | 227 |
(case Toplevel.init_of (#transition (the_command id)) of |
228 |
SOME name => get_prev id before ThyInfo.kill_thy name |
|
229 |
| NONE => get_prev id); |
|
27529 | 230 |
|
27524 | 231 |
in |
232 |
||
27530 | 233 |
fun linear_undo n = change_point (funpow n (fn id => undo_command (find_category is_proper id))); |
234 |
||
235 |
fun undo n = change_point (funpow n (fn id => undo_command |
|
236 |
(find_category (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id))); |
|
237 |
||
238 |
fun kill () = change_point (fn id => undo_command |
|
239 |
(if Toplevel.is_proof (the_state id) then find_category is_theory id else find_begin_theory id)); |
|
240 |
||
241 |
fun kill_proof () = change_point (fn id => |
|
242 |
if Toplevel.is_proof (the_state id) then undo_command (find_category is_theory id) |
|
243 |
else raise Toplevel.UNDEF); |
|
27524 | 244 |
|
245 |
end; |
|
246 |
||
247 |
||
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
248 |
(* toplevel loop *) |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
249 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
250 |
val crashes = ref ([]: exn list); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
251 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
252 |
local |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
253 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
254 |
fun raw_loop secure src = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
255 |
let |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
256 |
fun check_secure () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
257 |
(if secure then warning "Secure loop -- cannot exit to ML" else (); secure); |
27524 | 258 |
val prev = point (); |
259 |
val prev_name = Toplevel.name_of (#transition (the_command prev)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
260 |
val prompt_markup = |
27524 | 261 |
prev <> no_id ? Markup.markup |
262 |
(Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt); |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
263 |
in |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
264 |
(case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
265 |
NONE => if secure then quit () else () |
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
266 |
| SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ()) |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
267 |
handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash => |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
268 |
(CRITICAL (fn () => change crashes (cons crash)); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
269 |
warning "Recovering after Isar toplevel crash -- see also Isar.crashes"); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
270 |
raw_loop secure src) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
271 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
272 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
273 |
in |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
274 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
275 |
fun toplevel_loop {init, welcome, sync, secure} = |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
276 |
(Context.set_thread_data NONE; |
27530 | 277 |
if init then (init_point (); init_commands ()) else (); |
26643 | 278 |
if welcome then writeln (Session.welcome ()) else (); |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
279 |
uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ()); |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
280 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
281 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
282 |
|
26643 | 283 |
fun loop () = |
284 |
toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; |
|
27528 | 285 |
|
26643 | 286 |
fun main () = |
287 |
toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
288 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
289 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
290 |