# HG changeset patch
# User wenzelm
# Date 1482224778 -3600
# Node ID 88211daacf93511885dbff01910b18cf852eb465
# Parent  d1ca9ce0d9e47e1e509de9687386c91e436ad402
unused;

diff -r d1ca9ce0d9e4 -r 88211daacf93 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Tue Dec 20 10:01:53 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Tue Dec 20 10:06:18 2016 +0100
@@ -44,9 +44,6 @@
     def advance(text: String): Position =
       if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
 
-    def advance_symbols(text: String): Position =
-      if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
-
     def advance_codepoints(text: String): Position =
       if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
   }
@@ -107,10 +104,9 @@
     }
 
     def position(i: Text.Offset): Position = position(_.advance(_), i)
-    def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
     def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
 
-    // FIXME symbols, codepoints
+    // FIXME codepoints
     def offset(pos: Position): Option[Text.Offset] =
     {
       val l = pos.line
@@ -136,7 +132,6 @@
 {
   require(text.forall(c => c != '\r' && c != '\n'))
 
-  lazy val length_symbols: Int = Symbol.iterator(text).length
   lazy val length_codepoints: Int = Codepoint.iterator(text).length
 
   override def equals(that: Any): Boolean =