equal
deleted
inserted
replaced
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 { |