# HG changeset patch
# User wenzelm
# Date 1482941409 -3600
# Node ID 7e119f32276a34659f072a2604d5b5c386c9ef73
# Parent  642b6105e6f4012adb88862eb2c96a44040bba75
clarified modules;

diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/General/codepoint.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -25,7 +25,7 @@
 
   def length(s: String): Int = iterator(s).length
 
-  trait Length extends isabelle.Length
+  trait Length extends Text.Length
   {
     protected def codepoint_length(c: Int): Int = 1
 
@@ -34,7 +34,7 @@
 
     def offset(s: String, i: Int): Option[Text.Offset] =
     {
-      if (i <= 0 || s.forall(_ < 0x80)) isabelle.Length.offset(s, i)
+      if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
       else {
         val length = s.length
         var offset = 0
diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/General/length.scala
--- a/src/Pure/General/length.scala	Wed Dec 28 17:02:38 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/*  Title:      Pure/General/length.scala
-    Author:     Makarius
-
-Text length wrt. encoding.
-*/
-
-package isabelle
-
-
-trait Length
-{
-  def apply(text: String): Int
-  def offset(text: String, i: Int): Option[Text.Offset]
-}
-
-object Length extends Length
-{
-  def apply(text: String): Int = text.length
-  def offset(text: String, i: Int): Option[Text.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)) + ")")
-}
diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/General/symbol.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -130,11 +130,11 @@
 
   def length(text: CharSequence): Int = iterator(text).length
 
-  object Length extends isabelle.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)) isabelle.Length.offset(text, i)
+      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
   }
diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -808,7 +808,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(_, Length))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Text.Length))
             Line.Node_Position(name, pos)
           }
 
diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -31,7 +31,7 @@
         case i => i
       }
 
-    def advance(text: String, text_length: Length): Position =
+    def advance(text: String, text_length: Text.Length): Position =
       if (text.isEmpty) this
       else {
         val lines = Library.split_lines(text)
@@ -107,7 +107,7 @@
       }
     override def hashCode(): Int = lines.hashCode
 
-    def position(text_offset: Text.Offset, text_length: Length): Position =
+    def position(text_offset: Text.Offset, text_length: Text.Length): Position =
     {
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
       {
@@ -123,12 +123,12 @@
       move(text_offset, 0, lines)
     }
 
-    def range(text_range: Text.Range, text_length: Length): Range =
+    def range(text_range: Text.Range, text_length: Text.Length): Range =
       Range(
         position(text_range.start, text_length),
         position(text_range.stop, text_length))
 
-    def offset(pos: Position, text_length: Length): Option[Text.Offset] =
+    def offset(pos: Position, text_length: Text.Length): Option[Text.Offset] =
     {
       val l = pos.line
       val c = pos.column
diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/PIDE/text.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -181,4 +181,32 @@
         (rest, remove(i, count, string))
       }
   }
+
+
+  /* text length wrt. encoding */
+
+  trait Length
+  {
+    def apply(text: String): Int
+    def offset(text: String, i: Int): Option[Text.Offset]
+  }
+
+  object Length extends Length
+  {
+    def apply(text: String): Int = text.length
+    def offset(text: String, i: Int): Option[Text.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)) + ")")
+  }
 }
diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/build-jars	Wed Dec 28 17:10:09 2016 +0100
@@ -49,7 +49,6 @@
   General/graphics_file.scala
   General/http_server.scala
   General/json.scala
-  General/length.scala
   General/linear_set.scala
   General/logger.scala
   General/long_name.scala
diff -r 642b6105e6f4 -r 7e119f32276a src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -13,7 +13,7 @@
 
 
 case class Document_Model(
-  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length,
+  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Text.Length,
   changed: Boolean = true,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {
diff -r 642b6105e6f4 -r 7e119f32276a src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -27,14 +27,14 @@
   {
     try {
       var log_file: Option[Path] = None
-      var text_length = Length.encoding(default_text_length)
+      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()
 
       def text_length_choice: String =
-        commas(Length.encodings.map(
+        commas(Text.Length.encodings.map(
           { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
 
       val getopts = Getopts("""
@@ -51,7 +51,7 @@
   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
 """,
         "L:" -> (arg => log_file = Some(Path.explode(arg))),
-        "T:" -> (arg => Length.encoding(arg)),
+        "T:" -> (arg => Text.Length.encoding(arg)),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
@@ -95,7 +95,7 @@
 class Server(
   channel: Channel,
   options: Options,
-  text_length: Length = Length.encoding(Server.default_text_length),
+  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)
diff -r 642b6105e6f4 -r 7e119f32276a src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -270,7 +270,8 @@
             JEdit_Lib.buffer_lock(buffer) {
               (Line.Position.zero /:
                 (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_, Length))
+                  zipWithIndex.takeWhile(p => p._2 < offset - 1).
+                  map(_._1)))(_.advance(_, Text.Length))
             }
           hyperlink_file(focus, Line.Node_Position(name, pos))
         case _ =>