src/Tools/VSCode/src/server.scala
changeset 64682 7e119f32276a
parent 64679 b2bf280b7e13
child 64683 c0c09b6dfbe0
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:02:38 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:10:09 2016 +0100
     1.3 @@ -27,14 +27,14 @@
     1.4    {
     1.5      try {
     1.6        var log_file: Option[Path] = None
     1.7 -      var text_length = Length.encoding(default_text_length)
     1.8 +      var text_length = Text.Length.encoding(default_text_length)
     1.9        var dirs: List[Path] = Nil
    1.10        var logic = default_logic
    1.11        var modes: List[String] = Nil
    1.12        var options = Options.init()
    1.13  
    1.14        def text_length_choice: String =
    1.15 -        commas(Length.encodings.map(
    1.16 +        commas(Text.Length.encodings.map(
    1.17            { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
    1.18  
    1.19        val getopts = Getopts("""
    1.20 @@ -51,7 +51,7 @@
    1.21    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    1.22  """,
    1.23          "L:" -> (arg => log_file = Some(Path.explode(arg))),
    1.24 -        "T:" -> (arg => Length.encoding(arg)),
    1.25 +        "T:" -> (arg => Text.Length.encoding(arg)),
    1.26          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.27          "l:" -> (arg => logic = arg),
    1.28          "m:" -> (arg => modes = arg :: modes),
    1.29 @@ -95,7 +95,7 @@
    1.30  class Server(
    1.31    channel: Channel,
    1.32    options: Options,
    1.33 -  text_length: Length = Length.encoding(Server.default_text_length),
    1.34 +  text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
    1.35    session_name: String = Server.default_logic,
    1.36    session_dirs: List[Path] = Nil,
    1.37    modes: List[String] = Nil)