# HG changeset patch
# User wenzelm
# Date 1447967174 -3600
# Node ID 546e6494049fa547e3175a9adbc97989cad6109c
# Parent  3a010273df639e47105928b418f635d3fd33a0bf
trim lines for @{theory_text} similarly to @{text};

diff -r 3a010273df63 -r 546e6494049f src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Thu Nov 19 20:55:40 2015 +0100
+++ b/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:06:14 2015 +0100
@@ -14,7 +14,9 @@
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   val content: T list -> string
   val range: T list -> Position.range
+  val split_lines: T list -> T list list
   val trim_blanks: T list -> T list
+  val trim_lines: T list -> T list
   val is_eof: T -> bool
   val stopper: T Scan.stopper
   val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
@@ -60,10 +62,25 @@
       in Position.range pos pos' end
   | range [] = Position.no_range;
 
+
+(* lines and blanks *)
+
+fun split_lines [] = []
+  | split_lines (list: T list) =
+      let
+        fun split syms =
+          (case take_prefix (fn (s, _) => s <> "\n") syms of
+            (line, []) => [line]
+          | (line, nl :: rest) => line :: split rest);
+      in split list end;
+
 val trim_blanks =
   take_prefix (Symbol.is_blank o symbol) #> #2 #>
   take_suffix (Symbol.is_blank o symbol) #> #1;
 
+val trim_lines =
+  split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
+
 
 (* stopper *)
 
diff -r 3a010273df63 -r 546e6494049f src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 20:55:40 2015 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 22:06:14 2015 +0100
@@ -70,7 +70,9 @@
 
           val keywords = Thy_Header.get_keywords' ctxt;
           val toks =
-            Source.of_list (Input.source_explode source)
+            Input.source_explode source
+            |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
+            |> Source.of_list
             |> Token.source' true keywords
             |> Source.exhaust;
           val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);