equal
deleted
inserted
replaced
117 val _ = |
117 val _ = |
118 Theory.setup |
118 Theory.setup |
119 (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input) |
119 (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input) |
120 (fn {context = ctxt, argument, ...} => |
120 (fn {context = ctxt, argument, ...} => |
121 ctxt |> Context.proof_map |
121 ctxt |> Context.proof_map |
122 (ML_Context.expression ("result", Position.thread_data ()) |
122 (ML_Context.expression (Input.pos_of argument) |
123 "string" "Context.map_proof (GHC.set_result result)" |
123 (ML_Lex.read "Theory.local_setup (GHC.set_result (" @ |
124 (ML_Lex.read_source argument)) |
124 ML_Lex.read_source argument @ ML_Lex.read "))")) |
125 |> the_result |> print_string)); |
125 |> the_result |> print_string)); |
126 |
126 |
127 end; |
127 end; |