added option -T: text length encoding;
authorwenzelm
Tue Dec 20 17:09:40 2016 +0100 (2016-12-20)
changeset 64618c81bd30839a6
parent 64617 01e50039edc9
child 64619 e3d9a31281f3
added option -T: text length encoding;
src/Pure/General/length.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Pure/General/length.scala	Tue Dec 20 16:08:02 2016 +0100
     1.2 +++ b/src/Pure/General/length.scala	Tue Dec 20 17:09:40 2016 +0100
     1.3 @@ -19,13 +19,15 @@
     1.4    def offset(text: String, i: Int): Option[Text.Offset] =
     1.5      if (0 <= i && i <= text.length) Some(i) else None
     1.6  
     1.7 +  val encodings: List[(String, Length)] =
     1.8 +    List(
     1.9 +      "UTF-16" -> Length,
    1.10 +      "UTF-8" -> UTF8.Length,
    1.11 +      "codepoints" -> Codepoint.Length,
    1.12 +      "symbols" -> Symbol.Length)
    1.13 +
    1.14    def encoding(name: String): Length =
    1.15 -    name match {
    1.16 -      case "UTF-8" => UTF8.Length
    1.17 -      case "UTF-16" => Length
    1.18 -      case "codepoints" => Codepoint.Length
    1.19 -      case "symbols" => Symbol.Length
    1.20 -      case _ =>
    1.21 -        error("Bad text encoding: " + name + " (expected UTF-8, UTF-16, codepoints, symbols)")
    1.22 -    }
    1.23 +    encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
    1.24 +      error("Bad text length encoding: " + quote(name) +
    1.25 +        " (expected " + commas_quote(encodings.map(_._1)) + ")")
    1.26  }
     2.1 --- a/src/Tools/VSCode/src/server.scala	Tue Dec 20 16:08:02 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Dec 20 17:09:40 2016 +0100
     2.3 @@ -20,21 +20,28 @@
     2.4  {
     2.5    /* Isabelle tool wrapper */
     2.6  
     2.7 +  private val default_text_length = "UTF-16"
     2.8    private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
     2.9  
    2.10    val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
    2.11    {
    2.12      var log_file: Option[Path] = None
    2.13 +    var text_length = Length.encoding(default_text_length)
    2.14      var dirs: List[Path] = Nil
    2.15      var logic = default_logic
    2.16      var modes: List[String] = Nil
    2.17      var options = Options.init()
    2.18  
    2.19 +    def text_length_choice: String =
    2.20 +      commas(Length.encodings.map(
    2.21 +        { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
    2.22 +
    2.23      val getopts = Getopts("""
    2.24  Usage: isabelle vscode_server [OPTIONS]
    2.25  
    2.26    Options are:
    2.27      -L FILE      enable logging on FILE
    2.28 +    -T LENGTH    text length encoding: """ + text_length_choice + """
    2.29      -d DIR       include session directory
    2.30      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    2.31      -m MODE      add print mode for output
    2.32 @@ -43,6 +50,7 @@
    2.33    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    2.34  """,
    2.35        "L:" -> (arg => log_file = Some(Path.explode(arg))),
    2.36 +      "T:" -> (arg => Length.encoding(arg)),
    2.37        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    2.38        "l:" -> (arg => logic = arg),
    2.39        "m:" -> (arg => modes = arg :: modes),
    2.40 @@ -56,7 +64,7 @@
    2.41        error("Missing logic image " + quote(logic))
    2.42  
    2.43      val channel = new Channel(System.in, System.out, log_file)
    2.44 -    val server = new Server(channel, options, logic, dirs, modes)
    2.45 +    val server = new Server(channel, options, text_length, logic, dirs, modes)
    2.46  
    2.47      // prevent spurious garbage on the main protocol channel
    2.48      val orig_out = System.out
    2.49 @@ -78,6 +86,7 @@
    2.50  class Server(
    2.51    channel: Channel,
    2.52    options: Options,
    2.53 +  text_length: Length = Length.encoding(Server.default_text_length),
    2.54    session_name: String = Server.default_logic,
    2.55    session_dirs: List[Path] = Nil,
    2.56    modes: List[String] = Nil)
    2.57 @@ -185,12 +194,13 @@
    2.58      for {
    2.59        model <- state.value.models.get(uri)
    2.60        snapshot = model.snapshot()
    2.61 -      offset <- model.doc.offset(pos)
    2.62 +      offset <- model.doc.offset(pos, text_length)
    2.63        info <- tooltip(snapshot, Text.Range(offset, offset + 1))
    2.64      } yield {
    2.65 -      val r = Line.Range(model.doc.position(info.range.start), model.doc.position(info.range.stop))
    2.66 +      val start = model.doc.position(info.range.start, text_length)
    2.67 +      val stop = model.doc.position(info.range.stop, text_length)
    2.68        val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
    2.69 -      (r, List("```\n" + s + "\n```"))
    2.70 +      (Line.Range(start, stop), List("```\n" + s + "\n```"))
    2.71      }
    2.72  
    2.73    private val tooltip_descriptions =