# HG changeset patch # User wenzelm # Date 1489325018 -3600 # Node ID e8760a98db7838cd00f55644528278c799bf5ea8 # Parent ffab6f460a82c945268eda827dc939a99b8d4e43 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16; diff -r ffab6f460a82 -r e8760a98db78 src/Pure/General/codepoint.scala --- a/src/Pure/General/codepoint.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Pure/General/codepoint.scala Sun Mar 12 14:23:38 2017 +0100 @@ -24,30 +24,4 @@ } def length(s: String): Int = iterator(s).length - - trait Length extends Text.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)) Text.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 ffab6f460a82 -r e8760a98db78 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Pure/General/symbol.scala Sun Mar 12 14:23:38 2017 +0100 @@ -130,15 +130,6 @@ def length(text: CharSequence): Int = iterator(text).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)) Text.Length.offset(text, i) - else if (i <= length(text)) Some(iterator(text).take(i).mkString.length) - else None - } - /* decoding offsets */ diff -r ffab6f460a82 -r e8760a98db78 src/Pure/General/utf8.scala --- a/src/Pure/General/utf8.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Pure/General/utf8.scala Sun Mar 12 14:23:38 2017 +0100 @@ -21,15 +21,6 @@ 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 */ diff -r ffab6f460a82 -r e8760a98db78 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Pure/PIDE/document.scala Sun Mar 12 14:23:38 2017 +0100 @@ -845,7 +845,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(_, Text.Length)) + val pos = (Line.Position.zero /: sources_iterator)(_.advance(_)) Line.Node_Position(name, pos) } diff -r ffab6f460a82 -r e8760a98db78 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Pure/PIDE/line.scala Sun Mar 12 14:23:38 2017 +0100 @@ -40,12 +40,12 @@ case i => i } - def advance(text: String, text_length: Text.Length): Position = + def advance(text: String): Position = if (text.isEmpty) this else { val lines = logical_lines(text) val l = line + lines.length - 1 - val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last)) + val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length Position(l, c) } } @@ -89,12 +89,13 @@ object Document { - def apply(text: String, text_length: Text.Length): Document = - Document(logical_lines(text).map(s => Line(Library.trim_substring(s))), text_length) + def apply(text: String): Document = + Document(logical_lines(text).map(s => Line(Library.trim_substring(s)))) + + val empty: Document = apply("") private def split(line_text: String): List[Line] = - if (line_text == "") List(Line.empty) - else apply(line_text, Text.Length).lines + if (line_text == "") List(Line.empty) else apply(line_text).lines private def chop(lines: List[Line]): (String, List[Line]) = lines match { @@ -109,7 +110,7 @@ def text(lines: List[Line]): String = lines.mkString("", "\n", "") } - sealed case class Document(lines: List[Line], text_length: Text.Length) + sealed case class Document(lines: List[Line]) { lazy val text_range: Text.Range = Text.Range(0, Document.length(lines)) lazy val text: String = Document.text(lines) @@ -136,7 +137,7 @@ case line :: ls => val n = line.text.length if (ls.isEmpty || i <= n) - Position(lines_count).advance(line.text.substring(n - i), text_length) + Position(lines_count).advance(line.text.substring(n - i)) else move(i - (n + 1), lines_count + 1, ls) } } @@ -152,9 +153,12 @@ val c = pos.column val n = lines.length if (0 <= l && l < n) { - val line_offset = - (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 } - text_length.offset(lines(l).text, c).map(line_offset + _) + if (0 <= c && c <= lines(l).text.length) { + val line_offset = + (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 } + Some(line_offset + c) + } + else None } else if (l == n && c == 0) Some(text_range.length) else None @@ -170,49 +174,47 @@ if l1 <= l2 (removed_text, new_lines) <- { + val c1 = remove.start.column + val c2 = remove.stop.column + val (prefix, lines1) = lines.splitAt(l1) val (s1, rest1) = Document.chop(lines1) if (l1 == l2) { - for { - c1 <- text_length.offset(s1, remove.start.column) - c2 <- text_length.offset(s1, remove.stop.column) - if c1 <= c2 + if (0 <= c1 && c1 <= c2 && c2 <= s1.length) { + Some( + if (lines1.isEmpty) ("", prefix) + else { + val removed_text = s1.substring(c1, c2) + val changed_text = s1.substring(0, c1) + insert + s1.substring(c2) + (removed_text, prefix ::: Document.split(changed_text) ::: rest1) + }) } - yield { - if (lines1.isEmpty) ("", prefix) - else { - val removed_text = s1.substring(c1, c2) - val changed_text = s1.substring(0, c1) + insert + s1.substring(c2) - (removed_text, prefix ::: Document.split(changed_text) ::: rest1) - } - } + else None } else { val (middle, lines2) = rest1.splitAt(l2 - l1 - 1) val (s2, rest2) = Document.chop(lines2) - for { - c1 <- text_length.offset(s1, remove.start.column) - c2 <- text_length.offset(s2, remove.stop.column) + if (0 <= c1 && c1 <= s1.length && 0 <= c2 && c2 <= s2.length) { + Some( + if (lines1.isEmpty) ("", prefix) + else { + val r1 = s1.substring(c1) + val r2 = s2.substring(0, c2) + val removed_text = + if (lines2.isEmpty) Document.text(Line(r1) :: middle) + else Document.text(Line(r1) :: middle ::: List(Line(r2))) + val changed_text = s1.substring(0, c1) + insert + s2.substring(c2) + (removed_text, prefix ::: Document.split(changed_text) ::: rest2) + }) } - yield { - if (lines1.isEmpty) ("", prefix) - else { - val r1 = s1.substring(c1) - val r2 = s2.substring(0, c2) - val removed_text = - if (lines2.isEmpty) Document.text(Line(r1) :: middle) - else Document.text(Line(r1) :: middle ::: List(Line(r2))) - val changed_text = s1.substring(0, c1) + insert + s2.substring(c2) - (removed_text, prefix ::: Document.split(changed_text) ::: rest2) - } - } + else None } } } yield (Text.Edit.removes(edit_start, removed_text) ::: Text.Edit.inserts(edit_start, insert), - Document(new_lines, text_length)) + Document(new_lines)) } } diff -r ffab6f460a82 -r e8760a98db78 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Pure/PIDE/text.scala Sun Mar 12 14:23:38 2017 +0100 @@ -190,32 +190,4 @@ (rest, remove(i, count, string)) } } - - - /* text length wrt. encoding */ - - trait Length - { - def apply(text: String): Int - def offset(text: String, i: Int): Option[Offset] - } - - object Length extends Length - { - def apply(text: String): Int = text.length - def offset(text: String, i: Int): Option[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 ffab6f460a82 -r e8760a98db78 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sun Mar 12 14:23:38 2017 +0100 @@ -45,7 +45,7 @@ def init(session: Session, node_name: Document.Node.Name): Document_Model = { val resources = session.resources.asInstanceOf[VSCode_Resources] - val content = Content(Line.Document("", resources.text_length)) + val content = Content(Line.Document.empty) Document_Model(session, node_name, content) } } @@ -111,7 +111,7 @@ Text.Edit.replace(0, content.text, insert) match { case Nil => None case edits => - val content1 = Document_Model.Content(Line.Document(insert, content.doc.text_length)) + val content1 = Document_Model.Content(Line.Document(insert)) Some(copy(content = content1, pending_edits = pending_edits ::: edits)) } case Some(remove) => diff -r ffab6f460a82 -r e8760a98db78 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sun Mar 12 14:23:38 2017 +0100 @@ -22,30 +22,23 @@ { /* 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 => { try { var log_file: Option[Path] = None - 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() var system_mode = false - def text_length_choice: String = - commas(Text.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(default_logic) + """) -m MODE add print mode for output @@ -55,7 +48,6 @@ Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. """, "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), - "T:" -> (arg => Text.Length.encoding(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), @@ -67,7 +59,7 @@ val log = Logger.make(log_file) val channel = new Channel(System.in, System.out, log) - val server = new Server(channel, options, text_length, logic, dirs, modes, system_mode, log) + val server = new Server(channel, options, logic, dirs, modes, system_mode, log) // prevent spurious garbage on the main protocol channel val orig_out = System.out @@ -89,7 +81,6 @@ class Server( val channel: Channel, options: Options, - 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, @@ -222,8 +213,7 @@ } val base = Build.session_base(options, false, session_dirs, session_name) - val resources = - new VSCode_Resources(options, text_length, base, log) + val resources = new VSCode_Resources(options, base, log) { override def commit(change: Session.Change): Unit = if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) diff -r ffab6f460a82 -r e8760a98db78 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Mar 12 14:23:38 2017 +0100 @@ -200,7 +200,7 @@ resources.get_file_content(file) match { case Some(text) => val chunk = Symbol.Text_Chunk(text) - val doc = Line.Document(text, resources.text_length) + val doc = Line.Document(text) doc.range(chunk.decode(range)) case _ => Line.Range(Line.Position((line1 - 1) max 0)) diff -r ffab6f460a82 -r e8760a98db78 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 12 14:23:38 2017 +0100 @@ -41,7 +41,6 @@ class VSCode_Resources( val options: Options, - val text_length: Text.Length, base: Sessions.Base, log: Logger = No_Logger) extends Resources(base, log) { diff -r ffab6f460a82 -r e8760a98db78 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Sun Mar 12 14:23:38 2017 +0100 @@ -338,7 +338,7 @@ def node_position(offset: Text.Offset): Line.Node_Position = Line.Node_Position(node_name.node, - Line.Position.zero.advance(content.text.substring(0, offset), Text.Length)) + Line.Position.zero.advance(content.text.substring(0, offset))) def get_blob: Option[Document.Blob] = if (is_theory) None diff -r ffab6f460a82 -r e8760a98db78 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sun Mar 12 13:48:10 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Mar 12 14:23:38 2017 +0100 @@ -258,8 +258,7 @@ hyperlink( (Line.Position.zero /: (Symbol.iterator(text). - zipWithIndex.takeWhile(p => p._2 < offset - 1). - map(_._1)))(_.advance(_, Text.Length))) + zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))) case None => hyperlink(Line.Position((line1 - 1) max 0)) }