equal
deleted
inserted
replaced
98 Scan.lift (for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.text)) |
98 Scan.lift (for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.text)) |
99 >> (fn ((ctxt, ts), (fixes, body)) => |
99 >> (fn ((ctxt, ts), (fixes, body)) => |
100 (case Token.get_value body of |
100 (case Token.get_value body of |
101 SOME (Token.Source src) => |
101 SOME (Token.Source src) => |
102 let |
102 let |
103 val text = Method_Closure.read ctxt src; |
103 val text = Method.read ctxt src; |
104 val ts' = |
104 val ts' = |
105 map |
105 map |
106 (fn (b, (Parse_Tools.Real_Val v, match_args)) => |
106 (fn (b, (Parse_Tools.Real_Val v, match_args)) => |
107 ((Option.map (fn (b, att) => |
107 ((Option.map (fn (b, att) => |
108 (Parse_Tools.the_real_val b, att)) b, match_args), v) |
108 (Parse_Tools.the_real_val b, att)) b, match_args), v) |
199 |
199 |
200 val (binds, ctxt6) = ctxt5 |
200 val (binds, ctxt6) = ctxt5 |
201 |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev) |
201 |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev) |
202 ||> Proof_Context.restore_mode ctxt; |
202 ||> Proof_Context.restore_mode ctxt; |
203 |
203 |
204 val (text, src) = Method_Closure.read_closure_input ctxt6 (Token.input_of body); |
204 val (text, src) = Method.read_closure_input ctxt6 (Token.input_of body); |
205 |
205 |
206 val morphism = |
206 val morphism = |
207 Variable.export_morphism ctxt6 |
207 Variable.export_morphism ctxt6 |
208 (ctxt |
208 (ctxt |
209 |> fold Token.declare_maxidx src |
209 |> fold Token.declare_maxidx src |
643 in |
643 in |
644 (case m of |
644 (case m of |
645 Match_Fact net => |
645 Match_Fact net => |
646 make_fact_matches goal_ctxt (Item_Net.retrieve net) |
646 make_fact_matches goal_ctxt (Item_Net.retrieve net) |
647 |> Seq.map (fn (text, ctxt') => |
647 |> Seq.map (fn (text, ctxt') => |
648 Method_Closure.method_evaluate text ctxt' using (ctxt', st) |
648 Method.evaluate_runtime text ctxt' using (ctxt', st) |
649 |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm))) |
649 |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm))) |
650 | Match_Term net => |
650 | Match_Term net => |
651 make_term_matches goal_ctxt (Item_Net.retrieve net) |
651 make_term_matches goal_ctxt (Item_Net.retrieve net) |
652 |> Seq.map (fn (text, ctxt') => |
652 |> Seq.map (fn (text, ctxt') => |
653 Method_Closure.method_evaluate text ctxt' using (ctxt', st) |
653 Method.evaluate_runtime text ctxt' using (ctxt', st) |
654 |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm))) |
654 |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm))) |
655 | match_kind => |
655 | match_kind => |
656 if Thm.no_prems st then Seq.empty |
656 if Thm.no_prems st then Seq.empty |
657 else |
657 else |
658 let |
658 let |
719 I |
719 I |
720 |> Seq.map (pair outer_ctxt') |
720 |> Seq.map (pair outer_ctxt') |
721 end; |
721 end; |
722 |
722 |
723 fun apply_text (text, ctxt') = |
723 fun apply_text (text, ctxt') = |
724 Method_Closure.method_evaluate text ctxt' using (ctxt', focused_goal) |
724 Method.evaluate_runtime text ctxt' using (ctxt', focused_goal) |
725 |> Seq.filter_results |
725 |> Seq.filter_results |
726 |> Seq.maps (Seq.DETERM do_retrofit) |
726 |> Seq.maps (Seq.DETERM do_retrofit) |
727 |
727 |
728 in Seq.map apply_text texts end) |
728 in Seq.map apply_text texts end) |
729 end; |
729 end; |