# HG changeset patch
# User wenzelm
# Date 1482250180 -3600
# Node ID c81bd30839a6415eea376fc37ea2ecf3faca9177
# Parent  01e50039edc94fbffe919463e04bdd1da56e1971
added option -T: text length encoding;

diff -r 01e50039edc9 -r c81bd30839a6 src/Pure/General/length.scala
--- a/src/Pure/General/length.scala	Tue Dec 20 16:08:02 2016 +0100
+++ b/src/Pure/General/length.scala	Tue Dec 20 17:09:40 2016 +0100
@@ -19,13 +19,15 @@
   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 =
-    name match {
-      case "UTF-8" => UTF8.Length
-      case "UTF-16" => Length
-      case "codepoints" => Codepoint.Length
-      case "symbols" => Symbol.Length
-      case _ =>
-        error("Bad text encoding: " + name + " (expected UTF-8, UTF-16, codepoints, symbols)")
-    }
+    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 01e50039edc9 -r c81bd30839a6 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Dec 20 16:08:02 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Dec 20 17:09:40 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 =