--- a/src/Pure/General/symbol_pos.ML Thu Jan 18 21:41:30 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML Thu Jan 18 21:42:03 2018 +0100
@@ -11,9 +11,6 @@
val symbol: T -> Symbol.symbol
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 -> 'a scanner -> 'a scanner
@@ -69,23 +66,6 @@
| 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, _ :: rest) => line :: split rest);
- in split list end;
-
-val trim_blanks = trim (Symbol.is_blank o symbol);
-
-val trim_lines =
- split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
-
-
(* stopper *)
fun mk_eof pos = (Symbol.eof, pos);