# HG changeset patch # User wenzelm # Date 1483626752 -3600 # Node ID 5ecc426922b79abb755c7329272e1523e8032b6c # Parent 415dafeb966939fb1fefdb8d30612c2c6674d490 tuned; diff -r 415dafeb9669 -r 5ecc426922b7 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Thu Jan 05 15:15:51 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Thu Jan 05 15:32:32 2017 +0100 @@ -335,12 +335,12 @@ case Protocol.Initialize(id) => init(id) case Protocol.Shutdown(id) => shutdown(id) case Protocol.Exit(()) => exit() - case Protocol.DidOpenTextDocument(uri, lang, version, text) => - update_document(uri, text) - case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) => - update_document(uri, text) - case Protocol.DidCloseTextDocument(uri) => - close_document(uri) + case Protocol.DidOpenTextDocument(file, lang, version, text) => + update_document(file, text) + case Protocol.DidChangeTextDocument(file, version, List(Protocol.TextDocumentContent(text))) => + update_document(file, text) + case Protocol.DidCloseTextDocument(file) => + close_document(file) 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)