diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index df669839f1..889fc62f28 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -33,7 +33,7 @@ def fileChanged : RequestError := def methodNotFound (method : String) : RequestError := { code := ErrorCode.methodNotFound - message := s!"No request handler found for '${method}'" } + message := s!"No request handler found for '{method}'" } instance : Coe IO.Error RequestError where coe e := { code := ErrorCode.internalError @@ -160,7 +160,7 @@ def routeLspRequest (method : String) (params : Json) : IO (Except RequestError def handleLspRequest (method : String) (params : Json) : RequestM (RequestTask Json) := do match (← lookupLspRequestHandler method) with - | none => throw <| RequestError.methodNotFound method + | none => throwThe IO.Error <| IO.userError s!"internal server error: request '{method}' routed through watchdog but unknown in worker; are both using the same plugins?" | some rh => rh.handle params end HandlerTable diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 6bd0848091..0dbe2588f7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -529,6 +529,7 @@ int main(int argc, char ** argv) { case 'p': check_optarg("p"); load_plugin(optarg); + forwarded_args.push_back(string_ref("--plugin=" + std::string(optarg))); break; default: std::cerr << "Unknown command line option\n";