src/Tools/VSCode/src/language_server.scala
changeset 83414 f61236e8c7b0
parent 83410 166196bdda3c
child 83415 e78d50e3e1eb
equal deleted inserted replaced
83413:068cfdd057d0 83414:f61236e8c7b0
   549           case LSP.Preview_Request(file, column) => preview_request(file, column)
   549           case LSP.Preview_Request(file, column) => preview_request(file, column)
   550           case LSP.Symbols_Panel_Request => symbols_panel_request()
   550           case LSP.Symbols_Panel_Request => symbols_panel_request()
   551           case LSP.Documentation_Request => documentation_request()
   551           case LSP.Documentation_Request => documentation_request()
   552           case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
   552           case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
   553             sledgehammer.handle_request(provers, isar, try0, purpose)
   553             sledgehammer.handle_request(provers, isar, try0, purpose)
   554           case LSP.Sledgehammer_Cancel_Request => sledgehammer.cancel_query()
   554           case LSP.Sledgehammer_Cancel => sledgehammer.cancel()
   555           case LSP.Sledgehammer_Provers_Request => sledgehammer.send_provers()
   555           case LSP.Sledgehammer_Provers_Request => sledgehammer.send_provers()
   556           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
   556           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
   557         }
   557         }
   558       }
   558       }
   559       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
   559       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }