equal
deleted
inserted
replaced
97 ( scan_cmt |
97 ( scan_cmt |
98 (Scan.this_string "(*{" |-- |
98 (Scan.this_string "(*{" |-- |
99 Scan.repeat (Scan.unless (Scan.this_string "}*)") |
99 Scan.repeat (Scan.unless (Scan.this_string "}*)") |
100 (Scan.one (not o Symbol.is_eof))) --| |
100 (Scan.one (not o Symbol.is_eof))) --| |
101 Scan.this_string "}*)" >> |
101 Scan.this_string "}*)" >> |
102 (enclose "\\hfill\\textrm{\\textit{" "}}" o implode)) |
102 (Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode)) |
103 || Scan.one not_eof >> ML_Lex.content_of)) #> |
103 || Scan.one not_eof >> ML_Lex.content_of)) #> |
104 fst; |
104 fst; |
105 |
105 |
106 fun output_chunk src ctxt name = |
106 fun output_chunk src ctxt name = |
107 let |
107 let |
122 toks''') |
122 toks''') |
123 else ("", tok :: toks''') |
123 else ("", tok :: toks''') |
124 end) |
124 end) |
125 val txt = spc ^ implode (transform_cmts toks') |
125 val txt = spc ^ implode (transform_cmts toks') |
126 in |
126 in |
127 ((if ! ThyOutput.source then str_of_source src else txt) |
127 txt |> split_lines |> |
128 |> (if ! ThyOutput.quotes then quote else I) |
128 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
129 |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}" |
|
130 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
|
131 end; |
129 end; |
132 |
130 |
133 val _ = ThyOutput.add_commands |
131 val _ = ThyOutput.add_commands |
134 [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)]; |
132 [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)]; |
135 |
133 |