discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;

--- a/src/Pure/General/codepoint.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/General/codepoint.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -24,30 +24,4 @@
     }
 
   def length(s: String): Int = iterator(s).length
-
-  trait Length extends Text.Length
-  {
-    protected def codepoint_length(c: Int): Int = 1
-
-    def apply(s: String): Int =
-      (0 /: iterator(s)) { case (n, c) => n + codepoint_length(c) }
-
-    def offset(s: String, i: Int): Option[Text.Offset] =
-    {
-      if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
-      else {
-        val length = s.length
-        var offset = 0
-        var j = 0
-        while (offset < length && j < i) {
-          val c = s.codePointAt(offset)
-          offset += Character.charCount(c)
-          j += codepoint_length(c)
-        }
-        if (j >= i) Some(offset) else None
-      }
-    }
-  }
-
-  object Length extends Length
 }

--- a/src/Pure/General/symbol.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/General/symbol.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -130,15 +130,6 @@
 
   def length(text: CharSequence): Int = iterator(text).length
 
-  object Length extends Text.Length
-  {
-    def apply(text: String): Int = length(text)
-    def offset(text: String, i: Int): Option[Text.Offset] =
-      if (i <= 0 || iterator(text).forall(s => s.length == 1)) Text.Length.offset(text, i)
-      else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
-      else None
-  }
-
 
   /* decoding offsets */
 

--- a/src/Pure/General/utf8.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/General/utf8.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -21,15 +21,6 @@
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
-  object Length extends Codepoint.Length
-  {
-    override def codepoint_length(c: Int): Int =
-      if (c < 0x80) 1
-      else if (c < 0x800) 2
-      else if (c < 0x10000) 3
-      else 4
-  }
-
 
   /* permissive UTF-8 decoding */
 

--- a/src/Pure/PIDE/document.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -845,7 +845,7 @@
               node.commands.iterator.takeWhile(_ != command).map(_.source) ++
                 (if (offset == 0) Iterator.empty
                  else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Text.Length))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
             Line.Node_Position(name, pos)
           }
 

--- a/src/Pure/PIDE/line.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -40,12 +40,12 @@
         case i => i
       }
 
-    def advance(text: String, text_length: Text.Length): Position =
+    def advance(text: String): Position =
       if (text.isEmpty) this
       else {
         val lines = logical_lines(text)
         val l = line + lines.length - 1
-        val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
+        val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length
         Position(l, c)
       }
   }
@@ -89,12 +89,13 @@
 
   object Document
   {
-    def apply(text: String, text_length: Text.Length): Document =
-      Document(logical_lines(text).map(s => Line(Library.trim_substring(s))), text_length)
+    def apply(text: String): Document =
+      Document(logical_lines(text).map(s => Line(Library.trim_substring(s))))
+
+    val empty: Document = apply("")
 
     private def split(line_text: String): List[Line] =
-      if (line_text == "") List(Line.empty)
-      else apply(line_text, Text.Length).lines
+      if (line_text == "") List(Line.empty) else apply(line_text).lines
 
     private def chop(lines: List[Line]): (String, List[Line]) =
       lines match {
@@ -109,7 +110,7 @@
     def text(lines: List[Line]): String = lines.mkString("", "\n", "")
   }
 
-  sealed case class Document(lines: List[Line], text_length: Text.Length)
+  sealed case class Document(lines: List[Line])
   {
     lazy val text_range: Text.Range = Text.Range(0, Document.length(lines))
     lazy val text: String = Document.text(lines)
@@ -136,7 +137,7 @@
           case line :: ls =>
             val n = line.text.length
             if (ls.isEmpty || i <= n)
-              Position(lines_count).advance(line.text.substring(n - i), text_length)
+              Position(lines_count).advance(line.text.substring(n - i))
             else move(i - (n + 1), lines_count + 1, ls)
         }
       }
