30 val interact: bool Unsynchronized.ref |
30 val interact: bool Unsynchronized.ref |
31 val timing: bool Unsynchronized.ref |
31 val timing: bool Unsynchronized.ref |
32 val profiling: int Unsynchronized.ref |
32 val profiling: int Unsynchronized.ref |
33 type transition |
33 type transition |
34 val empty: transition |
34 val empty: transition |
35 val print_of: transition -> bool |
|
36 val name_of: transition -> string |
35 val name_of: transition -> string |
37 val pos_of: transition -> Position.T |
36 val pos_of: transition -> Position.T |
38 val name: string -> transition -> transition |
37 val name: string -> transition -> transition |
39 val position: Position.T -> transition -> transition |
38 val position: Position.T -> transition -> transition |
40 val interactive: bool -> transition -> transition |
39 val interactive: bool -> transition -> transition |
41 val set_print: bool -> transition -> transition |
|
42 val print: transition -> transition |
|
43 val init_theory: (unit -> theory) -> transition -> transition |
40 val init_theory: (unit -> theory) -> transition -> transition |
44 val is_init: transition -> bool |
41 val is_init: transition -> bool |
45 val modify_init: (unit -> theory) -> transition -> transition |
42 val modify_init: (unit -> theory) -> transition -> transition |
46 val exit: transition -> transition |
43 val exit: transition -> transition |
47 val keep: (state -> unit) -> transition -> transition |
44 val keep: (state -> unit) -> transition -> transition |
314 |
311 |
315 datatype transition = Transition of |
312 datatype transition = Transition of |
316 {name: string, (*command name*) |
313 {name: string, (*command name*) |
317 pos: Position.T, (*source position*) |
314 pos: Position.T, (*source position*) |
318 int_only: bool, (*interactive-only*) (* TTY / Proof General legacy*) |
315 int_only: bool, (*interactive-only*) (* TTY / Proof General legacy*) |
319 print: bool, (*print result state*) |
|
320 timing: Time.time option, (*prescient timing information*) |
316 timing: Time.time option, (*prescient timing information*) |
321 trans: trans list}; (*primitive transitions (union)*) |
317 trans: trans list}; (*primitive transitions (union)*) |
322 |
318 |
323 fun make_transition (name, pos, int_only, print, timing, trans) = |
319 fun make_transition (name, pos, int_only, timing, trans) = |
324 Transition {name = name, pos = pos, int_only = int_only, print = print, |
320 Transition {name = name, pos = pos, int_only = int_only, |
325 timing = timing, trans = trans}; |
321 timing = timing, trans = trans}; |
326 |
322 |
327 fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) = |
323 fun map_transition f (Transition {name, pos, int_only, timing, trans}) = |
328 make_transition (f (name, pos, int_only, print, timing, trans)); |
324 make_transition (f (name, pos, int_only, timing, trans)); |
329 |
325 |
330 val empty = make_transition ("", Position.none, false, false, NONE, []); |
326 val empty = make_transition ("", Position.none, false, NONE, []); |
331 |
327 |
332 |
328 |
333 (* diagnostics *) |
329 (* diagnostics *) |
334 |
330 |
335 fun print_of (Transition {print, ...}) = print; |
|
336 fun name_of (Transition {name, ...}) = name; |
331 fun name_of (Transition {name, ...}) = name; |
337 fun pos_of (Transition {pos, ...}) = pos; |
332 fun pos_of (Transition {pos, ...}) = pos; |
338 |
333 |
339 fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr); |
334 fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr); |
340 fun at_command tr = command_msg "At " tr; |
335 fun at_command tr = command_msg "At " tr; |
343 ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); |
338 ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); |
344 |
339 |
345 |
340 |
346 (* modify transitions *) |
341 (* modify transitions *) |
347 |
342 |
348 fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) => |
343 fun name name = map_transition (fn (_, pos, int_only, timing, trans) => |
349 (name, pos, int_only, print, timing, trans)); |
344 (name, pos, int_only, timing, trans)); |
350 |
345 |
351 fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) => |
346 fun position pos = map_transition (fn (name, _, int_only, timing, trans) => |
352 (name, pos, int_only, print, timing, trans)); |
347 (name, pos, int_only, timing, trans)); |
353 |
348 |
354 fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) => |
349 fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) => |
355 (name, pos, int_only, print, timing, trans)); |
350 (name, pos, int_only, timing, trans)); |
356 |
351 |
357 fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) => |
352 fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) => |
358 (name, pos, int_only, print, timing, tr :: trans)); |
353 (name, pos, int_only, timing, tr :: trans)); |
359 |
354 |
360 val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) => |
355 val reset_trans = map_transition (fn (name, pos, int_only, timing, _) => |
361 (name, pos, int_only, print, timing, [])); |
356 (name, pos, int_only, timing, [])); |
362 |
|
363 fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) => |
|
364 (name, pos, int_only, print, timing, trans)); |
|
365 |
|
366 val print = set_print true; |
|
367 |
357 |
368 |
358 |
369 (* basic transitions *) |
359 (* basic transitions *) |
370 |
360 |
371 fun init_theory f = add_trans (Init f); |
361 fun init_theory f = add_trans (Init f); |
581 |
571 |
582 |
572 |
583 (* apply transitions *) |
573 (* apply transitions *) |
584 |
574 |
585 fun get_timing (Transition {timing, ...}) = timing; |
575 fun get_timing (Transition {timing, ...}) = timing; |
586 fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) => |
576 fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) => |
587 (name, pos, int_only, print, timing, trans)); |
577 (name, pos, int_only, timing, trans)); |
588 |
578 |
589 local |
579 local |
590 |
580 |
591 fun app int (tr as Transition {trans, print, ...}) = |
581 fun app int (tr as Transition {name, trans, ...}) = |
592 setmp_thread_position tr (fn state => |
582 setmp_thread_position tr (fn state => |
593 let |
583 let |
594 val timing_start = Timing.start (); |
584 val timing_start = Timing.start (); |
595 |
585 |
596 val (result, opt_err) = |
586 val (result, opt_err) = |
597 state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling)); |
587 state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling)); |
598 val _ = if int andalso not (! quiet) andalso print then print_state result else (); |
588 |
|
589 val _ = |
|
590 if int andalso not (! quiet) andalso Keyword.is_printed name |
|
591 then print_state result else (); |
599 |
592 |
600 val timing_result = Timing.result timing_start; |
593 val timing_result = Timing.result timing_start; |
601 val timing_props = |
594 val timing_props = |
602 Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr); |
595 Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr); |
603 val _ = Timing.protocol_message timing_props timing_result; |
596 val _ = Timing.protocol_message timing_props timing_result; |
741 (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o |
734 (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o |
742 end_proof (fn _ => future_proof #> |
735 end_proof (fn _ => future_proof #> |
743 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); |
736 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); |
744 |
737 |
745 val st'' = st' |
738 val st'' = st' |
746 |> command (head_tr |> set_print false |> reset_trans |> forked_proof); |
739 |> command (head_tr |> reset_trans |> forked_proof); |
747 val end_result = Result (end_tr, st''); |
740 val end_result = Result (end_tr, st''); |
748 val result = |
741 val result = |
749 Result_List [head_result, Result.get (presentation_context_of st''), end_result]; |
742 Result_List [head_result, Result.get (presentation_context_of st''), end_result]; |
750 in (result, st'') end |
743 in (result, st'') end |
751 end; |
744 end; |