--- a/src/Pure/Admin/check_sources.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/Admin/check_sources.scala Tue Dec 20 18:11:42 2016 +0100
@@ -25,9 +25,9 @@
try {
Symbol.decode_strict(line)
- for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
+ for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
{
- Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
+ Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
Position.here(line_pos(i)))
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/codepoint.scala Tue Dec 20 18:11:42 2016 +0100
@@ -0,0 +1,53 @@
+/* Title: Pure/General/codepoint.scala
+ Author: Makarius
+
+Unicode codepoints vs. Unicode string encoding.
+*/
+
+package isabelle
+
+
+object Codepoint
+{
+ def string(c: Int): String = new String(Array(c), 0, 1)
+
+ def iterator(s: String): Iterator[Int] =
+ new Iterator[Int] {
+ var offset = 0
+ def hasNext: Boolean = offset < s.length
+ def next: Int =
+ {
+ val c = s.codePointAt(offset)
+ offset += Character.charCount(c)
+ c
+ }
+ }
+
+ def length(s: String): Int = iterator(s).length
+
+ trait Length extends isabelle.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)) isabelle.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
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/length.scala Tue Dec 20 18:11:42 2016 +0100
@@ -0,0 +1,33 @@
+/* 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)) + ")")
+}
--- a/src/Pure/General/symbol.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/General/symbol.scala Tue Dec 20 18:11:42 2016 +0100
@@ -128,14 +128,15 @@
def explode(text: CharSequence): List[Symbol] = iterator(text).toList
- def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
+ def length(text: CharSequence): Int = iterator(text).length
+
+ object Length extends isabelle.Length
{
- var (line, column) = pos
- for (sym <- iterator(text)) {
- if (is_newline(sym)) { line += 1; column = 1 }
- else column += 1
- }
- (line, column)
+ 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)
+ else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
+ else None
}
--- a/src/Pure/General/word.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/General/word.scala Tue Dec 20 18:11:42 2016 +0100
@@ -12,23 +12,6 @@
object Word
{
- /* codepoints */
-
- def codepoint_iterator(str: String): Iterator[Int] =
- new Iterator[Int] {
- var offset = 0
- def hasNext: Boolean = offset < str.length
- def next: Int =
- {
- val c = str.codePointAt(offset)
- offset += Character.charCount(c)
- c
- }
- }
-
- def codepoint(c: Int): String = new String(Array(c), 0, 1)
-
-
/* directionality */
def bidi_detect(str: String): Boolean =
@@ -51,7 +34,7 @@
}
def perhaps_capitalize(str: String): String =
- if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
+ if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
capitalize(str)
else str
@@ -70,10 +53,10 @@
}
def unapply(str: String): Option[Case] =
if (str.nonEmpty) {
- if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
- else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
+ if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
+ else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
else {
- val it = codepoint_iterator(str)
+ val it = Codepoint.iterator(str)
if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
Some(Capitalized)
else None
--- a/src/Pure/Isar/document_structure.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/Isar/document_structure.scala Tue Dec 20 18:11:42 2016 +0100
@@ -190,8 +190,7 @@
toks.filterNot(_.is_space) match {
case List(tok) if tok.is_comment =>
val s = tok.source
- if (Word.codepoint_iterator(s).exists(c =>
- Character.isLetter(c) || Character.isDigit(c)))
+ if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c)))
{
if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
--- a/src/Pure/Isar/outer_syntax.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Tue Dec 20 18:11:42 2016 +0100
@@ -154,8 +154,8 @@
val name = cmd.source
val offset =
(0 /: span.takeWhile(_ != cmd)) {
- case (i, tok) => i + Symbol.iterator(tok.source).length }
- val end_offset = offset + Symbol.iterator(name).length
+ case (i, tok) => i + Symbol.length(tok.source) }
+ val end_offset = offset + Symbol.length(name)
val pos = Position.Range(Text.Range(offset, end_offset) + 1)
Command_Span.Command_Span(name, pos)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/line.scala Tue Dec 20 18:11:42 2016 +0100
@@ -0,0 +1,134 @@
+/* Title: Pure/PIDE/line.scala
+ Author: Makarius
+
+Line-oriented text.
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+
+object Line
+{
+ /* position */
+
+ object Position
+ {
+ val zero: Position = Position(0, 0)
+ }
+
+ sealed case class Position(line: Int, column: Int)
+ {
+ def line1: Int = line + 1
+ def column1: Int = column + 1
+ def print: String = line1.toString + ":" + column1.toString
+
+ def compare(that: Position): Int =
+ line compare that.line match {
+ case 0 => column compare that.column
+ case i => i
+ }
+
+ def advance(text: String, length: Length = Length): Position =
+ if (text.isEmpty) this
+ else {
+ val lines = Library.split_lines(text)
+ val l = line + lines.length - 1
+ val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
+ Position(l, c)
+ }
+ }
+
+
+ /* range (right-open interval) */
+
+ sealed case class Range(start: Position, stop: Position)
+ {
+ if (start.compare(stop) > 0)
+ error("Bad line range: " + start.print + ".." + stop.print)
+
+ def print: String = start.print + ".." + stop.print
+ }
+
+
+ /* document with newline as separator (not terminator) */
+
+ object Document
+ {
+ val empty: Document = new Document("", Nil)
+
+ def apply(lines: List[Line]): Document =
+ if (lines.isEmpty) empty
+ else new Document(lines.mkString("", "\n", ""), lines)
+
+ def apply(text: String): Document =
+ if (text.contains('\r'))
+ apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
+ else if (text == "") Document.empty
+ else new Document(text, Library.split_lines(text).map(Line(_)))
+ }
+
+ final class Document private(val text: String, val lines: List[Line])
+ {
+ override def toString: String = text
+
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Document => lines == other.lines
+ case _ => false
+ }
+ override def hashCode(): Int = lines.hashCode
+
+ def position(offset: Text.Offset, length: Length = Length): Position =
+ {
+ @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
+ {
+ lines_rest match {
+ case Nil => require(i == 0); Position(lines_count, 0)
+ case line :: ls =>
+ val n = line.text.length
+ if (ls.isEmpty || i <= n)
+ Position(lines_count, 0).advance(line.text.substring(n - i), length)
+ else move(i - (n + 1), lines_count + 1, ls)
+ }
+ }
+ move(offset, 0, lines)
+ }
+
+ def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
+ {
+ val l = pos.line
+ val c = pos.column
+ if (0 <= l && l < lines.length) {
+ val line_offset =
+ if (l == 0) 0
+ else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
+ length.offset(lines(l).text, c).map(line_offset + _)
+ }
+ else None
+ }
+ }
+
+
+ /* line text */
+
+ val empty: Line = new Line("")
+ def apply(text: String): Line = if (text == "") empty else new Line(text)
+}
+
+final class Line private(val text: String)
+{
+ require(text.forall(c => c != '\r' && c != '\n'))
+
+ lazy val length_codepoints: Int = Codepoint.iterator(text).length
+
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Line => text == other.text
+ case _ => false
+ }
+ override def hashCode(): Int = text.hashCode
+ override def toString: String = text
+}
--- a/src/Pure/PIDE/protocol.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Dec 20 18:11:42 2016 +0100
@@ -337,8 +337,7 @@
val toks_yxml =
{
import XML.Encode._
- val encode_tok: T[Token] =
- (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
+ val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
YXML.string_of_body(list(encode_tok)(toks))
}
--- a/src/Pure/System/utf8.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/System/utf8.scala Tue Dec 20 18:11:42 2016 +0100
@@ -21,6 +21,15 @@
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 */
@@ -88,4 +97,3 @@
new Decode_Chars(decode, buffer, start, end)
}
}
-
--- a/src/Pure/build-jars Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Pure/build-jars Tue Dec 20 18:11:42 2016 +0100
@@ -39,6 +39,7 @@
GUI/wrap_panel.scala
General/antiquote.scala
General/bytes.scala
+ General/codepoint.scala
General/completion.scala
General/date.scala
General/exn.scala
@@ -48,6 +49,7 @@
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
@@ -85,6 +87,7 @@
PIDE/document.scala
PIDE/document_id.scala
PIDE/editor.scala
+ PIDE/line.scala
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
@@ -141,25 +144,24 @@
library.scala
term.scala
term_xml.scala
- "../Tools/Graphview/graph_file.scala"
- "../Tools/Graphview/graph_panel.scala"
- "../Tools/Graphview/graphview.scala"
- "../Tools/Graphview/layout.scala"
- "../Tools/Graphview/main_panel.scala"
- "../Tools/Graphview/metrics.scala"
- "../Tools/Graphview/model.scala"
- "../Tools/Graphview/mutator.scala"
- "../Tools/Graphview/mutator_dialog.scala"
- "../Tools/Graphview/mutator_event.scala"
- "../Tools/Graphview/popups.scala"
- "../Tools/Graphview/shapes.scala"
- "../Tools/Graphview/tree_panel.scala"
- "../Tools/VSCode/src/channel.scala"
- "../Tools/VSCode/src/document_model.scala"
- "../Tools/VSCode/src/line.scala"
- "../Tools/VSCode/src/protocol.scala"
- "../Tools/VSCode/src/server.scala"
- "../Tools/VSCode/src/uri_resources.scala"
+ ../Tools/Graphview/graph_file.scala
+ ../Tools/Graphview/graph_panel.scala
+ ../Tools/Graphview/graphview.scala
+ ../Tools/Graphview/layout.scala
+ ../Tools/Graphview/main_panel.scala
+ ../Tools/Graphview/metrics.scala
+ ../Tools/Graphview/model.scala
+ ../Tools/Graphview/mutator.scala
+ ../Tools/Graphview/mutator_dialog.scala
+ ../Tools/Graphview/mutator_event.scala
+ ../Tools/Graphview/popups.scala
+ ../Tools/Graphview/shapes.scala
+ ../Tools/Graphview/tree_panel.scala
+ ../Tools/VSCode/src/channel.scala
+ ../Tools/VSCode/src/document_model.scala
+ ../Tools/VSCode/src/protocol.scala
+ ../Tools/VSCode/src/server.scala
+ ../Tools/VSCode/src/uri_resources.scala
)
--- a/src/Tools/VSCode/src/line.scala Tue Dec 20 16:18:56 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-/* Title: Tools/VSCode/src/line.scala
- Author: Makarius
-
-Line-oriented text.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-import scala.annotation.tailrec
-
-
-object Line
-{
- /* position */
-
- object Position
- {
- val zero: Position = Position(0, 0)
- }
-
- sealed case class Position(line: Int, column: Int)
- {
- def line1: Int = line + 1
- def column1: Int = column + 1
- def print: String = line1.toString + ":" + column1.toString
-
- def compare(that: Position): Int =
- line compare that.line match {
- case 0 => column compare that.column
- case i => i
- }
-
- private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position =
- {
- var l = line
- var c = column
- for (x <- iterator) {
- if (is_newline(x)) { l += 1; c = 0 } else c += 1
- }
- Position(l, c)
- }
-
- def advance(text: String): Position =
- if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
-
- def advance_symbols(text: String): Position =
- if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
-
- def advance_codepoints(text: String): Position =
- if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10)
- }
-
-
- /* range (right-open interval) */
-
- sealed case class Range(start: Position, stop: Position)
- {
- if (start.compare(stop) > 0)
- error("Bad line range: " + start.print + ".." + stop.print)
-
- def print: String = start.print + ".." + stop.print
- }
-
-
- /* document with newline as separator (not terminator) */
-
- object Document
- {
- val empty: Document = new Document("", Nil)
-
- def apply(lines: List[Line]): Document =
- if (lines.isEmpty) empty
- else new Document(lines.mkString("", "\n", ""), lines)
-
- def apply(text: String): Document =
- if (text.contains('\r'))
- apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
- else if (text == "") Document.empty
- else new Document(text, Library.split_lines(text).map(Line(_)))
- }
-
- final class Document private(val text: String, val lines: List[Line])
- {
- override def toString: String = text
-
- override def equals(that: Any): Boolean =
- that match {
- case other: Document => lines == other.lines
- case _ => false
- }
- override def hashCode(): Int = lines.hashCode
-
- private def position(advance: (Position, String) => Position, offset: Text.Offset): Position =
- {
- @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
- {
- lines_rest match {
- case Nil => require(i == 0); Position(lines_count, 0)
- case line :: ls =>
- val n = line.text.length
- if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i))
- else move(i - (n + 1), lines_count + 1, ls)
- }
- }
- move(offset, 0, lines)
- }
-
- def position(i: Text.Offset): Position = position(_.advance(_), i)
- def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
- def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
-
- // FIXME symbols, codepoints
- def offset(pos: Position): Option[Text.Offset] =
- {
- val l = pos.line
- val c = pos.column
- if (0 <= l && l < lines.length) {
- val line_offset =
- if (l == 0) 0
- else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 })
- if (c <= lines(l).text.length) Some(line_offset + c) else None
- }
- else None
- }
- }
-
-
- /* line text */
-
- val empty: Line = new Line("")
- def apply(text: String): Line = if (text == "") empty else new Line(text)
-}
-
-final class Line private(val text: String)
-{
- require(text.forall(c => c != '\r' && c != '\n'))
-
- lazy val length_symbols: Int = Symbol.iterator(text).length
- lazy val length_codepoints: Int = Word.codepoint_iterator(text).length
-
- override def equals(that: Any): Boolean =
- that match {
- case other: Line => text == other.text
- case _ => false
- }
- override def hashCode(): Int = text.hashCode
- override def toString: String = text
-}
--- a/src/Tools/VSCode/src/server.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala Tue Dec 20 18:11:42 2016 +0100
@@ -20,21 +20,28 @@
{
/* 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 =>
{
var log_file: Option[Path] = None
+ var text_length = 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(
+ { 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(logic) + """)
-m MODE add print mode for output
@@ -43,6 +50,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)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
@@ -56,7 +64,7 @@
error("Missing logic image " + quote(logic))
val channel = new Channel(System.in, System.out, log_file)
- val server = new Server(channel, options, logic, dirs, modes)
+ val server = new Server(channel, options, text_length, logic, dirs, modes)
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
@@ -78,6 +86,7 @@
class Server(
channel: Channel,
options: Options,
+ text_length: Length = Length.encoding(Server.default_text_length),
session_name: String = Server.default_logic,
session_dirs: List[Path] = Nil,
modes: List[String] = Nil)
@@ -185,12 +194,13 @@
for {
model <- state.value.models.get(uri)
snapshot = model.snapshot()
- offset <- model.doc.offset(pos)
+ offset <- model.doc.offset(pos, text_length)
info <- tooltip(snapshot, Text.Range(offset, offset + 1))
} yield {
- val r = Line.Range(model.doc.position(info.range.start), model.doc.position(info.range.stop))
+ val start = model.doc.position(info.range.start, text_length)
+ val stop = model.doc.position(info.range.stop, text_length)
val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
- (r, List("```\n" + s + "\n```"))
+ (Line.Range(start, stop), List("```\n" + s + "\n```"))
}
private val tooltip_descriptions =
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 20 16:18:56 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 20 18:11:42 2016 +0100
@@ -269,14 +269,13 @@
case Some(name) =>
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) if offset > 0 =>
- val (line, column) =
+ val pos =
JEdit_Lib.buffer_lock(buffer) {
- ((1, 1) /:
+ (Line.Position.zero /:
(Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
- zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
- Symbol.advance_line_column)
+ zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
}
- Some(hyperlink_file(focus, name, line, column))
+ Some(hyperlink_file(focus, name, pos.line1, pos.column1))
case _ => Some(hyperlink_file(focus, name, line))
}
case None => None
@@ -297,8 +296,8 @@
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 (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
- Some(hyperlink_file(focus, file_name, line, column))
+ val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+ Some(hyperlink_file(focus, file_name, pos.line1, pos.column1))
}
}
}