# HG changeset patch # User wenzelm # Date 1482253902 -3600 # Node ID 14f938969779e535cfd1b038d6cffa37a4c642e3 # Parent 20ccca53dd736a2aa17b672d19b75cbaa7f404e2# Parent e3d9a31281f31b9484eb91052f7f70cba930f8e1 merged diff -r 20ccca53dd73 -r 14f938969779 src/Pure/Admin/check_sources.scala --- 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))) } } diff -r 20ccca53dd73 -r 14f938969779 src/Pure/General/codepoint.scala --- /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 +} diff -r 20ccca53dd73 -r 14f938969779 src/Pure/General/length.scala --- /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)) + ")") +} diff -r 20ccca53dd73 -r 14f938969779 src/Pure/General/symbol.scala --- 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 } diff -r 20ccca53dd73 -r 14f938969779 src/Pure/General/word.scala --- 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 diff -r 20ccca53dd73 -r 14f938969779 src/Pure/Isar/document_structure.scala --- 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) diff -r 20ccca53dd73 -r 14f938969779 src/Pure/Isar/outer_syntax.scala --- 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) } diff -r 20ccca53dd73 -r 14f938969779 src/Pure/PIDE/line.scala --- /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 +} diff -r 20ccca53dd73 -r 14f938969779 src/Pure/PIDE/protocol.scala --- 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)) } diff -r 20ccca53dd73 -r 14f938969779 src/Pure/System/utf8.scala --- 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) } } - diff -r 20ccca53dd73 -r 14f938969779 src/Pure/build-jars --- 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 ) diff -r 20ccca53dd73 -r 14f938969779 src/Tools/VSCode/src/line.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 -} diff -r 20ccca53dd73 -r 14f938969779 src/Tools/VSCode/src/server.scala --- 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 = diff -r 20ccca53dd73 -r 14f938969779 src/Tools/jEdit/src/jedit_editor.scala --- 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)) } } }