equal
deleted
inserted
replaced
231 end; |
231 end; |
232 |
232 |
233 |
233 |
234 (* interactive state transformations *) |
234 (* interactive state transformations *) |
235 |
235 |
236 local nonfix >> >>> in |
236 fun op >> raw_tr = |
237 |
|
238 fun >> raw_tr = |
|
239 let |
237 let |
240 val id = create_command raw_tr; |
238 val id = create_command raw_tr; |
241 val {category, transition = tr, ...} = the_command id; |
239 val {category, transition = tr, ...} = the_command id; |
242 val (prev, prev_state) = point_state (); |
240 val (prev, prev_state) = point_state (); |
243 val _ = |
241 val _ = |
252 (update_status status id; set_exn NONE; |
250 (update_status status id; set_exn NONE; |
253 if is_regular category then set_point id else (); |
251 if is_regular category then set_point id else (); |
254 true)) |
252 true)) |
255 end; |
253 end; |
256 |
254 |
257 fun >>> [] = () |
255 fun op >>> [] = () |
258 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
256 | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); |
259 |
|
260 end; |
|
261 |
257 |
262 |
258 |
263 (* implicit navigation wrt. proper commands *) |
259 (* implicit navigation wrt. proper commands *) |
264 |
260 |
265 local |
261 local |
314 prev <> no_id ? Markup.markup |
310 prev <> no_id ? Markup.markup |
315 (Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt); |
311 (Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt); |
316 in |
312 in |
317 (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of |
313 (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of |
318 NONE => if secure then quit () else () |
314 NONE => if secure then quit () else () |
319 | SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ()) |
315 | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) |
320 handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash => |
316 handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash => |
321 (CRITICAL (fn () => change crashes (cons crash)); |
317 (CRITICAL (fn () => change crashes (cons crash)); |
322 warning "Recovering after Isar toplevel crash -- see also Isar.crashes"); |
318 warning "Recovering after Isar toplevel crash -- see also Isar.crashes"); |
323 raw_loop secure src) |
319 raw_loop secure src) |
324 end; |
320 end; |