equal
deleted
inserted
replaced
53 | SOME NONE => Seq.empty |
53 | SOME NONE => Seq.empty |
54 | NONE => v); |
54 | NONE => v); |
55 \<close> |
55 \<close> |
56 |
56 |
57 method_setup catch = \<open> |
57 method_setup catch = \<open> |
58 Method_Closure.parse_method -- Method_Closure.parse_method >> |
58 Method_Closure.method_text -- Method_Closure.method_text >> |
59 (fn (text, text') => fn ctxt => fn using => fn st => |
59 (fn (text, text') => fn ctxt => fn using => fn st => |
60 let |
60 let |
61 val method = Method_Closure.method_evaluate text ctxt using; |
61 val method = Method_Closure.method_evaluate text ctxt using; |
62 val backup_results = Method_Closure.method_evaluate text' ctxt using st; |
62 val backup_results = Method_Closure.method_evaluate text' ctxt using st; |
63 in |
63 in |