@@ -152,9 +153,12 @@
       val c = pos.column
       val n = lines.length
       if (0 <= l && l < n) {
-        val line_offset =
-          (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
-        text_length.offset(lines(l).text, c).map(line_offset + _)
+        if (0 <= c && c <= lines(l).text.length) {
+          val line_offset =
+            (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
+          Some(line_offset + c)
+        }
+        else None
       }
       else if (l == n && c == 0) Some(text_range.length)
       else None
@@ -170,49 +174,47 @@
         if l1 <= l2
         (removed_text, new_lines) <-
         {
+          val c1 = remove.start.column
+          val c2 = remove.stop.column
+
           val (prefix, lines1) = lines.splitAt(l1)
           val (s1, rest1) = Document.chop(lines1)
 
           if (l1 == l2) {
-            for {
-              c1 <- text_length.offset(s1, remove.start.column)
-              c2 <- text_length.offset(s1, remove.stop.column)
-              if c1 <= c2
+            if (0 <= c1 && c1 <= c2 && c2 <= s1.length) {
+              Some(
+                if (lines1.isEmpty) ("", prefix)
+                else {
+                  val removed_text = s1.substring(c1, c2)
+                  val changed_text = s1.substring(0, c1) + insert + s1.substring(c2)
+                  (removed_text, prefix ::: Document.split(changed_text) ::: rest1)
+                })
             }
-            yield {
-              if (lines1.isEmpty) ("", prefix)
-              else {
-                val removed_text = s1.substring(c1, c2)
-                val changed_text = s1.substring(0, c1) + insert + s1.substring(c2)
-                (removed_text, prefix ::: Document.split(changed_text) ::: rest1)
-              }
-            }
+            else None
           }
           else {
             val (middle, lines2) = rest1.splitAt(l2 - l1 - 1)
             val (s2, rest2) = Document.chop(lines2)
-            for {
-              c1 <- text_length.offset(s1, remove.start.column)
-              c2 <- text_length.offset(s2, remove.stop.column)
+            if (0 <= c1 && c1 <= s1.length && 0 <= c2 && c2 <= s2.length) {
+              Some(
+                if (lines1.isEmpty) ("", prefix)
+                else {
+                  val r1 = s1.substring(c1)
+                  val r2 = s2.substring(0, c2)
+                  val removed_text =
+                    if (lines2.isEmpty) Document.text(Line(r1) :: middle)
+                    else Document.text(Line(r1) :: middle ::: List(Line(r2)))
+                  val changed_text = s1.substring(0, c1) + insert + s2.substring(c2)
+                  (removed_text, prefix ::: Document.split(changed_text) ::: rest2)
+                })
             }
-            yield {
-              if (lines1.isEmpty) ("", prefix)
-              else {
-                val r1 = s1.substring(c1)
-                val r2 = s2.substring(0, c2)
-                val removed_text =
-                  if (lines2.isEmpty) Document.text(Line(r1) :: middle)
-                  else Document.text(Line(r1) :: middle ::: List(Line(r2)))
-                val changed_text = s1.substring(0, c1) + insert + s2.substring(c2)
-                (removed_text, prefix ::: Document.split(changed_text) ::: rest2)
-              }
-            }
+            else None
           }
         }
       }
       yield
         (Text.Edit.removes(edit_start, removed_text) ::: Text.Edit.inserts(edit_start, insert),
-          Document(new_lines, text_length))
+          Document(new_lines))
     }
   }
 

--- a/src/Pure/PIDE/text.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -190,32 +190,4 @@
         (rest, remove(i, count, string))
       }
   }
-
-
-  /* text length wrt. encoding */
-
-  trait Length
-  {
-    def apply(text: String): Int
-    def offset(text: String, i: Int): Option[Offset]
-  }
-
-  object Length extends Length
-  {
-    def apply(text: String): Int = text.length
-    def offset(text: String, i: Int): Option[Offset] =
-      if (0 <= i && i <= text.length) Some(i) else None
-
-    val encodings: List[(String, Length)] =
-      List(
-        "UTF-16" -> Length,
-        "UTF-8" -> UTF8.Length,
-        "codepoints" -> Codepoint.Length,
-        "symbols" -> Symbol.Length)
-
-    def encoding(name: String): Length =
-      encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
-        error("Bad text length encoding: " + quote(name) +
-          " (expected " + commas_quote(encodings.map(_._1)) + ")")
-  }
 }

