From 429079c889b7b612e8466ff7ca26fdb9d8dae4ff Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 17 Apr 2024 15:44:09 -0400 Subject: [PATCH 1/6] feat: lean CLI option to print messages as JSON --- src/Lean/Data/Position.lean | 3 ++- src/Lean/Elab/Frontend.lean | 6 +++--- src/Lean/Language/Basic.lean | 12 +++++++++--- src/Lean/Message.lean | 12 +++++++++++- src/util/shell.cpp | 10 ++++++++-- 5 files changed, 33 insertions(+), 10 deletions(-) diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index bb3047b06f3d..2af14fc623f4 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude import Lean.Data.Format +import Lean.Data.Json import Lean.ToExpr namespace Lean @@ -12,7 +13,7 @@ namespace Lean structure Position where line : Nat column : Nat - deriving Inhabited, DecidableEq, Repr + deriving Inhabited, DecidableEq, Repr, ToJson, FromJson namespace Position protected def lt : Position → Position → Bool diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 1e5992ae4572..8d7d15f9754d 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -107,6 +107,7 @@ def runFrontend (mainModuleName : Name) (trustLevel : UInt32 := 0) (ileanFileName? : Option String := none) + (messagesAsJson : Bool := false) : IO (Environment × Bool) := do let inputCtx := Parser.mkInputContext input fileName -- TODO: replace with `#lang` processing @@ -125,8 +126,7 @@ def runFrontend commandState := { commandState with infoState.enabled := true } let s ← IO.processCommands inputCtx parserState commandState - for msg in s.commandState.messages.toList do - IO.print (← msg.toString (includeEndPos := Language.printMessageEndPos.get opts)) + Language.reportMessages s.commandState.messages opts messagesAsJson if let some ileanFileName := ileanFileName? then let trees := s.commandState.infoState.trees.toArray @@ -141,7 +141,7 @@ def runFrontend let processor := Language.Lean.process let snap ← processor none ctx let snaps := Language.toSnapshotTree snap - snaps.runAndReport opts + snaps.runAndReport opts messagesAsJson if let some ileanFileName := ileanFileName? then let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[]) let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index e09fad85236c..1fcec4df9d62 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -142,14 +142,20 @@ register_builtin_option printMessageEndPos : Bool := { defValue := false, descr := "print end position of each message in addition to start position" } +/-- Report messages on stdout. If `messagesAsJson` is true, print messages as JSON (one per line). -/ +def reportMessages (msgLog : MessageLog) (opts : Options) (messagesAsJson := false) : IO Unit := do + if messagesAsJson then + msgLog.forM (·.toJson <&> (·.compress) >>= IO.println) + else + msgLog.forM (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print) + /-- Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are reported in tree preorder. This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how the language server reports snapshots asynchronously. -/ -partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) : IO Unit := do - s.element.diagnostics.msgLog.forM - (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print) +partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (messagesAsJson := false) : IO Unit := do + reportMessages s.element.diagnostics.msgLog opts messagesAsJson for t in s.children do t.get.runAndReport opts diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 3414b5c3b98b..87ca8535ce65 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -23,7 +23,7 @@ def mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String) (en inductive MessageSeverity where | information | warning | error - deriving Inhabited, BEq + deriving Inhabited, BEq, ToJson, FromJson structure MessageDataContext where env : Environment @@ -234,6 +234,16 @@ protected def toString (msg : Message) (includeEndPos := false) : IO String := d str := str ++ "\n" return str +protected def toJson (msg : Message) : IO Json := do + return Json.mkObj [ + ("severity", toJson msg.severity), + ("fileName", msg.fileName), + ("pos", toJson msg.pos), + ("endPos", toJson msg.endPos), + ("caption", msg.caption), + ("data", ← msg.data.toString), + ] + end Message /-- A persistent array of messages. -/ diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 9ed796413b7a..d206e240b0db 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -217,6 +217,7 @@ static void display_help(std::ostream & out) { #endif std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n"; std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n"; + std::cout << " --json print messages as JSON objects (one per line)\n"; std::cout << " --deps just print dependencies of a Lean input\n"; std::cout << " --print-prefix print the installation prefix for Lean and exit\n"; std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n"; @@ -230,6 +231,7 @@ static void display_help(std::ostream & out) { static int print_prefix = 0; static int print_libdir = 0; +static int json_messages = 0; static struct option g_long_options[] = { {"version", no_argument, 0, 'v'}, @@ -260,6 +262,7 @@ static struct option g_long_options[] = { #endif {"plugin", required_argument, 0, 'p'}, {"load-dynlib", required_argument, 0, 'l'}, + {"json", no_argument, &json_messages, 1}, {"print-prefix", no_argument, &print_prefix, 1}, {"print-libdir", no_argument, &print_libdir, 1}, #ifdef LEAN_DEBUG @@ -346,6 +349,7 @@ extern "C" object * lean_run_frontend( object * main_module_name, uint32_t trust_level, object * ilean_filename, + uint8_t messages_as_json, object * w ); pair_ref run_new_frontend( @@ -353,7 +357,8 @@ pair_ref run_new_frontend( options const & opts, std::string const & file_name, name const & main_module_name, uint32_t trust_level, - optional const & ilean_file_name + optional const & ilean_file_name, + uint8_t messages_as_json ) { object * oilean_file_name = mk_option_none(); if (ilean_file_name) { @@ -366,6 +371,7 @@ pair_ref run_new_frontend( main_module_name.to_obj_arg(), trust_level, oilean_file_name, + messages_as_json, io_mk_world() )); } @@ -716,7 +722,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { if (!main_module_name) main_module_name = name("_stdin"); - pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn); + pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_messages); env = r.fst(); bool ok = unbox(r.snd().raw()); From a1ca962f161407d2a71409a351607d05fcd31da7 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 18 Apr 2024 12:56:37 -0400 Subject: [PATCH 2/6] refactor: changes suggested by Sebastian --- src/Lean/Elab/Frontend.lean | 6 ++-- src/Lean/Language/Basic.lean | 10 +++--- src/Lean/Message.lean | 65 +++++++++++++++++++++++++----------- src/util/shell.cpp | 14 ++++---- 4 files changed, 60 insertions(+), 35 deletions(-) diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index 8d7d15f9754d..b07fd9b47da9 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -107,7 +107,7 @@ def runFrontend (mainModuleName : Name) (trustLevel : UInt32 := 0) (ileanFileName? : Option String := none) - (messagesAsJson : Bool := false) + (jsonOutput : Bool := false) : IO (Environment × Bool) := do let inputCtx := Parser.mkInputContext input fileName -- TODO: replace with `#lang` processing @@ -126,7 +126,7 @@ def runFrontend commandState := { commandState with infoState.enabled := true } let s ← IO.processCommands inputCtx parserState commandState - Language.reportMessages s.commandState.messages opts messagesAsJson + Language.reportMessages s.commandState.messages opts jsonOutput if let some ileanFileName := ileanFileName? then let trees := s.commandState.infoState.trees.toArray @@ -141,7 +141,7 @@ def runFrontend let processor := Language.Lean.process let snap ← processor none ctx let snaps := Language.toSnapshotTree snap - snaps.runAndReport opts messagesAsJson + snaps.runAndReport opts jsonOutput if let some ileanFileName := ileanFileName? then let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[]) let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 1fcec4df9d62..ec0cecb1a5eb 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -142,9 +142,9 @@ register_builtin_option printMessageEndPos : Bool := { defValue := false, descr := "print end position of each message in addition to start position" } -/-- Report messages on stdout. If `messagesAsJson` is true, print messages as JSON (one per line). -/ -def reportMessages (msgLog : MessageLog) (opts : Options) (messagesAsJson := false) : IO Unit := do - if messagesAsJson then +/-- Reports messages on stdout. If `json` is true, prints messages as JSON (one per line). -/ +def reportMessages (msgLog : MessageLog) (opts : Options) (json := false) : IO Unit := do + if json then msgLog.forM (·.toJson <&> (·.compress) >>= IO.println) else msgLog.forM (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print) @@ -154,8 +154,8 @@ def reportMessages (msgLog : MessageLog) (opts : Options) (messagesAsJson := fal reported in tree preorder. This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how the language server reports snapshots asynchronously. -/ -partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (messagesAsJson := false) : IO Unit := do - reportMessages s.element.diagnostics.msgLog opts messagesAsJson +partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do + reportMessages s.element.diagnostics.msgLog opts json for t in s.children do t.get.runAndReport opts diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 87ca8535ce65..8373d61f551c 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -205,9 +205,15 @@ instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr end MessageData -/-- A `Message` is a richly formatted piece of information emitted by Lean. -They are rendered by client editors in the infoview and in diagnostic windows. -/ -structure Message where +/-- +A `BaseMessage` is a richly formatted piece of information emitted by Lean. +They are rendered by client editors in the infoview and in diagnostic windows. +There are two varieties in the Lean core: +* `Message`: Uses structured, effectful `MessageData` for formatting content. +* `SerialMessage`: Stores pure `String` data. Obtained by running the effectful +`Message.serialize`. +-/ +structure BaseMessage (α : Type u) where fileName : String pos : Position endPos : Option Position := none @@ -216,33 +222,52 @@ structure Message where severity : MessageSeverity := MessageSeverity.error caption : String := "" /-- The content of the message. -/ - data : MessageData - deriving Inhabited + data : α + deriving Inhabited, ToJson, FromJson -namespace Message +/-- A `Message` is a richly formatted piece of information emitted by Lean. +They are rendered by client editors in the infoview and in diagnostic windows. -/ +abbrev Message := BaseMessage MessageData + +/-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly +serialized and is thus appropriate for use in pure contexts where the effectful +`MessageData.toString` cannot be used. -/ +abbrev SerialMessage := BaseMessage String + +namespace SerialMessage -protected def toString (msg : Message) (includeEndPos := false) : IO String := do - let mut str ← msg.data.toString +@[inline] def toMessage (msg : SerialMessage) : Message := + {msg with data := msg.data} + +instance : Coe SerialMessage Message := ⟨SerialMessage.toMessage⟩ + +protected def toString (msg : SerialMessage) (includeEndPos := false) : String := Id.run do + let mut str := msg.data let endPos := if includeEndPos then msg.endPos else none unless msg.caption == "" do str := msg.caption ++ ":\n" ++ str match msg.severity with - | MessageSeverity.information => pure () - | MessageSeverity.warning => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str - | MessageSeverity.error => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str + | .information => pure () + | .warning => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str + | .error => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str if str.isEmpty || str.back != '\n' then str := str ++ "\n" return str -protected def toJson (msg : Message) : IO Json := do - return Json.mkObj [ - ("severity", toJson msg.severity), - ("fileName", msg.fileName), - ("pos", toJson msg.pos), - ("endPos", toJson msg.endPos), - ("caption", msg.caption), - ("data", ← msg.data.toString), - ] +instance : ToString SerialMessage := ⟨SerialMessage.toString⟩ + +end SerialMessage + +namespace Message + +@[inline] def serialize (msg : Message) : IO SerialMessage := do + return {msg with data := ← msg.data.toString} + +@[inline] protected def toString (msg : Message) (includeEndPos := false) : IO String := do + return (← msg.serialize).toString includeEndPos + +@[inline] protected def toJson (msg : Message) : IO Json := do + return toJson (← msg.serialize) end Message diff --git a/src/util/shell.cpp b/src/util/shell.cpp index d206e240b0db..1209672b4a9f 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -217,7 +217,7 @@ static void display_help(std::ostream & out) { #endif std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n"; std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n"; - std::cout << " --json print messages as JSON objects (one per line)\n"; + std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n"; std::cout << " --deps just print dependencies of a Lean input\n"; std::cout << " --print-prefix print the installation prefix for Lean and exit\n"; std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n"; @@ -231,7 +231,7 @@ static void display_help(std::ostream & out) { static int print_prefix = 0; static int print_libdir = 0; -static int json_messages = 0; +static int json_output = 0; static struct option g_long_options[] = { {"version", no_argument, 0, 'v'}, @@ -262,7 +262,7 @@ static struct option g_long_options[] = { #endif {"plugin", required_argument, 0, 'p'}, {"load-dynlib", required_argument, 0, 'l'}, - {"json", no_argument, &json_messages, 1}, + {"json", no_argument, &json_output, 1}, {"print-prefix", no_argument, &print_prefix, 1}, {"print-libdir", no_argument, &print_libdir, 1}, #ifdef LEAN_DEBUG @@ -349,7 +349,7 @@ extern "C" object * lean_run_frontend( object * main_module_name, uint32_t trust_level, object * ilean_filename, - uint8_t messages_as_json, + uint8_t json_output, object * w ); pair_ref run_new_frontend( @@ -358,7 +358,7 @@ pair_ref run_new_frontend( name const & main_module_name, uint32_t trust_level, optional const & ilean_file_name, - uint8_t messages_as_json + uint8_t json ) { object * oilean_file_name = mk_option_none(); if (ilean_file_name) { @@ -371,7 +371,7 @@ pair_ref run_new_frontend( main_module_name.to_obj_arg(), trust_level, oilean_file_name, - messages_as_json, + json_output, io_mk_world() )); } @@ -722,7 +722,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { if (!main_module_name) main_module_name = name("_stdin"); - pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_messages); + pair_ref r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output); env = r.fst(); bool ok = unbox(r.snd().raw()); From d64388431c4f6b394099e08f3c30299abc637747 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 18 Apr 2024 13:08:18 -0400 Subject: [PATCH 3/6] refactor: `SnapshotTree.forM` --- src/Lean/Language/Basic.lean | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index ec0cecb1a5eb..7f15370276a7 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -135,6 +135,11 @@ class ToSnapshotTree (α : Type) where toSnapshotTree : α → SnapshotTree export ToSnapshotTree (toSnapshotTree) +/-- Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree preorder. -/ +@[specialize] partial def SnapshotTree.forM [Monad m] (s : SnapshotTree) + (f : Snapshot → m PUnit) : m PUnit := do + match s with | mk element children => f element; children.forM (·.get.forM f) + /-- Option for printing end position of each message in addition to start position. Used for testing message ranges in the test suite. -/ @@ -154,19 +159,12 @@ def reportMessages (msgLog : MessageLog) (opts : Options) (json := false) : IO U reported in tree preorder. This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how the language server reports snapshots asynchronously. -/ -partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do - reportMessages s.element.diagnostics.msgLog opts json - for t in s.children do - t.get.runAndReport opts +def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do + s.forM (reportMessages ·.diagnostics.msgLog opts json) /-- Waits on and returns all snapshots in the tree. -/ -partial def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot := - go s |>.run #[] |>.2 -where - go s : StateM (Array Snapshot) Unit := do - modify (·.push s.element) - for t in s.children do - go t.get +def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot := + s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2 /-- Metadata that does not change during the lifetime of the language processing process. -/ structure ModuleProcessingContext where @@ -219,7 +217,7 @@ end Language /-- Builds a function for processing a language using incremental snapshots by passing the previous snapshot to `Language.process` on subsequent invocations. -/ -partial def Language.mkIncrementalProcessor (process : Option InitSnap → ProcessingM InitSnap) +def Language.mkIncrementalProcessor (process : Option InitSnap → ProcessingM InitSnap) (ctx : ModuleProcessingContext) : BaseIO (Parser.InputContext → BaseIO InitSnap) := do let oldRef ← IO.mkRef none return fun ictx => do From 2724f26cec9e029f9f212fc7d68390b5d0ae9dea Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 18 Apr 2024 14:00:55 -0400 Subject: [PATCH 4/6] chore: inline fixes --- src/Lean/Message.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 8373d61f551c..af64ed00d471 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -263,11 +263,13 @@ namespace Message @[inline] def serialize (msg : Message) : IO SerialMessage := do return {msg with data := ← msg.data.toString} -@[inline] protected def toString (msg : Message) (includeEndPos := false) : IO String := do - return (← msg.serialize).toString includeEndPos +protected def toString (msg : Message) (includeEndPos := false) : IO String := do + -- Remark: We inline here to avoid a copy in the case were `msg` is shared + return inline <| (← msg.serialize).toString includeEndPos -@[inline] protected def toJson (msg : Message) : IO Json := do - return toJson (← msg.serialize) +protected def toJson (msg : Message) : IO Json := do + -- Remark: We inline here to avoid a copy in the case were `msg` is shared + return inline <| toJson (← msg.serialize) end Message From 6610dd6eb0128de4778f2c25c88bda5ef5504320 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 18 Apr 2024 14:05:27 -0400 Subject: [PATCH 5/6] chore: docstring line length / formatting --- src/Lean/Language/Basic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 7f15370276a7..7803777cc20e 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -135,7 +135,9 @@ class ToSnapshotTree (α : Type) where toSnapshotTree : α → SnapshotTree export ToSnapshotTree (toSnapshotTree) -/-- Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree preorder. -/ +/-- + Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree + preorder. -/ @[specialize] partial def SnapshotTree.forM [Monad m] (s : SnapshotTree) (f : Snapshot → m PUnit) : m PUnit := do match s with | mk element children => f element; children.forM (·.get.forM f) From 39580056e3e53d57436a331f66a4741e99ed15c5 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 19 Apr 2024 12:42:35 -0400 Subject: [PATCH 6/6] chore: address review comments --- src/Lean/Language/Basic.lean | 5 ++++- src/Lean/Message.lean | 6 ++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 7803777cc20e..2b1a20fc9ea1 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -140,7 +140,10 @@ export ToSnapshotTree (toSnapshotTree) preorder. -/ @[specialize] partial def SnapshotTree.forM [Monad m] (s : SnapshotTree) (f : Snapshot → m PUnit) : m PUnit := do - match s with | mk element children => f element; children.forM (·.get.forM f) + match s with + | mk element children => + f element + children.forM (·.get.forM f) /-- Option for printing end position of each message in addition to start position. Used for testing diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index af64ed00d471..012c8c187bdb 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -239,8 +239,6 @@ namespace SerialMessage @[inline] def toMessage (msg : SerialMessage) : Message := {msg with data := msg.data} -instance : Coe SerialMessage Message := ⟨SerialMessage.toMessage⟩ - protected def toString (msg : SerialMessage) (includeEndPos := false) : String := Id.run do let mut str := msg.data let endPos := if includeEndPos then msg.endPos else none @@ -264,11 +262,11 @@ namespace Message return {msg with data := ← msg.data.toString} protected def toString (msg : Message) (includeEndPos := false) : IO String := do - -- Remark: We inline here to avoid a copy in the case were `msg` is shared + -- Remark: The inline here avoids a new message allocation when `msg` is shared return inline <| (← msg.serialize).toString includeEndPos protected def toJson (msg : Message) : IO Json := do - -- Remark: We inline here to avoid a copy in the case were `msg` is shared + -- Remark: The inline here avoids a new message allocation when `msg` is shared return inline <| toJson (← msg.serialize) end Message