From e6b281816910e400bc7bcf03c4ccfaebc7f7fcf0 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Tue, 15 Jun 2021 12:20:18 -0700
Subject: [PATCH] chore: fixes

---
 src/Lean/Server/Requests.lean | 4 ++--
 src/shell/lean.cpp            | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

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";