merged
authorwenzelm
Tue Dec 20 18:11:42 2016 +0100 (2016-12-20)
changeset 6462014f938969779
parent 64608 20ccca53dd73
parent 64619 e3d9a31281f3
child 64621 7116f2634e32
merged
src/Tools/VSCode/src/line.scala
     1.1 --- a/src/Pure/Admin/check_sources.scala	Tue Dec 20 16:18:56 2016 +0100
     1.2 +++ b/src/Pure/Admin/check_sources.scala	Tue Dec 20 18:11:42 2016 +0100
     1.3 @@ -25,9 +25,9 @@
     1.4        try {
     1.5          Symbol.decode_strict(line)
     1.6  
     1.7 -        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
     1.8 +        for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
     1.9          {
    1.10 -          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
    1.11 +          Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
    1.12              Position.here(line_pos(i)))
    1.13          }
    1.14        }
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/codepoint.scala	Tue Dec 20 18:11:42 2016 +0100
     2.3 @@ -0,0 +1,53 @@
     2.4 +/*  Title:      Pure/General/codepoint.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Unicode codepoints vs. Unicode string encoding.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Codepoint
    2.14 +{
    2.15 +  def string(c: Int): String = new String(Array(c), 0, 1)
    2.16 +
    2.17 +  def iterator(s: String): Iterator[Int] =
    2.18 +    new Iterator[Int] {
    2.19 +      var offset = 0
    2.20 +      def hasNext: Boolean = offset < s.length
    2.21 +      def next: Int =
    2.22 +      {
    2.23 +        val c = s.codePointAt(offset)
    2.24 +        offset += Character.charCount(c)
    2.25 +        c
    2.26 +      }
    2.27 +    }
    2.28 +
    2.29 +  def length(s: String): Int = iterator(s).length
    2.30 +
    2.31 +  trait Length extends isabelle.Length
    2.32 +  {
    2.33 +    protected def codepoint_length(c: Int): Int = 1
    2.34 +
    2.35 +    def apply(s: String): Int =
    2.36 +      (0 /: iterator(s)) { case (n, c) => n + codepoint_length(c) }
    2.37 +
    2.38 +    def offset(s: String, i: Int): Option[Text.Offset] =
    2.39 +    {
    2.40 +      if (i <= 0 || s.forall(_ < 0x80)) isabelle.Length.offset(s, i)
    2.41 +      else {
    2.42 +        val length = s.length
    2.43 +        var offset = 0
    2.44 +        var j = 0
    2.45 +        while (offset < length && j < i) {
    2.46 +          val c = s.codePointAt(offset)
    2.47 +          offset += Character.charCount(c)
    2.48 +          j += codepoint_length(c)
    2.49 +        }
    2.50 +        if (j >= i) Some(offset) else None
    2.51 +      }
    2.52 +    }
    2.53 +  }
    2.54 +
    2.55 +  object Length extends Length
    2.56 +}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/length.scala	Tue Dec 20 18:11:42 2016 +0100
     3.3 @@ -0,0 +1,33 @@
     3.4 +/*  Title:      Pure/General/length.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Text length wrt. encoding.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +trait Length
    3.14 +{
    3.15 +  def apply(text: String): Int
    3.16 +  def offset(text: String, i: Int): Option[Text.Offset]
    3.17 +}
    3.18 +
    3.19 +object Length extends Length
    3.20 +{
    3.21 +  def apply(text: String): Int = text.length
    3.22 +  def offset(text: String, i: Int): Option[Text.Offset] =
    3.23 +    if (0 <= i && i <= text.length) Some(i) else None
    3.24 +
    3.25 +  val encodings: List[(String, Length)] =
    3.26 +    List(
    3.27 +      "UTF-16" -> Length,
    3.28 +      "UTF-8" -> UTF8.Length,
    3.29 +      "codepoints" -> Codepoint.Length,
    3.30 +      "symbols" -> Symbol.Length)
    3.31 +
    3.32 +  def encoding(name: String): Length =
    3.33 +    encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
    3.34 +      error("Bad text length encoding: " + quote(name) +
    3.35 +        " (expected " + commas_quote(encodings.map(_._1)) + ")")
    3.36 +}
     4.1 --- a/src/Pure/General/symbol.scala	Tue Dec 20 16:18:56 2016 +0100
     4.2 +++ b/src/Pure/General/symbol.scala	Tue Dec 20 18:11:42 2016 +0100
     4.3 @@ -128,14 +128,15 @@
     4.4  
     4.5    def explode(text: CharSequence): List[Symbol] = iterator(text).toList
     4.6  
     4.7 -  def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
     4.8 +  def length(text: CharSequence): Int = iterator(text).length
     4.9 +
    4.10 +  object Length extends isabelle.Length
    4.11    {
    4.12 -    var (line, column) = pos
    4.13 -    for (sym <- iterator(text)) {
    4.14 -      if (is_newline(sym)) { line += 1; column = 1 }
    4.15 -      else column += 1
    4.16 -    }
    4.17 -    (line, column)
    4.18 +    def apply(text: String): Int = length(text)
    4.19 +    def offset(text: String, i: Int): Option[Text.Offset] =
    4.20 +      if (i <= 0 || iterator(text).forall(s => s.length == 1)) isabelle.Length.offset(text, i)
    4.21 +      else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
    4.22 +      else None
    4.23    }
    4.24  
    4.25  
     5.1 --- a/src/Pure/General/word.scala	Tue Dec 20 16:18:56 2016 +0100
     5.2 +++ b/src/Pure/General/word.scala	Tue Dec 20 18:11:42 2016 +0100
     5.3 @@ -12,23 +12,6 @@
     5.4  
     5.5  object Word
     5.6  {
     5.7 -  /* codepoints */
     5.8 -
     5.9 -  def codepoint_iterator(str: String): Iterator[Int] =
    5.10 -    new Iterator[Int] {
    5.11 -      var offset = 0
    5.12 -      def hasNext: Boolean = offset < str.length
    5.13 -      def next: Int =
    5.14 -      {
    5.15 -        val c = str.codePointAt(offset)
    5.16 -        offset += Character.charCount(c)
    5.17 -        c
    5.18 -      }
    5.19 -    }
    5.20 -
    5.21 -  def codepoint(c: Int): String = new String(Array(c), 0, 1)
    5.22 -
    5.23 -
    5.24    /* directionality */
    5.25  
    5.26    def bidi_detect(str: String): Boolean =
    5.27 @@ -51,7 +34,7 @@
    5.28      }
    5.29  
    5.30    def perhaps_capitalize(str: String): String =
    5.31 -    if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
    5.32 +    if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
    5.33        capitalize(str)
    5.34      else str
    5.35  
    5.36 @@ -70,10 +53,10 @@
    5.37        }
    5.38      def unapply(str: String): Option[Case] =
    5.39        if (str.nonEmpty) {
    5.40 -        if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
    5.41 -        else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
    5.42 +        if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
    5.43 +        else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
    5.44          else {
    5.45 -          val it = codepoint_iterator(str)
    5.46 +          val it = Codepoint.iterator(str)
    5.47            if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
    5.48              Some(Capitalized)
    5.49            else None
     6.1 --- a/src/Pure/Isar/document_structure.scala	Tue Dec 20 16:18:56 2016 +0100
     6.2 +++ b/src/Pure/Isar/document_structure.scala	Tue Dec 20 18:11:42 2016 +0100
     6.3 @@ -190,8 +190,7 @@
     6.4          toks.filterNot(_.is_space) match {
     6.5            case List(tok) if tok.is_comment =>
     6.6              val s = tok.source
     6.7 -            if (Word.codepoint_iterator(s).exists(c =>
     6.8 -                  Character.isLetter(c) || Character.isDigit(c)))
     6.9 +            if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c)))
    6.10              {
    6.11                if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
    6.12                else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
     7.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 20 16:18:56 2016 +0100
     7.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 20 18:11:42 2016 +0100
     7.3 @@ -154,8 +154,8 @@
     7.4                val name = cmd.source
     7.5                val offset =
     7.6                  (0 /: span.takeWhile(_ != cmd)) {
     7.7 -                  case (i, tok) => i + Symbol.iterator(tok.source).length }
     7.8 -              val end_offset = offset + Symbol.iterator(name).length
     7.9 +                  case (i, tok) => i + Symbol.length(tok.source) }
    7.10 +              val end_offset = offset + Symbol.length(name)
    7.11                val pos = Position.Range(Text.Range(offset, end_offset) + 1)
    7.12                Command_Span.Command_Span(name, pos)
    7.13            }
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/PIDE/line.scala	Tue Dec 20 18:11:42 2016 +0100
     8.3 @@ -0,0 +1,134 @@
     8.4 +/*  Title:      Pure/PIDE/line.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Line-oriented text.
     8.8 +*/
     8.9 +
    8.10 +package isabelle
    8.11 +
    8.12 +
    8.13 +import scala.annotation.tailrec
    8.14 +
    8.15 +
    8.16 +object Line
    8.17 +{
    8.18 +  /* position */
    8.19 +
    8.20 +  object Position
    8.21 +  {
    8.22 +    val zero: Position = Position(0, 0)
    8.23 +  }
    8.24 +
    8.25 +  sealed case class Position(line: Int, column: Int)
    8.26 +  {
    8.27 +    def line1: Int = line + 1
    8.28 +    def column1: Int = column + 1
    8.29 +    def print: String = line1.toString + ":" + column1.toString
    8.30 +
    8.31 +    def compare(that: Position): Int =
    8.32 +      line compare that.line match {
    8.33 +        case 0 => column compare that.column
    8.34 +        case i => i
    8.35 +      }
    8.36 +
    8.37 +    def advance(text: String, length: Length = Length): Position =
    8.38 +      if (text.isEmpty) this
    8.39 +      else {
    8.40 +        val lines = Library.split_lines(text)
    8.41 +        val l = line + lines.length - 1
    8.42 +        val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
    8.43 +        Position(l, c)
    8.44 +      }
    8.45 +  }
    8.46 +
    8.47 +
    8.48 +  /* range (right-open interval) */
    8.49 +
    8.50 +  sealed case class Range(start: Position, stop: Position)
    8.51 +  {
    8.52 +    if (start.compare(stop) > 0)
    8.53 +      error("Bad line range: " + start.print + ".." + stop.print)
    8.54 +
    8.55 +    def print: String = start.print + ".." + stop.print
    8.56 +  }
    8.57 +
    8.58 +
    8.59 +  /* document with newline as separator (not terminator) */
    8.60 +
    8.61 +  object Document
    8.62 +  {
    8.63 +    val empty: Document = new Document("", Nil)
    8.64 +
    8.65 +    def apply(lines: List[Line]): Document =
    8.66 +      if (lines.isEmpty) empty
    8.67 +      else new Document(lines.mkString("", "\n", ""), lines)
    8.68 +
    8.69 +    def apply(text: String): Document =
    8.70 +      if (text.contains('\r'))
    8.71 +        apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
    8.72 +      else if (text == "") Document.empty
    8.73 +      else new Document(text, Library.split_lines(text).map(Line(_)))
    8.74 +  }
    8.75 +
    8.76 +  final class Document private(val text: String, val lines: List[Line])
    8.77 +  {
    8.78 +    override def toString: String = text
    8.79 +
    8.80 +    override def equals(that: Any): Boolean =
    8.81 +      that match {
    8.82 +        case other: Document => lines == other.lines
    8.83 +        case _ => false
    8.84 +      }
    8.85 +    override def hashCode(): Int = lines.hashCode
    8.86 +
    8.87 +    def position(offset: Text.Offset, length: Length = Length): Position =
    8.88 +    {
    8.89 +      @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
    8.90 +      {
    8.91 +        lines_rest match {
    8.92 +          case Nil => require(i == 0); Position(lines_count, 0)
    8.93 +          case line :: ls =>
    8.94 +            val n = line.text.length
    8.95 +            if (ls.isEmpty || i <= n)
    8.96 +              Position(lines_count, 0).advance(line.text.substring(n - i), length)
    8.97 +            else move(i - (n + 1), lines_count + 1, ls)
    8.98 +        }
    8.99 +      }
   8.100 +      move(offset, 0, lines)
   8.101 +    }
   8.102 +
   8.103 +    def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
   8.104 +    {
   8.105 +      val l = pos.line
   8.106 +      val c = pos.column
   8.107 +      if (0 <= l && l < lines.length) {
   8.108 +        val line_offset =
   8.109 +          if (l == 0) 0
   8.110 +          else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
   8.111 +        length.offset(lines(l).text, c).map(line_offset + _)
   8.112 +      }
   8.113 +      else None
   8.114 +    }
   8.115 +  }
   8.116 +
   8.117 +
   8.118 +  /* line text */
   8.119 +
   8.120 +  val empty: Line = new Line("")
   8.121 +  def apply(text: String): Line = if (text == "") empty else new Line(text)
   8.122 +}
   8.123 +
   8.124 +final class Line private(val text: String)
   8.125 +{
   8.126 +  require(text.forall(c => c != '\r' && c != '\n'))
   8.127 +
   8.128 +  lazy val length_codepoints: Int = Codepoint.iterator(text).length
   8.129 +
   8.130 +  override def equals(that: Any): Boolean =
   8.131 +    that match {
   8.132 +      case other: Line => text == other.text
   8.133 +      case _ => false
   8.134 +    }
   8.135 +  override def hashCode(): Int = text.hashCode
   8.136 +  override def toString: String = text
   8.137 +}
     9.1 --- a/src/Pure/PIDE/protocol.scala	Tue Dec 20 16:18:56 2016 +0100
     9.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Dec 20 18:11:42 2016 +0100
     9.3 @@ -337,8 +337,7 @@
     9.4      val toks_yxml =
     9.5      {
     9.6        import XML.Encode._
     9.7 -      val encode_tok: T[Token] =
     9.8 -        (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
     9.9 +      val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
    9.10        YXML.string_of_body(list(encode_tok)(toks))
    9.11      }
    9.12  
    10.1 --- a/src/Pure/System/utf8.scala	Tue Dec 20 16:18:56 2016 +0100
    10.2 +++ b/src/Pure/System/utf8.scala	Tue Dec 20 18:11:42 2016 +0100
    10.3 @@ -21,6 +21,15 @@
    10.4  
    10.5    def bytes(s: String): Array[Byte] = s.getBytes(charset)
    10.6  
    10.7 +  object Length extends Codepoint.Length
    10.8 +  {
    10.9 +    override def codepoint_length(c: Int): Int =
   10.10 +      if (c < 0x80) 1
   10.11 +      else if (c < 0x800) 2
   10.12 +      else if (c < 0x10000) 3
   10.13 +      else 4
   10.14 +  }
   10.15 +
   10.16  
   10.17    /* permissive UTF-8 decoding */
   10.18  
   10.19 @@ -88,4 +97,3 @@
   10.20      new Decode_Chars(decode, buffer, start, end)
   10.21    }
   10.22  }
   10.23 -
    11.1 --- a/src/Pure/build-jars	Tue Dec 20 16:18:56 2016 +0100
    11.2 +++ b/src/Pure/build-jars	Tue Dec 20 18:11:42 2016 +0100
    11.3 @@ -39,6 +39,7 @@
    11.4    GUI/wrap_panel.scala
    11.5    General/antiquote.scala
    11.6    General/bytes.scala
    11.7 +  General/codepoint.scala
    11.8    General/completion.scala
    11.9    General/date.scala
   11.10    General/exn.scala
   11.11 @@ -48,6 +49,7 @@
   11.12    General/graphics_file.scala
   11.13    General/http_server.scala
   11.14    General/json.scala
   11.15 +  General/length.scala
   11.16    General/linear_set.scala
   11.17    General/logger.scala
   11.18    General/long_name.scala
   11.19 @@ -85,6 +87,7 @@
   11.20    PIDE/document.scala
   11.21    PIDE/document_id.scala
   11.22    PIDE/editor.scala
   11.23 +  PIDE/line.scala
   11.24    PIDE/markup.scala
   11.25    PIDE/markup_tree.scala
   11.26    PIDE/protocol.scala
   11.27 @@ -141,25 +144,24 @@
   11.28    library.scala
   11.29    term.scala
   11.30    term_xml.scala
   11.31 -  "../Tools/Graphview/graph_file.scala"
   11.32 -  "../Tools/Graphview/graph_panel.scala"
   11.33 -  "../Tools/Graphview/graphview.scala"
   11.34 -  "../Tools/Graphview/layout.scala"
   11.35 -  "../Tools/Graphview/main_panel.scala"
   11.36 -  "../Tools/Graphview/metrics.scala"
   11.37 -  "../Tools/Graphview/model.scala"
   11.38 -  "../Tools/Graphview/mutator.scala"
   11.39 -  "../Tools/Graphview/mutator_dialog.scala"
   11.40 -  "../Tools/Graphview/mutator_event.scala"
   11.41 -  "../Tools/Graphview/popups.scala"
   11.42 -  "../Tools/Graphview/shapes.scala"
   11.43 -  "../Tools/Graphview/tree_panel.scala"
   11.44 -  "../Tools/VSCode/src/channel.scala"
   11.45 -  "../Tools/VSCode/src/document_model.scala"
   11.46 -  "../Tools/VSCode/src/line.scala"
   11.47 -  "../Tools/VSCode/src/protocol.scala"
   11.48 -  "../Tools/VSCode/src/server.scala"
   11.49 -  "../Tools/VSCode/src/uri_resources.scala"
   11.50 +  ../Tools/Graphview/graph_file.scala
   11.51 +  ../Tools/Graphview/graph_panel.scala
   11.52 +  ../Tools/Graphview/graphview.scala
   11.53 +  ../Tools/Graphview/layout.scala
   11.54 +  ../Tools/Graphview/main_panel.scala
   11.55 +  ../Tools/Graphview/metrics.scala
   11.56 +  ../Tools/Graphview/model.scala
   11.57 +  ../Tools/Graphview/mutator.scala
   11.58 +  ../Tools/Graphview/mutator_dialog.scala
   11.59 +  ../Tools/Graphview/mutator_event.scala
   11.60 +  ../Tools/Graphview/popups.scala
   11.61 +  ../Tools/Graphview/shapes.scala
   11.62 +  ../Tools/Graphview/tree_panel.scala
   11.63 +  ../Tools/VSCode/src/channel.scala
   11.64 +  ../Tools/VSCode/src/document_model.scala
   11.65 +  ../Tools/VSCode/src/protocol.scala
   11.66 +  ../Tools/VSCode/src/server.scala
   11.67 +  ../Tools/VSCode/src/uri_resources.scala
   11.68  )
   11.69  
   11.70  
    12.1 --- a/src/Tools/VSCode/src/line.scala	Tue Dec 20 16:18:56 2016 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,151 +0,0 @@
    12.4 -/*  Title:      Tools/VSCode/src/line.scala
    12.5 -    Author:     Makarius
    12.6 -
    12.7 -Line-oriented text.
    12.8 -*/
    12.9 -
   12.10 -package isabelle.vscode
   12.11 -
   12.12 -
   12.13 -import isabelle._
   12.14 -
   12.15 -import scala.annotation.tailrec
   12.16 -
   12.17 -
   12.18 -object Line
   12.19 -{
   12.20 -  /* position */
   12.21 -
   12.22 -  object Position
   12.23 -  {
   12.24 -    val zero: Position = Position(0, 0)
   12.25 -  }
   12.26 -
   12.27 -  sealed case class Position(line: Int, column: Int)
   12.28 -  {
   12.29 -    def line1: Int = line + 1
   12.30 -    def column1: Int = column + 1
   12.31 -    def print: String = line1.toString + ":" + column1.toString
   12.32 -
   12.33 -    def compare(that: Position): Int =
   12.34 -      line compare that.line match {
   12.35 -        case 0 => column compare that.column
   12.36 -        case i => i
   12.37 -      }
   12.38 -
   12.39 -    private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position =
   12.40 -    {
   12.41 -      var l = line
   12.42 -      var c = column
   12.43 -      for (x <- iterator) {
   12.44 -        if (is_newline(x)) { l += 1; c = 0 } else c += 1
   12.45 -      }
   12.46 -      Position(l, c)
   12.47 -    }
   12.48 -
   12.49 -    def advance(text: String): Position =
   12.50 -      if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
   12.51 -
   12.52 -    def advance_symbols(text: String): Position =
   12.53 -      if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
   12.54 -
   12.55 -    def advance_codepoints(text: String): Position =
   12.56 -      if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10)
   12.57 -  }
   12.58 -
   12.59 -
   12.60 -  /* range (right-open interval) */
   12.61 -
   12.62 -  sealed case class Range(start: Position, stop: Position)
   12.63 -  {
   12.64 -    if (start.compare(stop) > 0)
   12.65 -      error("Bad line range: " + start.print + ".." + stop.print)
   12.66 -
   12.67 -    def print: String = start.print + ".." + stop.print
   12.68 -  }
   12.69 -
   12.70 -
   12.71 -  /* document with newline as separator (not terminator) */
   12.72 -
   12.73 -  object Document
   12.74 -  {
   12.75 -    val empty: Document = new Document("", Nil)
   12.76 -
   12.77 -    def apply(lines: List[Line]): Document =
   12.78 -      if (lines.isEmpty) empty
   12.79 -      else new Document(lines.mkString("", "\n", ""), lines)
   12.80 -
   12.81 -    def apply(text: String): Document =
   12.82 -      if (text.contains('\r'))
   12.83 -        apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
   12.84 -      else if (text == "") Document.empty
   12.85 -      else new Document(text, Library.split_lines(text).map(Line(_)))
   12.86 -  }
   12.87 -
   12.88 -  final class Document private(val text: String, val lines: List[Line])
   12.89 -  {
   12.90 -    override def toString: String = text
   12.91 -
   12.92 -    override def equals(that: Any): Boolean =
   12.93 -      that match {
   12.94 -        case other: Document => lines == other.lines
   12.95 -        case _ => false
   12.96 -      }
   12.97 -    override def hashCode(): Int = lines.hashCode
   12.98 -
   12.99 -    private def position(advance: (Position, String) => Position, offset: Text.Offset): Position =
  12.100 -    {
  12.101 -      @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
  12.102 -      {
  12.103 -        lines_rest match {
  12.104 -          case Nil => require(i == 0); Position(lines_count, 0)
  12.105 -          case line :: ls =>
  12.106 -            val n = line.text.length
  12.107 -            if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i))
  12.108 -            else move(i - (n + 1), lines_count + 1, ls)
  12.109 -        }
  12.110 -      }
  12.111 -      move(offset, 0, lines)
  12.112 -    }
  12.113 -
  12.114 -    def position(i: Text.Offset): Position = position(_.advance(_), i)
  12.115 -    def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
  12.116 -    def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
  12.117 -
  12.118 -    // FIXME symbols, codepoints
  12.119 -    def offset(pos: Position): Option[Text.Offset] =
  12.120 -    {
  12.121 -      val l = pos.line
  12.122 -      val c = pos.column
  12.123 -      if (0 <= l && l < lines.length) {
  12.124 -        val line_offset =
  12.125 -          if (l == 0) 0
  12.126 -          else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 })
  12.127 -        if (c <= lines(l).text.length) Some(line_offset + c) else None
  12.128 -      }
  12.129 -      else None
  12.130 -    }
  12.131 -  }
  12.132 -
  12.133 -
  12.134 -  /* line text */
  12.135 -
  12.136 -  val empty: Line = new Line("")
  12.137 -  def apply(text: String): Line = if (text == "") empty else new Line(text)
  12.138 -}
  12.139 -
  12.140 -final class Line private(val text: String)
  12.141 -{
  12.142 -  require(text.forall(c => c != '\r' && c != '\n'))
  12.143 -
  12.144 -  lazy val length_symbols: Int = Symbol.iterator(text).length
  12.145 -  lazy val length_codepoints: Int = Word.codepoint_iterator(text).length
  12.146 -
  12.147 -  override def equals(that: Any): Boolean =
  12.148 -    that match {
  12.149 -      case other: Line => text == other.text
  12.150 -      case _ => false
  12.151 -    }
  12.152 -  override def hashCode(): Int = text.hashCode
  12.153 -  override def toString: String = text
  12.154 -}
    13.1 --- a/src/Tools/VSCode/src/server.scala	Tue Dec 20 16:18:56 2016 +0100
    13.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Dec 20 18:11:42 2016 +0100
    13.3 @@ -20,21 +20,28 @@
    13.4  {
    13.5    /* Isabelle tool wrapper */
    13.6  
    13.7 +  private val default_text_length = "UTF-16"
    13.8    private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    13.9  
   13.10    val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
   13.11    {
   13.12      var log_file: Option[Path] = None
   13.13 +    var text_length = Length.encoding(default_text_length)
   13.14      var dirs: List[Path] = Nil
   13.15      var logic = default_logic
   13.16      var modes: List[String] = Nil
   13.17      var options = Options.init()
   13.18  
   13.19 +    def text_length_choice: String =
   13.20 +      commas(Length.encodings.map(
   13.21 +        { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
   13.22 +
   13.23      val getopts = Getopts("""
   13.24  Usage: isabelle vscode_server [OPTIONS]
   13.25  
   13.26    Options are:
   13.27      -L FILE      enable logging on FILE
   13.28 +    -T LENGTH    text length encoding: """ + text_length_choice + """
   13.29      -d DIR       include session directory
   13.30      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   13.31      -m MODE      add print mode for output
   13.32 @@ -43,6 +50,7 @@
   13.33    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
   13.34  """,
   13.35        "L:" -> (arg => log_file = Some(Path.explode(arg))),
   13.36 +      "T:" -> (arg => Length.encoding(arg)),
   13.37        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   13.38        "l:" -> (arg => logic = arg),
   13.39        "m:" -> (arg => modes = arg :: modes),
   13.40 @@ -56,7 +64,7 @@
   13.41        error("Missing logic image " + quote(logic))
   13.42  
   13.43      val channel = new Channel(System.in, System.out, log_file)
   13.44 -    val server = new Server(channel, options, logic, dirs, modes)
   13.45 +    val server = new Server(channel, options, text_length, logic, dirs, modes)
   13.46  
   13.47      // prevent spurious garbage on the main protocol channel
   13.48      val orig_out = System.out
   13.49 @@ -78,6 +86,7 @@
   13.50  class Server(
   13.51    channel: Channel,
   13.52    options: Options,
   13.53 +  text_length: Length = Length.encoding(Server.default_text_length),
   13.54    session_name: String = Server.default_logic,
   13.55    session_dirs: List[Path] = Nil,
   13.56    modes: List[String] = Nil)
   13.57 @@ -185,12 +194,13 @@
   13.58      for {
   13.59        model <- state.value.models.get(uri)
   13.60        snapshot = model.snapshot()
   13.61 -      offset <- model.doc.offset(pos)
   13.62 +      offset <- model.doc.offset(pos, text_length)
   13.63        info <- tooltip(snapshot, Text.Range(offset, offset + 1))
   13.64      } yield {
   13.65 -      val r = Line.Range(model.doc.position(info.range.start), model.doc.position(info.range.stop))
   13.66 +      val start = model.doc.position(info.range.start, text_length)
   13.67 +      val stop = model.doc.position(info.range.stop, text_length)
   13.68        val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
   13.69 -      (r, List("```\n" + s + "\n```"))
   13.70 +      (Line.Range(start, stop), List("```\n" + s + "\n```"))
   13.71      }
   13.72  
   13.73    private val tooltip_descriptions =
    14.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 16:18:56 2016 +0100
    14.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 18:11:42 2016 +0100
    14.3 @@ -269,14 +269,13 @@
    14.4        case Some(name) =>
    14.5          JEdit_Lib.jedit_buffer(name) match {
    14.6            case Some(buffer) if offset > 0 =>
    14.7 -            val (line, column) =
    14.8 +            val pos =
    14.9                JEdit_Lib.buffer_lock(buffer) {
   14.10 -                ((1, 1) /:
   14.11 +                (Line.Position.zero /:
   14.12                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
   14.13 -                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
   14.14 -                      Symbol.advance_line_column)
   14.15 +                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
   14.16                }
   14.17 -            Some(hyperlink_file(focus, name, line, column))
   14.18 +            Some(hyperlink_file(focus, name, pos.line1, pos.column1))
   14.19            case _ => Some(hyperlink_file(focus, name, line))
   14.20          }
   14.21        case None => None
   14.22 @@ -297,8 +296,8 @@
   14.23              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   14.24                (if (offset == 0) Iterator.empty
   14.25                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
   14.26 -          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
   14.27 -          Some(hyperlink_file(focus, file_name, line, column))
   14.28 +          val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
   14.29 +          Some(hyperlink_file(focus, file_name, pos.line1, pos.column1))
   14.30        }
   14.31      }
   14.32    }