src/Pure/PIDE/text.scala
changeset 64682 7e119f32276a
parent 64678 914dffe59cc5
child 64816 e306cab8edf9
equal deleted inserted replaced
64681:642b6105e6f4 64682:7e119f32276a
   179           if (count == text.length) None
   179           if (count == text.length) None
   180           else Some(Edit.remove(start, text.substring(count)))
   180           else Some(Edit.remove(start, text.substring(count)))
   181         (rest, remove(i, count, string))
   181         (rest, remove(i, count, string))
   182       }
   182       }
   183   }
   183   }
       
   184 
       
   185 
       
   186   /* text length wrt. encoding */
       
   187 
       
   188   trait Length
       
   189   {
       
   190     def apply(text: String): Int
       
   191     def offset(text: String, i: Int): Option[Text.Offset]
       
   192   }
       
   193 
       
   194   object Length extends Length
       
   195   {
       
   196     def apply(text: String): Int = text.length
       
   197     def offset(text: String, i: Int): Option[Text.Offset] =
       
   198       if (0 <= i && i <= text.length) Some(i) else None
       
   199 
       
   200     val encodings: List[(String, Length)] =
       
   201       List(
       
   202         "UTF-16" -> Length,
       
   203         "UTF-8" -> UTF8.Length,
       
   204         "codepoints" -> Codepoint.Length,
       
   205         "symbols" -> Symbol.Length)
       
   206 
       
   207     def encoding(name: String): Length =
       
   208       encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
       
   209         error("Bad text length encoding: " + quote(name) +
       
   210           " (expected " + commas_quote(encodings.map(_._1)) + ")")
       
   211   }
   184 }
   212 }