# 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);