clarified modules;
authorwenzelm
Wed Dec 28 17:10:09 2016 +0100 (2016-12-28 ago)
changeset 646827e119f32276a
parent 64681 642b6105e6f4
child 64683 c0c09b6dfbe0
clarified modules;
src/Pure/General/codepoint.scala
src/Pure/General/length.scala
src/Pure/General/symbol.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/line.scala
src/Pure/PIDE/text.scala
src/Pure/build-jars
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/General/codepoint.scala	Wed Dec 28 17:02:38 2016 +0100
     1.2 +++ b/src/Pure/General/codepoint.scala	Wed Dec 28 17:10:09 2016 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5    def length(s: String): Int = iterator(s).length
     1.6  
     1.7 -  trait Length extends isabelle.Length
     1.8 +  trait Length extends Text.Length
     1.9    {
    1.10      protected def codepoint_length(c: Int): Int = 1
    1.11  
    1.12 @@ -34,7 +34,7 @@
    1.13  
    1.14      def offset(s: String, i: Int): Option[Text.Offset] =
    1.15      {
    1.16 -      if (i <= 0 || s.forall(_ < 0x80)) isabelle.Length.offset(s, i)
    1.17 +      if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
    1.18        else {
    1.19          val length = s.length
    1.20          var offset = 0
     2.1 --- a/src/Pure/General/length.scala	Wed Dec 28 17:02:38 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,33 +0,0 @@
     2.4 -/*  Title:      Pure/General/length.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Text length wrt. encoding.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -trait Length
    2.14 -{
    2.15 -  def apply(text: String): Int
    2.16 -  def offset(text: String, i: Int): Option[Text.Offset]
    2.17 -}
    2.18 -
    2.19 -object Length extends Length
    2.20 -{
    2.21 -  def apply(text: String): Int = text.length
    2.22 -  def offset(text: String, i: Int): Option[Text.Offset] =
    2.23 -    if (0 <= i && i <= text.length) Some(i) else None
    2.24 -
    2.25 -  val encodings: List[(String, Length)] =
    2.26 -    List(
    2.27 -      "UTF-16" -> Length,
    2.28 -      "UTF-8" -> UTF8.Length,
    2.29 -      "codepoints" -> Codepoint.Length,
    2.30 -      "symbols" -> Symbol.Length)
    2.31 -
    2.32 -  def encoding(name: String): Length =
    2.33 -    encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
    2.34 -      error("Bad text length encoding: " + quote(name) +
    2.35 -        " (expected " + commas_quote(encodings.map(_._1)) + ")")
    2.36 -}
     3.1 --- a/src/Pure/General/symbol.scala	Wed Dec 28 17:02:38 2016 +0100
     3.2 +++ b/src/Pure/General/symbol.scala	Wed Dec 28 17:10:09 2016 +0100
     3.3 @@ -130,11 +130,11 @@
     3.4  
     3.5    def length(text: CharSequence): Int = iterator(text).length
     3.6  
     3.7 -  object Length extends isabelle.Length
     3.8 +  object Length extends Text.Length
     3.9    {
    3.10      def apply(text: String): Int = length(text)
    3.11      def offset(text: String, i: Int): Option[Text.Offset] =
    3.12 -      if (i <= 0 || iterator(text).forall(s => s.length == 1)) isabelle.Length.offset(text, i)
    3.13 +      if (i <= 0 || iterator(text).forall(s => s.length == 1)) Text.Length.offset(text, i)
    3.14        else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
    3.15        else None
    3.16    }
     4.1 --- a/src/Pure/PIDE/document.scala	Wed Dec 28 17:02:38 2016 +0100
     4.2 +++ b/src/Pure/PIDE/document.scala	Wed Dec 28 17:10:09 2016 +0100
     4.3 @@ -808,7 +808,7 @@
     4.4                node.commands.iterator.takeWhile(_ != command).map(_.source) ++
     4.5                  (if (offset == 0) Iterator.empty
     4.6                   else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
     4.7 -            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Length))
     4.8 +            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Text.Length))
     4.9              Line.Node_Position(name, pos)
    4.10            }
    4.11  
     5.1 --- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:02:38 2016 +0100
     5.2 +++ b/src/Pure/PIDE/line.scala	Wed Dec 28 17:10:09 2016 +0100
     5.3 @@ -31,7 +31,7 @@
     5.4          case i => i
     5.5        }
     5.6  
     5.7 -    def advance(text: String, text_length: Length): Position =
     5.8 +    def advance(text: String, text_length: Text.Length): Position =
     5.9        if (text.isEmpty) this
    5.10        else {
    5.11          val lines = Library.split_lines(text)
    5.12 @@ -107,7 +107,7 @@
    5.13        }
    5.14      override def hashCode(): Int = lines.hashCode
    5.15  
    5.16 -    def position(text_offset: Text.Offset, text_length: Length): Position =
    5.17 +    def position(text_offset: Text.Offset, text_length: Text.Length): Position =
    5.18      {
    5.19        @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
    5.20        {
    5.21 @@ -123,12 +123,12 @@
    5.22        move(text_offset, 0, lines)
    5.23      }
    5.24  
    5.25 -    def range(text_range: Text.Range, text_length: Length): Range =
    5.26 +    def range(text_range: Text.Range, text_length: Text.Length): Range =
    5.27        Range(
    5.28          position(text_range.start, text_length),
    5.29          position(text_range.stop, text_length))
    5.30  
    5.31 -    def offset(pos: Position, text_length: Length): Option[Text.Offset] =
    5.32 +    def offset(pos: Position, text_length: Text.Length): Option[Text.Offset] =
    5.33      {
    5.34        val l = pos.line
    5.35        val c = pos.column
     6.1 --- a/src/Pure/PIDE/text.scala	Wed Dec 28 17:02:38 2016 +0100
     6.2 +++ b/src/Pure/PIDE/text.scala	Wed Dec 28 17:10:09 2016 +0100
     6.3 @@ -181,4 +181,32 @@
     6.4          (rest, remove(i, count, string))
     6.5        }
     6.6    }
     6.7 +
     6.8 +
     6.9 +  /* text length wrt. encoding */
    6.10 +
    6.11 +  trait Length
    6.12 +  {
    6.13 +    def apply(text: String): Int
    6.14 +    def offset(text: String, i: Int): Option[Text.Offset]
    6.15 +  }
    6.16 +
    6.17 +  object Length extends Length
    6.18 +  {
    6.19 +    def apply(text: String): Int = text.length
    6.20 +    def offset(text: String, i: Int): Option[Text.Offset] =
    6.21 +      if (0 <= i && i <= text.length) Some(i) else None
    6.22 +
    6.23 +    val encodings: List[(String, Length)] =
    6.24 +      List(
    6.25 +        "UTF-16" -> Length,
    6.26 +        "UTF-8" -> UTF8.Length,
    6.27 +        "codepoints" -> Codepoint.Length,
    6.28 +        "symbols" -> Symbol.Length)
    6.29 +
    6.30 +    def encoding(name: String): Length =
    6.31 +      encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
    6.32 +        error("Bad text length encoding: " + quote(name) +
    6.33 +          " (expected " + commas_quote(encodings.map(_._1)) + ")")
    6.34 +  }
    6.35  }
     7.1 --- a/src/Pure/build-jars	Wed Dec 28 17:02:38 2016 +0100
     7.2 +++ b/src/Pure/build-jars	Wed Dec 28 17:10:09 2016 +0100
     7.3 @@ -49,7 +49,6 @@
     7.4    General/graphics_file.scala
     7.5    General/http_server.scala
     7.6    General/json.scala
     7.7 -  General/length.scala
     7.8    General/linear_set.scala
     7.9    General/logger.scala
    7.10    General/long_name.scala
     8.1 --- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:02:38 2016 +0100
     8.2 +++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:10:09 2016 +0100
     8.3 @@ -13,7 +13,7 @@
     8.4  
     8.5  
     8.6  case class Document_Model(
     8.7 -  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length,
     8.8 +  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Text.Length,
     8.9    changed: Boolean = true,
    8.10    published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    8.11  {
     9.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:02:38 2016 +0100
     9.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:10:09 2016 +0100
     9.3 @@ -27,14 +27,14 @@
     9.4    {
     9.5      try {
     9.6        var log_file: Option[Path] = None
     9.7 -      var text_length = Length.encoding(default_text_length)
     9.8 +      var text_length = Text.Length.encoding(default_text_length)
     9.9        var dirs: List[Path] = Nil
    9.10        var logic = default_logic
    9.11        var modes: List[String] = Nil
    9.12        var options = Options.init()
    9.13  
    9.14        def text_length_choice: String =
    9.15 -        commas(Length.encodings.map(
    9.16 +        commas(Text.Length.encodings.map(
    9.17            { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
    9.18  
    9.19        val getopts = Getopts("""
    9.20 @@ -51,7 +51,7 @@
    9.21    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    9.22  """,
    9.23          "L:" -> (arg => log_file = Some(Path.explode(arg))),
    9.24 -        "T:" -> (arg => Length.encoding(arg)),
    9.25 +        "T:" -> (arg => Text.Length.encoding(arg)),
    9.26          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    9.27          "l:" -> (arg => logic = arg),
    9.28          "m:" -> (arg => modes = arg :: modes),
    9.29 @@ -95,7 +95,7 @@
    9.30  class Server(
    9.31    channel: Channel,
    9.32    options: Options,
    9.33 -  text_length: Length = Length.encoding(Server.default_text_length),
    9.34 +  text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
    9.35    session_name: String = Server.default_logic,
    9.36    session_dirs: List[Path] = Nil,
    9.37    modes: List[String] = Nil)
    10.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 17:02:38 2016 +0100
    10.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Dec 28 17:10:09 2016 +0100
    10.3 @@ -270,7 +270,8 @@
    10.4              JEdit_Lib.buffer_lock(buffer) {
    10.5                (Line.Position.zero /:
    10.6                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    10.7 -                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_, Length))
    10.8 +                  zipWithIndex.takeWhile(p => p._2 < offset - 1).
    10.9 +                  map(_._1)))(_.advance(_, Text.Length))
   10.10              }
   10.11            hyperlink_file(focus, Line.Node_Position(name, pos))
   10.12          case _ =>