more explicit error;
authorwenzelm
Wed Dec 21 16:22:23 2016 +0100 (2016-12-21)
changeset 646447dbc9485ed70
parent 64643 b755f6069ba2
child 64645 0b513620d949
more explicit error;
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:14:47 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:22:23 2016 +0100
     1.3 @@ -25,18 +25,19 @@
     1.4  
     1.5    val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
     1.6    {
     1.7 -    var log_file: Option[Path] = None
     1.8 -    var text_length = 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 +    try {
    1.14 +      var log_file: Option[Path] = None
    1.15 +      var text_length = Length.encoding(default_text_length)
    1.16 +      var dirs: List[Path] = Nil
    1.17 +      var logic = default_logic
    1.18 +      var modes: List[String] = Nil
    1.19 +      var options = Options.init()
    1.20  
    1.21 -    def text_length_choice: String =
    1.22 -      commas(Length.encodings.map(
    1.23 -        { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
    1.24 +      def text_length_choice: String =
    1.25 +        commas(Length.encodings.map(
    1.26 +          { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
    1.27  
    1.28 -    val getopts = Getopts("""
    1.29 +      val getopts = Getopts("""
    1.30  Usage: isabelle vscode_server [OPTIONS]
    1.31  
    1.32    Options are:
    1.33 @@ -49,30 +50,37 @@
    1.34  
    1.35    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
    1.36  """,
    1.37 -      "L:" -> (arg => log_file = Some(Path.explode(arg))),
    1.38 -      "T:" -> (arg => Length.encoding(arg)),
    1.39 -      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.40 -      "l:" -> (arg => logic = arg),
    1.41 -      "m:" -> (arg => modes = arg :: modes),
    1.42 -      "o:" -> (arg => options = options + arg))
    1.43 +        "L:" -> (arg => log_file = Some(Path.explode(arg))),
    1.44 +        "T:" -> (arg => Length.encoding(arg)),
    1.45 +        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.46 +        "l:" -> (arg => logic = arg),
    1.47 +        "m:" -> (arg => modes = arg :: modes),
    1.48 +        "o:" -> (arg => options = options + arg))
    1.49  
    1.50 -    val more_args = getopts(args)
    1.51 -    if (more_args.nonEmpty) getopts.usage()
    1.52 +      val more_args = getopts(args)
    1.53 +      if (more_args.nonEmpty) getopts.usage()
    1.54 +
    1.55 +      if (!Build.build(options = options, build_heap = true, no_build = true,
    1.56 +            dirs = dirs, sessions = List(logic)).ok)
    1.57 +        error("Missing logic image " + quote(logic))
    1.58  
    1.59 -    if (!Build.build(options = options, build_heap = true, no_build = true,
    1.60 -          dirs = dirs, sessions = List(logic)).ok)
    1.61 -      error("Missing logic image " + quote(logic))
    1.62 -
    1.63 -    val channel = new Channel(System.in, System.out, log_file)
    1.64 -    val server = new Server(channel, options, text_length, logic, dirs, modes)
    1.65 +      val channel = new Channel(System.in, System.out, log_file)
    1.66 +      val server = new Server(channel, options, text_length, logic, dirs, modes)
    1.67  
    1.68 -    // prevent spurious garbage on the main protocol channel
    1.69 -    val orig_out = System.out
    1.70 -    try {
    1.71 -      System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
    1.72 -      server.start()
    1.73 +      // prevent spurious garbage on the main protocol channel
    1.74 +      val orig_out = System.out
    1.75 +      try {
    1.76 +        System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
    1.77 +        server.start()
    1.78 +      }
    1.79 +      finally { System.setOut(orig_out) }
    1.80      }
    1.81 -    finally { System.setOut(orig_out) }
    1.82 +    catch {
    1.83 +      case exn: Throwable =>
    1.84 +        val channel = new Channel(System.in, System.out, None)
    1.85 +        channel.error_message(Exn.message(exn))
    1.86 +        throw(exn)
    1.87 +    }
    1.88    })
    1.89  
    1.90