src/Pure/Thy/document_antiquotations.ML
changeset 61705 546e6494049f
parent 61704 3a010273df63
child 61748 fc53fbf9fe01
     1.1 --- a/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 20:55:40 2015 +0100
     1.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 22:06:14 2015 +0100
     1.3 @@ -70,7 +70,9 @@
     1.4  
     1.5            val keywords = Thy_Header.get_keywords' ctxt;
     1.6            val toks =
     1.7 -            Source.of_list (Input.source_explode source)
     1.8 +            Input.source_explode source
     1.9 +            |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
    1.10 +            |> Source.of_list
    1.11              |> Token.source' true keywords
    1.12              |> Source.exhaust;
    1.13            val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);