changeset 61036 | f6f2959bed67 |
parent 60189 | 0d3a62127057 |
child 61457 | 3e21699bb83b |
--- a/src/Pure/pure_syn.ML Fri Aug 28 10:50:48 2015 +0200 +++ b/src/Pure/pure_syn.ML Fri Aug 28 11:09:26 2015 +0200 @@ -43,7 +43,7 @@ val _ = Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text" - (Parse.document_source >> K (Toplevel.keep (fn _ => ()))); + (Parse.document_source >> (fn s => Toplevel.keep (fn _ => Thy_Output.report_text s))); val _ = Outer_Syntax.command ("theory", @{here}) "begin theory"