diff -r 50cfc6775361 -r 41d2452845fc src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sat Mar 11 20:18:06 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sat Mar 11 20:22:43 2017 +0100 @@ -152,6 +152,18 @@ } + /* caret handling */ + + private val delay_caret_update: Standard_Thread.Delay = + Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger) + { session.caret_focus.post(Session.Caret_Focus) } + + private def update_caret(caret: Option[(JFile, Line.Position)]) + { + resources.update_caret(caret) + delay_caret_update.invoke() + } + /* output to client */ @@ -362,6 +374,7 @@ case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) + case Protocol.Caret_Update(caret) => update_caret(caret) case _ => log("### IGNORED") } }