equal
deleted
inserted
replaced
90 val skip_proof: (int History.T -> int History.T) -> transition -> transition |
90 val skip_proof: (int History.T -> int History.T) -> transition -> transition |
91 val skip_proof_to_theory: (int -> bool) -> transition -> transition |
91 val skip_proof_to_theory: (int -> bool) -> transition -> transition |
92 val unknown_theory: transition -> transition |
92 val unknown_theory: transition -> transition |
93 val unknown_proof: transition -> transition |
93 val unknown_proof: transition -> transition |
94 val unknown_context: transition -> transition |
94 val unknown_context: transition -> transition |
95 val thread_properties: unit -> Markup.property list |
|
96 val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a |
95 val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a |
97 val excursion: transition list -> unit |
96 val excursion: transition list -> unit |
98 val set_state: state -> unit |
97 val set_state: state -> unit |
99 val get_state: unit -> state |
98 val get_state: unit -> state |
100 val exn: unit -> (exn * string) option |
99 val exn: unit -> (exn * string) option |
668 |
667 |
669 (** toplevel transactions **) |
668 (** toplevel transactions **) |
670 |
669 |
671 (* thread transition properties *) |
670 (* thread transition properties *) |
672 |
671 |
|
672 fun setmp_thread_position (Transition {props, pos, ...}) f x = |
|
673 Position.setmp_thread_data pos f x; |
|
674 |
|
675 |
|
676 (* apply transitions *) |
|
677 |
673 local |
678 local |
674 val tag = Universal.tag () : Markup.property list Universal.tag; |
|
675 in |
|
676 |
|
677 fun thread_properties () = these (Multithreading.get_data tag); |
|
678 |
|
679 fun setmp_thread_properties (Transition {name, props, pos, ...}) f x = |
|
680 setmp_thread_data tag (thread_properties ()) |
|
681 (fold (AList.update (op =)) ((Markup.nameN, name) :: Position.properties_of pos) props) f x; |
|
682 |
|
683 end; |
|
684 |
|
685 |
|
686 (* apply transitions *) |
|
687 |
|
688 local |
|
689 |
679 |
690 fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) = |
680 fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) = |
691 setmp_thread_properties tr (fn state => |
681 setmp_thread_position tr (fn state => |
692 let |
682 let |
693 val _ = |
683 val _ = |
694 if not int andalso int_only then warning (command_msg "Interactive-only " tr) |
684 if not int andalso int_only then warning (command_msg "Interactive-only " tr) |
695 else (); |
685 else (); |
696 |
686 |
768 NONE => false |
758 NONE => false |
769 | SOME (state', exn_info) => |
759 | SOME (state', exn_info) => |
770 (global_state := (state', exn_info); |
760 (global_state := (state', exn_info); |
771 (case exn_info of |
761 (case exn_info of |
772 NONE => () |
762 NONE => () |
773 | SOME err => setmp_thread_properties tr print_exn err); |
763 | SOME err => setmp_thread_position tr print_exn err); |
774 true)); |
764 true)); |
775 |
765 |
776 fun >>> [] = () |
766 fun >>> [] = () |
777 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
767 | >>> (tr :: trs) = if >> tr then >>> trs else (); |
778 |
768 |