author | wenzelm |
Wed, 16 Jul 2008 11:20:24 +0200 | |
changeset 27616 | a811269b577c |
parent 27606 | 82399f3a8ca8 |
child 27620 | dfecac40e4be |
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 |
27616 | 10 |
type id = string |
11 |
val no_id: id |
|
12 |
val create_command: Toplevel.transition -> id |
|
27530 | 13 |
val init_point: unit -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
14 |
val state: unit -> Toplevel.state |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
15 |
val context: unit -> Proof.context |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
16 |
val goal: unit -> thm |
27533 | 17 |
val print: unit -> unit |
27616 | 18 |
val exn: unit -> (exn * string) option |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
19 |
val >> : Toplevel.transition -> bool |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
20 |
val >>> : Toplevel.transition list -> unit |
27529 | 21 |
val linear_undo: int -> unit |
27524 | 22 |
val undo: int -> unit |
27530 | 23 |
val kill: unit -> unit |
24 |
val kill_proof: unit -> unit |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
25 |
val crashes: exn list ref |
26643 | 26 |
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
|
27 |
val loop: unit -> unit |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
28 |
val main: unit -> unit |
27616 | 29 |
val insert_command: id -> id -> unit |
30 |
val remove_command: id -> unit |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
31 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
32 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
33 |
structure Isar: ISAR = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
34 |
struct |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
35 |
|
27432 | 36 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
37 |
(** individual toplevel commands **) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
38 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
39 |
(* unique identification *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
40 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
41 |
type id = string; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
42 |
val no_id : id = ""; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
43 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
44 |
fun identify tr = |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
45 |
(case Toplevel.get_id tr of |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
46 |
SOME id => (id, tr) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
47 |
| NONE => |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
48 |
let val id = "isabelle:" ^ serial_string () |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
49 |
in (id, Toplevel.put_id id tr) end); |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
50 |
|
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 |
(* command category *) |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
53 |
|
27524 | 54 |
datatype category = Empty | Theory | Proof | Diag | Control; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
55 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
56 |
fun category_of tr = |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
57 |
let val name = Toplevel.name_of tr in |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
58 |
if name = "" then Empty |
27524 | 59 |
else if OuterKeyword.is_theory name then Theory |
60 |
else if OuterKeyword.is_proof name then Proof |
|
61 |
else if OuterKeyword.is_diag name then Diag |
|
62 |
else Control |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
63 |
end; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
64 |
|
27524 | 65 |
val is_theory = fn Theory => true | _ => false; |
66 |
val is_proper = fn Theory => true | Proof => true | _ => false; |
|
67 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
68 |
|
27616 | 69 |
(* command status *) |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
70 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
71 |
datatype status = |
27616 | 72 |
Unprocessed | |
73 |
Running | |
|
74 |
Failed of exn * string | |
|
75 |
Finished of Toplevel.state; |
|
76 |
||
77 |
fun status_markup Unprocessed = Markup.unprocessed |
|
78 |
| status_markup Running = Markup.running |
|
79 |
| status_markup (Failed _) = Markup.failed |
|
80 |
| status_markup (Finished _) = Markup.finished; |
|
81 |
||
82 |
||
83 |
(* datatype command *) |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
84 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
85 |
datatype command = Command of |
27501 | 86 |
{category: category, |
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
87 |
transition: Toplevel.transition, |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
88 |
status: status}; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
89 |
|
27501 | 90 |
fun make_command (category, transition, status) = |
91 |
Command {category = category, transition = transition, status = status}; |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
92 |
|
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
93 |
val empty_command = |
27616 | 94 |
make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel); |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
95 |
|
27501 | 96 |
fun map_command f (Command {category, transition, status}) = |
97 |
make_command (f (category, transition, status)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
98 |
|
27501 | 99 |
fun map_status f = map_command (fn (category, transition, status) => |
100 |
(category, transition, f status)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
101 |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
102 |
|
27501 | 103 |
(* global collection of identified commands *) |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
104 |
|
27518 | 105 |
fun err_dup id = sys_error ("Duplicate command " ^ quote id); |
106 |
fun err_undef id = sys_error ("Unknown command " ^ quote id); |
|
107 |
||
27616 | 108 |
local val global_commands = ref (Graph.empty: command Graph.T) in |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
109 |
|
27501 | 110 |
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f) |
27616 | 111 |
handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad; |
112 |
||
113 |
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands); |
|
27501 | 114 |
|
27616 | 115 |
end; |
116 |
||
117 |
||
118 |
fun init_commands () = change_commands (K Graph.empty); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
119 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
120 |
fun the_command id = |
27524 | 121 |
let val Command cmd = |
122 |
if id = no_id then empty_command |
|
27616 | 123 |
else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad) |
27524 | 124 |
in cmd end; |
27518 | 125 |
|
126 |
fun prev_command id = |
|
127 |
if id = no_id then NONE |
|
128 |
else |
|
27616 | 129 |
(case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of |
27518 | 130 |
[] => NONE |
131 |
| [prev] => SOME prev |
|
132 |
| _ => sys_error ("Non-linear command dependency " ^ quote id)); |
|
27501 | 133 |
|
27616 | 134 |
fun next_commands id = |
135 |
if id = no_id then [] |
|
136 |
else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad; |
|
137 |
||
138 |
fun descendant_commands ids = |
|
139 |
Graph.all_succs (get_commands ()) (filter_out (fn id => id = no_id) ids) |
|
140 |
handle Graph.UNDEF bad => err_undef bad; |
|
141 |
||
142 |
||
143 |
(* maintain status *) |
|
144 |
||
145 |
fun report_status markup id = Toplevel.status (#transition (the_command id)) markup; |
|
146 |
||
147 |
fun update_status status id = change_commands (Graph.map_node id (map_status (fn old_status => |
|
148 |
let |
|
149 |
val markup = status_markup status; |
|
150 |
val _ = if markup <> status_markup old_status then report_status markup id else (); |
|
151 |
in status end))); |
|
27501 | 152 |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
153 |
|
27616 | 154 |
(* create and dispose commands *) |
27524 | 155 |
|
27616 | 156 |
fun create_command raw_tr = |
157 |
let |
|
158 |
val (id, tr) = identify raw_tr; |
|
159 |
val cmd = make_command (category_of tr, tr, Unprocessed); |
|
160 |
val _ = change_commands (Graph.new_node (id, cmd)); |
|
161 |
in id end; |
|
162 |
||
163 |
fun dispose_command id = |
|
164 |
let |
|
165 |
val desc = descendant_commands [id]; |
|
166 |
val _ = List.app (report_status Markup.disposed) desc; |
|
167 |
val _ = change_commands (Graph.del_nodes desc); |
|
168 |
in () end; |
|
27606 | 169 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
170 |
|
27616 | 171 |
(* final state *) |
27501 | 172 |
|
27616 | 173 |
fun the_state id = |
174 |
(case the_command id of |
|
175 |
{status = Finished state, ...} => state |
|
176 |
| {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition)); |
|
27501 | 177 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
178 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
179 |
|
27616 | 180 |
(** TTY model -- single-threaded **) |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
181 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
182 |
(* global point *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
183 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
184 |
local val global_point = ref no_id in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
185 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
186 |
fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f); |
27524 | 187 |
fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point); |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
188 |
|
27501 | 189 |
end; |
190 |
||
27616 | 191 |
|
27524 | 192 |
fun set_point id = change_point (K id); |
27530 | 193 |
fun init_point () = set_point no_id; |
27524 | 194 |
|
27616 | 195 |
fun point_state () = NAMED_CRITICAL "Isar" (fn () => |
196 |
let val id = point () in (id, the_state id) end); |
|
27501 | 197 |
|
27616 | 198 |
fun state () = #2 (point_state ()); |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
199 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
200 |
fun context () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
201 |
Toplevel.context_of (state ()) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
202 |
handle Toplevel.UNDEF => error "Unknown context"; |
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 goal () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
205 |
#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
|
206 |
handle Toplevel.UNDEF => error "No goal present"; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
207 |
|
27533 | 208 |
fun print () = Toplevel.print_state false (state ()); |
209 |
||
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
210 |
|
27616 | 211 |
(* global failure status *) |
212 |
||
213 |
local val global_exn = ref (NONE: (exn * string) option) in |
|
214 |
||
215 |
fun set_exn err = global_exn := err; |
|
216 |
fun exn () = ! global_exn; |
|
217 |
||
218 |
end; |
|
219 |
||
220 |
||
221 |
(* interactive state transformations *) |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
222 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
223 |
nonfix >> >>>; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
224 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
225 |
fun >> raw_tr = |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
226 |
let |
27616 | 227 |
val id = create_command raw_tr; |
228 |
val {category, transition = tr, ...} = the_command id; |
|
229 |
val (prev, prev_state) = point_state (); |
|
230 |
val _ = if prev <> no_id then change_commands (Graph.add_edge (prev, id)) else (); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
231 |
in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
232 |
(case Toplevel.transition true tr prev_state of |
27501 | 233 |
NONE => (dispose_command id; false) |
27616 | 234 |
| SOME (_, SOME err) => |
235 |
(Toplevel.error_msg tr err; set_exn (SOME err); dispose_command id; true) |
|
236 |
| SOME (state, NONE) => |
|
237 |
(set_exn NONE; |
|
238 |
if category = Control then dispose_command id |
|
239 |
else (update_status (Finished state) id; set_point id); |
|
240 |
true)) |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
241 |
end; |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
242 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
243 |
fun >>> [] = () |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
244 |
| >>> (tr :: trs) = if >> tr then >>> trs else (); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
245 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
246 |
|
27530 | 247 |
(* implicit navigation wrt. proper commands *) |
27524 | 248 |
|
249 |
local |
|
250 |
||
251 |
fun err_undo () = error "Undo history exhausted"; |
|
252 |
||
253 |
fun get_prev id = the_default no_id (prev_command id); |
|
254 |
||
27530 | 255 |
fun find_category which id = |
27524 | 256 |
(case #category (the_command id) of |
257 |
Empty => err_undo () |
|
27530 | 258 |
| category => if which category then id else find_category which (get_prev id)); |
259 |
||
260 |
fun find_begin_theory id = |
|
261 |
if id = no_id then err_undo () |
|
262 |
else if is_some (Toplevel.init_of (#transition (the_command id))) then id |
|
263 |
else find_begin_theory (get_prev id); |
|
27524 | 264 |
|
27529 | 265 |
fun undo_command id = |
27530 | 266 |
(case Toplevel.init_of (#transition (the_command id)) of |
267 |
SOME name => get_prev id before ThyInfo.kill_thy name |
|
268 |
| NONE => get_prev id); |
|
27529 | 269 |
|
27524 | 270 |
in |
271 |
||
27530 | 272 |
fun linear_undo n = change_point (funpow n (fn id => undo_command (find_category is_proper id))); |
273 |
||
274 |
fun undo n = change_point (funpow n (fn id => undo_command |
|
275 |
(find_category (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id))); |
|
276 |
||
277 |
fun kill () = change_point (fn id => undo_command |
|
278 |
(if Toplevel.is_proof (the_state id) then find_category is_theory id else find_begin_theory id)); |
|
279 |
||
280 |
fun kill_proof () = change_point (fn id => |
|
281 |
if Toplevel.is_proof (the_state id) then undo_command (find_category is_theory id) |
|
282 |
else raise Toplevel.UNDEF); |
|
27524 | 283 |
|
284 |
end; |
|
285 |
||
286 |
||
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
287 |
(* toplevel loop *) |
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 |
val crashes = ref ([]: exn list); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
290 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
291 |
local |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
292 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
293 |
fun raw_loop secure src = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
294 |
let |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
295 |
fun check_secure () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
296 |
(if secure then warning "Secure loop -- cannot exit to ML" else (); secure); |
27524 | 297 |
val prev = point (); |
298 |
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
|
299 |
val prompt_markup = |
27524 | 300 |
prev <> no_id ? Markup.markup |
301 |
(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
|
302 |
in |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
303 |
(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
|
304 |
NONE => if secure then quit () else () |
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
305 |
| 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
|
306 |
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
|
307 |
(CRITICAL (fn () => change crashes (cons crash)); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
308 |
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
|
309 |
raw_loop secure src) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
310 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
311 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
312 |
in |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
313 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
314 |
fun toplevel_loop {init, welcome, sync, secure} = |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
315 |
(Context.set_thread_data NONE; |
27530 | 316 |
if init then (init_point (); init_commands ()) else (); |
26643 | 317 |
if welcome then writeln (Session.welcome ()) else (); |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
318 |
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
|
319 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
320 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
321 |
|
26643 | 322 |
fun loop () = |
323 |
toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; |
|
27528 | 324 |
|
26643 | 325 |
fun main () = |
326 |
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
|
327 |
|
27616 | 328 |
|
329 |
||
330 |
(** editor model **) |
|
331 |
||
332 |
(* run commands *) (* FIXME *) |
|
333 |
||
334 |
fun run_commands ids = |
|
335 |
let |
|
336 |
val _ = List.app (update_status Unprocessed) ids; |
|
337 |
in () end; |
|
338 |
||
339 |
||
340 |
(* modify document *) |
|
341 |
||
342 |
fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () => |
|
343 |
let |
|
344 |
val nexts = next_commands prev; |
|
345 |
val _ = change_commands |
|
346 |
(fold (fn next => Graph.del_edge (prev, next) #> Graph.add_edge (id, next)) nexts #> |
|
347 |
Graph.add_edge (prev, id)); |
|
348 |
in descendant_commands [id] end) |> run_commands; |
|
349 |
||
350 |
fun remove_command id = NAMED_CRITICAL "Isar" (fn () => |
|
351 |
let |
|
352 |
val prev_edge = |
|
353 |
(case prev_command id of NONE => K I |
|
354 |
| SOME prev => fn next => Graph.add_edge (prev, next)); |
|
355 |
val nexts = next_commands id; |
|
356 |
val _ = change_commands (fold (fn next => Graph.del_edge (id, next) #> prev_edge next) nexts); |
|
357 |
in descendant_commands nexts end) |> run_commands; |
|
358 |
||
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
359 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
360 |