# HG changeset patch
# User wenzelm
# Date 1516308123 -3600
# Node ID bc8a76d5839a04874e12c2ca9e2cf43cdd2f4f03
# Parent  a5ca98950a914a0a28bee524c9770c7a71ac5a03
unused;

diff -r a5ca98950a91 -r bc8a76d5839a src/Pure/General/symbol_pos.ML
--- 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);