src/Tools/VSCode/src/server.scala
changeset 64655 ea34f36ff6a5
parent 64651 ea5620f7b0d8
child 64667 cdb0d559a24b
equal deleted inserted replaced
64654:31b681e38c70 64655:ea34f36ff6a5
   273           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
   273           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
   274           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   274           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   275           case _ => channel.log("### IGNORED")
   275           case _ => channel.log("### IGNORED")
   276         }
   276         }
   277       }
   277       }
   278       catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) }
   278       catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
   279     }
   279     }
   280 
   280 
   281     @tailrec def loop()
   281     @tailrec def loop()
   282     {
   282     {
   283       channel.read() match {
   283       channel.read() match {