src/Pure/General/symbol_pos.ML

   val ~$$ : Symbol.symbol -> T list -> T * T list
   val $$$ : Symbol.symbol -> T list -> T list * T list
   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
   val scan_pos: T list -> Position.T * T list
   val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list

 fun range (syms as (_, pos) :: _) =
       let val pos' = List.last syms |-> Position.advance
       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 *)
 
 fun mk_eof pos = (Symbol.eof, pos);