--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -45,7 +45,7 @@
   def init(session: Session, node_name: Document.Node.Name): Document_Model =
   {
     val resources = session.resources.asInstanceOf[VSCode_Resources]
-    val content = Content(Line.Document("", resources.text_length))
+    val content = Content(Line.Document.empty)
     Document_Model(session, node_name, content)
   }
 }
@@ -111,7 +111,7 @@
         Text.Edit.replace(0, content.text, insert) match {
           case Nil => None
           case edits =>
-            val content1 = Document_Model.Content(Line.Document(insert, content.doc.text_length))
+            val content1 = Document_Model.Content(Line.Document(insert))
             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
         }
       case Some(remove) =>

--- a/src/Tools/VSCode/src/server.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -22,30 +22,23 @@
 {
   /* Isabelle tool wrapper */
 
-  private val default_text_length = "UTF-16"
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
 
   val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
   {
     try {
       var log_file: Option[Path] = None
-      var text_length = Text.Length.encoding(default_text_length)
       var dirs: List[Path] = Nil
       var logic = default_logic
       var modes: List[String] = Nil
       var options = Options.init()
       var system_mode = false
 
-      def text_length_choice: String =
-        commas(Text.Length.encodings.map(
-          { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
-
       val getopts = Getopts("""
 Usage: isabelle vscode_server [OPTIONS]
 
   Options are:
     -L FILE      enable logging on FILE
-    -T LENGTH    text length encoding: """ + text_length_choice + """
     -d DIR       include session directory
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -m MODE      add print mode for output
@@ -55,7 +48,6 @@
   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
 """,
         "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
-        "T:" -> (arg => Text.Length.encoding(arg)),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
         "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
@@ -67,7 +59,7 @@
 
       val log = Logger.make(log_file)
       val channel = new Channel(System.in, System.out, log)
-      val server = new Server(channel, options, text_length, logic, dirs, modes, system_mode, log)
+      val server = new Server(channel, options, logic, dirs, modes, system_mode, log)
 
       // prevent spurious garbage on the main protocol channel
       val orig_out = System.out
@@ -89,7 +81,6 @@
 class Server(
   val channel: Channel,
   options: Options,
-  text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
   session_name: String = Server.default_logic,
   session_dirs: List[Path] = Nil,
   modes: List[String] = Nil,
@@ -222,8 +213,7 @@
         }
 
         val base = Build.session_base(options, false, session_dirs, session_name)
-        val resources =
-          new VSCode_Resources(options, text_length, base, log)
+        val resources = new VSCode_Resources(options, base, log)
           {
             override def commit(change: Session.Change): Unit =
               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -200,7 +200,7 @@
           resources.get_file_content(file) match {
             case Some(text) =>
               val chunk = Symbol.Text_Chunk(text)
-              val doc = Line.Document(text, resources.text_length)
+              val doc = Line.Document(text)
               doc.range(chunk.decode(range))
             case _ =>
               Line.Range(Line.Position((line1 - 1) max 0))

--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -41,7 +41,6 @@
 
 class VSCode_Resources(
   val options: Options,
-  val text_length: Text.Length,
   base: Sessions.Base,
   log: Logger = No_Logger) extends Resources(base, log)
 {

--- a/src/Tools/jEdit/src/document_model.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -338,7 +338,7 @@
 
   def node_position(offset: Text.Offset): Line.Node_Position =
     Line.Node_Position(node_name.node,
-      Line.Position.zero.advance(content.text.substring(0, offset), Text.Length))
+      Line.Position.zero.advance(content.text.substring(0, offset)))
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -258,8 +258,7 @@
             hyperlink(
               (Line.Position.zero /:
                 (Symbol.iterator(text).
-                  zipWithIndex.takeWhile(p => p._2 < offset - 1).
-                  map(_._1)))(_.advance(_, Text.Length)))
+                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_)))
           case None =>
             hyperlink(Line.Position((line1 - 1) max 0))
         }