src/Tools/VSCode/src/server.scala
changeset 64724 44dbf8cc2d7f
parent 64722 6df73de0d3c7
child 64725 38305f56c769
equal deleted inserted replaced
64723:65bcb1fbaa73 64724:44dbf8cc2d7f
   304             update_document(uri, text)
   304             update_document(uri, text)
   305           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
   305           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
   306             update_document(uri, text)
   306             update_document(uri, text)
   307           case Protocol.DidCloseTextDocument(uri) =>
   307           case Protocol.DidCloseTextDocument(uri) =>
   308             close_document(uri)
   308             close_document(uri)
   309           case Protocol.DidSaveTextDocument(uri) => log("SAVE " + uri)
       
   310           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
   309           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
   311           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   310           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   312           case _ => log("### IGNORED")
   311           case _ => log("### IGNORED")
   313         }
   312         }
   314       }
   313       }