From 883c197830d2c8df4d5e8265f7b0ea368be2ad59 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Sun, 20 Dec 2020 18:05:11 +0100 Subject: [PATCH] chore: string formatting --- src/Lean/Data/Json/Parser.lean | 4 ++-- src/Lean/Data/Json/Printer.lean | 9 ++++++--- src/Lean/Data/JsonRpc.lean | 24 ++++++++++++------------ src/Lean/Data/Lsp/Communication.lean | 8 ++++---- src/Lean/Server/FileWorker.lean | 7 +++---- src/Lean/Server/Watchdog.lean | 8 ++++---- 6 files changed, 31 insertions(+), 29 deletions(-) diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean index 042c9860c4..904e81a90c 100644 --- a/src/Lean/Data/Json/Parser.lean +++ b/src/Lean/Data/Json/Parser.lean @@ -79,7 +79,7 @@ def expect (s : String) : Quickparse Unit := fun it => if it.extract (it.forward s.length) = s then success (it.forward s.length) () else - error it ("expected: " ++ s) + error it s!"expected: {s}" @[inline] def ws : Quickparse Unit := fun it => @@ -311,7 +311,7 @@ namespace Json def parse (s : String) : Except String Lean.Json := match Json.Parser.any s.mkIterator with | Quickparse.Result.success _ res => Except.ok res - | Quickparse.Result.error it err => Except.error ("offset " ++ it.i.repr ++ ": " ++ err) + | Quickparse.Result.error it err => Except.error s!"offset {it.i.repr}: {err}" end Json diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean index 3cf90b3d5a..0f8ff62fe0 100644 --- a/src/Lean/Data/Json/Printer.lean +++ b/src/Lean/Data/Json/Printer.lean @@ -71,10 +71,13 @@ partial def compress : Json → String | bool false => "false" | num s => s.toString | str s => renderString s - | arr elems => "[" ++ ",".intercalate (elems.map compress).toList ++ "]" + | arr elems => + let f := ",".intercalate (elems.map compress).toList + s!"[{f}]" | obj kvs => - let ckvs := kvs.fold (fun acc k j => (renderString k ++ ":" ++ compress j) :: acc) []; - "{" ++ ",".intercalate ckvs ++ "}" + let ckvs := kvs.fold (fun acc k j => s!"{renderString k}:{compress j}" :: acc) [] + let ckvs := ",".intercalate ckvs + s!"{ckvs}" instance : ToFormat Json := ⟨render⟩ instance : ToString Json := ⟨pretty⟩ diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index 88536cdbc7..448897ae6a 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -197,7 +197,7 @@ section let j ← h.readJson nBytes match fromJson? j with | some m => pure m - | none => throw $ userError ("JSON '" ++ j.compress ++ "' did not have the format of a JSON-RPC message") + | none => throw $ userError s!"JSON '{j.compress}' did not have the format of a JSON-RPC message" def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α) [FromJson α] : IO (Request α) := do let m ← h.readMessage nBytes @@ -209,11 +209,11 @@ section let j := toJson params match fromJson? j with | some v => pure ⟨id, expectedMethod, v⟩ - | none => throw $ userError ("unexpected param '" ++ j.compress ++ "' for method '" ++ expectedMethod ++ "'") - | none => throw $ userError ("unexpected lack of param for method '" ++ expectedMethod ++ "'") + | none => throw $ userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'" + | none => throw $ userError s!"Unexpected lack of param for method '{expectedMethod}'" else - throw $ userError ("expected method '" ++ expectedMethod ++ "', got method '" ++ method ++ "'") - | _ => throw $ userError "expected request, got other type of message" + throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'" + | _ => throw $ userError "Expected request, got other type of message" def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α) [FromJson α] : IO (Notification α) := do let m ← h.readMessage nBytes @@ -225,11 +225,11 @@ section let j := toJson params match fromJson? j with | some v => pure ⟨expectedMethod, v⟩ - | none => throw $ userError ("unexpected param '" ++ j.compress ++ "' for method '" ++ expectedMethod ++ "'") - | none => throw $ userError ("unexpected lack of param for method '" ++ expectedMethod ++ "'") + | none => throw $ userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'" + | none => throw $ userError s!"Unexpected lack of param for method '{expectedMethod}'" else - throw $ userError ("expected method '" ++ expectedMethod ++ "', got method '" ++ method ++ "'") - | _ => throw $ userError "expected notification, got other type of message" + throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'" + | _ => throw $ userError "Expected notification, got other type of message" def readResponseAs (h : FS.Stream) (nBytes : Nat) (expectedID : RequestID) (α) [FromJson α] : IO (Response α) := do let m ← h.readMessage nBytes @@ -238,10 +238,10 @@ section if id = expectedID then match fromJson? result with | some v => pure ⟨expectedID, v⟩ - | none => throw $ userError s!"unexpected result '{result.compress}'" + | none => throw $ userError s!"Unexpected result '{result.compress}'" else - throw $ userError s!"expected id {expectedID}, got id {id}" - | _ => throw $ userError "expected response, got other type of message" + throw $ userError s!"Expected id {expectedID}, got id {id}" + | _ => throw $ userError "Expected response, got other type of message" end section diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean index 791d0238b0..13fc52fdd2 100644 --- a/src/Lean/Data/Lsp/Communication.lean +++ b/src/Lean/Data/Lsp/Communication.lean @@ -34,7 +34,7 @@ section | some hf => let tail ← readHeaderFields h pure (hf :: tail) - | none => throw $ userError ("Invalid header field: " ++ l) + | none => throw $ userError s!"Invalid header field: {l}" /-- Returns the Content-Length. -/ private def readLspHeader (h : FS.Stream) : IO Nat := do @@ -42,8 +42,8 @@ section match fields.lookup "Content-Length" with | some length => match length.toNat? with | some n => pure n - | none => throw $ userError ("Content-Length header value '" ++ length ++ "' is not a Nat") - | none => throw $ userError ("No Content-Length header in header fields: " ++ toString fields) + | none => throw $ userError s!"Content-Length header value '{length}' is not a Nat" + | none => throw $ userError s!"No Content-Length header in header fields: {toString fields}" def readLspMessage (h : FS.Stream) : IO Message := do let nBytes ← readLspHeader h @@ -69,7 +69,7 @@ section -- inlined implementation instead of using jsonrpc's writeMessage -- to maintain the atomicity of putStr let j := (toJson msg).compress - let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n" + let header := s!"Content-Length: {toString j.utf8ByteSize}\r\n\r\n" h.putStr (header ++ j) h.flush diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 4e7fd583f6..2fbca1d4f9 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -226,7 +226,7 @@ section MessageHandling def parseParams (paramType : Type) [FromJson paramType] (params : Json) : ServerM paramType := match fromJson? params with | some parsed => pure parsed - | none => throwServerError $ "Got param with wrong structure: " ++ params.compress + | none => throwServerError s!"Got param with wrong structure: {params.compress}" def handleNotification (method : String) (params : Json) : ServerM Unit := do let handle := fun paramType [FromJson paramType] (handler : paramType → ServerM Unit) => @@ -234,7 +234,7 @@ section MessageHandling match method with | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange | "$/cancelRequest" => handle CancelParams handleCancelRequest - | _ => throwServerError $ "Got unsupported notification method: " ++ method + | _ => throwServerError s!"Got unsupported notification method: {method}" def queueRequest (id : RequestID) (handler : RequestID → α → ServerM Unit) (params : α) : ServerM Unit := do @@ -249,8 +249,7 @@ section MessageHandling match method with | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam handleWaitForDiagnostics | "textDocument/hover" => handle HoverParams handleHover - | _ => throwServerError $ "Got unsupported request: " ++ method ++ - " params: " ++ toString params + | _ => throwServerError s!"Got unsupported request: {method}" end MessageHandling section MainLoop diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 28fbea2b89..1ad7d89267 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -164,7 +164,7 @@ section ServerM def findFileWorker (uri : DocumentUri) : ServerM FileWorker := do match (←(←read).fileWorkersRef.get).find? uri with | some fw => fw - | none => throwServerError $ "Got unknown document URI (" ++ uri ++ ")" + | none => throwServerError s!"Got unknown document URI ({uri})" def eraseFileWorker (uri : DocumentUri) : ServerM Unit := do (←read).fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase uri) @@ -334,7 +334,7 @@ section MessageHandling def parseParams (paramType : Type) [FromJson paramType] (params : Json) : ServerM paramType := match fromJson? params with | some parsed => pure parsed - | none => throwServerError $ "Got param with wrong structure: " ++ params.compress + | none => throwServerError s!"Got param with wrong structure: {params.compress}" def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do let handle := fun α [FromJson α] [ToJson α] [FileSource α] => do @@ -344,7 +344,7 @@ section MessageHandling match method with | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam | "textDocument/hover" => handle HoverParams - | _ => throwServerError $ "Got unsupported request: " ++ method ++ " params: " ++ toString params + | _ => throwServerError s!"Got unsupported request: {method}" def handleNotification (method : String) (params : Json) : ServerM Unit := let handle := (fun α [FromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler) @@ -491,7 +491,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : : WatchdogM (List (Notification PublishDiagnosticsParams)) := do writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParam.mk target⟩ let rec loop : WatchdogM (List (Notification PublishDiagnosticsParams)) := do - let error : IO (List (Notification PublishDiagnosticsParams)) := throw $ userError "got unexpected packet while collecting diagnostics" + let error : IO (List (Notification PublishDiagnosticsParams)) := throw $ userError "Got unexpected packet while collecting diagnostics" match ←(←stdout).readLspMessage with | Message.response id _ => if id = waitForDiagnosticsId then