equal
deleted
inserted
replaced
137 Scan.this_string "}*)" >> |
137 Scan.this_string "}*)" >> |
138 (Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode)) |
138 (Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode)) |
139 || Scan.one not_eof >> ML_Lex.content_of)) #> |
139 || Scan.one not_eof >> ML_Lex.content_of)) #> |
140 fst; |
140 fst; |
141 |
141 |
142 fun output_chunk src ctxt name = |
142 fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name = |
143 let |
143 let |
144 val toks = the_chunk (ProofContext.theory_of ctxt) name; |
144 val toks = the_chunk (ProofContext.theory_of ctxt) name; |
145 val (spc, toks') = (case toks of |
145 val (spc, toks') = (case toks of |
146 [] => ("", []) |
146 [] => ("", []) |
147 | [tok] => ("", [tok]) |
147 | [tok] => ("", [tok]) |
162 in |
162 in |
163 txt |> split_lines |> |
163 txt |> split_lines |> |
164 output_list (fn _ => fn s => Pretty.str s) src ctxt |
164 output_list (fn _ => fn s => Pretty.str s) src ctxt |
165 end; |
165 end; |
166 |
166 |
167 val _ = ThyOutput.add_commands |
167 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
168 [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)]; |
|
169 |
168 |
170 end; |
169 end; |