trim lines for @{theory_text} similarly to @{text};
authorwenzelm
Thu Nov 19 22:06:14 2015 +0100 (2015-11-19)
changeset 61705546e6494049f
parent 61704 3a010273df63
child 61706 a1510dfb9bfa
trim lines for @{theory_text} similarly to @{text};
src/Pure/General/symbol_pos.ML
src/Pure/Thy/document_antiquotations.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Nov 19 20:55:40 2015 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:06:14 2015 +0100
     1.3 @@ -14,7 +14,9 @@
     1.4    val ~$$$ : Symbol.symbol -> T list -> T list * T list
     1.5    val content: T list -> string
     1.6    val range: T list -> Position.range
     1.7 +  val split_lines: T list -> T list list
     1.8    val trim_blanks: T list -> T list
     1.9 +  val trim_lines: T list -> T list
    1.10    val is_eof: T -> bool
    1.11    val stopper: T Scan.stopper
    1.12    val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
    1.13 @@ -60,10 +62,25 @@
    1.14        in Position.range pos pos' end
    1.15    | range [] = Position.no_range;
    1.16  
    1.17 +
    1.18 +(* lines and blanks *)
    1.19 +
    1.20 +fun split_lines [] = []
    1.21 +  | split_lines (list: T list) =
    1.22 +      let
    1.23 +        fun split syms =
    1.24 +          (case take_prefix (fn (s, _) => s <> "\n") syms of
    1.25 +            (line, []) => [line]
    1.26 +          | (line, nl :: rest) => line :: split rest);
    1.27 +      in split list end;
    1.28 +
    1.29  val trim_blanks =
    1.30    take_prefix (Symbol.is_blank o symbol) #> #2 #>
    1.31    take_suffix (Symbol.is_blank o symbol) #> #1;
    1.32  
    1.33 +val trim_lines =
    1.34 +  split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
    1.35 +
    1.36  
    1.37  (* stopper *)
    1.38  
     2.1 --- a/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 20:55:40 2015 +0100
     2.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 22:06:14 2015 +0100
     2.3 @@ -70,7 +70,9 @@
     2.4  
     2.5            val keywords = Thy_Header.get_keywords' ctxt;
     2.6            val toks =
     2.7 -            Source.of_list (Input.source_explode source)
     2.8 +            Input.source_explode source
     2.9 +            |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
    2.10 +            |> Source.of_list
    2.11              |> Token.source' true keywords
    2.12              |> Source.exhaust;
    2.13            val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);