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)