src/Tools/VSCode/src/server.scala
changeset 64687 04806ad1e43a
parent 64684 fe2c9c215b36
child 64690 599873de8b01
equal deleted inserted replaced
64686:7888be4fa496 64687:04806ad1e43a
   306           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
   306           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
   307           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   307           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   308           case _ => channel.log("### IGNORED")
   308           case _ => channel.log("### IGNORED")
   309         }
   309         }
   310       }
   310       }
   311       catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
   311       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
   312     }
   312     }
   313 
   313 
   314     @tailrec def loop()
   314     @tailrec def loop()
   315     {
   315     {
   316       channel.read() match {
   316       channel.read() match {