diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index e965135791..d934bf6ffc 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -82,7 +82,7 @@ where doAdd := do
   profileitM Exception "type checking" (← getOptions) do
     withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
       if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning m!"declaration uses 'sorry'"
+        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
       let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
         |> ofExceptKernelException
       setEnv env
diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index 8b6c6d12a9..4af49333af 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -59,12 +59,29 @@ structure WorkspaceClientCapabilities where
   workspaceEdit? : Option WorkspaceEditClientCapabilities := none
   deriving ToJson, FromJson
 
+structure LeanClientCapabilities where
+  /--
+  Whether the client supports `DiagnosticWith.isSilent = true`.
+  If `none` or `false`, silent diagnostics will not be served to the client.
+  -/
+  silentDiagnosticSupport? : Option Bool := none
+  deriving ToJson, FromJson
+
 structure ClientCapabilities where
   textDocument? : Option TextDocumentClientCapabilities := none
   window?       : Option WindowClientCapabilities       := none
   workspace?    : Option WorkspaceClientCapabilities    := none
+  /-- Capabilties for Lean language server extensions. -/
+  lean?         : Option LeanClientCapabilities         := none
   deriving ToJson, FromJson
 
+def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
+  let some lean := c.lean?
+    | return false
+  let some silentDiagnosticSupport := lean.silentDiagnosticSupport?
+    | return false
+  return silentDiagnosticSupport
+
 -- TODO largely unimplemented
 structure ServerCapabilities where
   textDocumentSync?         : Option TextDocumentSyncOptions := none
diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index da81c222a3..9dca235f30 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -66,13 +66,42 @@ inductive DiagnosticTag where
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 1 => return DiagnosticTag.unnecessary
-  | Except.ok 2 => return DiagnosticTag.deprecated
-  | _      => throw "unknown DiagnosticTag"⟩
+  | Except.ok 1  => return DiagnosticTag.unnecessary
+  | Except.ok 2  => return DiagnosticTag.deprecated
+  | _            => throw "unknown DiagnosticTag"⟩
 
 instance : ToJson DiagnosticTag := ⟨fun
-  | DiagnosticTag.unnecessary => (1 : Nat)
-  | DiagnosticTag.deprecated  => (2 : Nat)⟩
+  | DiagnosticTag.unnecessary   => (1 : Nat)
+  | DiagnosticTag.deprecated    => (2 : Nat)⟩
+
+/--
+Custom diagnostic tags provided by the language server.
+We use a separate diagnostic field for this to avoid confusing LSP clients with our custom tags.
+-/
+inductive LeanDiagnosticTag where
+  /--
+  Diagnostics representing an "unsolved goals" error.
+  Corresponds to `MessageData.tagged `Tactic.unsolvedGoals ..`.
+  -/
+  | unsolvedGoals
+  /--
+  Diagnostics representing a "goals accomplished" silent message.
+  Corresponds to `MessageData.tagged `goalsAccomplished ..`.
+  -/
+  | goalsAccomplished
+  deriving Inhabited, BEq, Ord
+
+instance : FromJson LeanDiagnosticTag where
+  fromJson? j :=
+    match j.getNat? with
+    | .ok 1 => return LeanDiagnosticTag.unsolvedGoals
+    | .ok 2 => return LeanDiagnosticTag.goalsAccomplished
+    | _     => throw "unknown LeanDiagnosticTag"
+
+instance : ToJson LeanDiagnosticTag where
+  toJson
+  | .unsolvedGoals => (1 : Nat)
+  | .goalsAccomplished => (2 : Nat)
 
 /-- Represents a related message and source code location for a diagnostic.
     This should be used to point to code locations that cause or are related to
@@ -94,6 +123,13 @@ structure DiagnosticWith (α : Type) where
   /-- Extension: preserve semantic range of errors when truncating them for display purposes. -/
   fullRange? : Option Range := some range
   severity? : Option DiagnosticSeverity := none
+  /--
+  Extension: whether this diagnostic should not be displayed as a regular diagnostic in the editor.
+  In VS Code, this means that the diagnostic does not have a squiggly and is not displayed in
+  the InfoView under 'All Messages', but it is still displayed under 'Messages'.
+  Defaults to `false`.
+  -/
+  isSilent? : Option Bool := none
   /-- The diagnostic's code, which might appear in the user interface. -/
   code? : Option DiagnosticCode := none
   /-- A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'. -/
@@ -104,6 +140,8 @@ structure DiagnosticWith (α : Type) where
   message : α
   /-- Additional metadata about the diagnostic. -/
   tags? : Option (Array DiagnosticTag) := none
+  /-- Additional Lean-specific metadata about the diagnostic. -/
+  leanTags? : Option (Array LeanDiagnosticTag) := none
   /-- An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property. -/
   relatedInformation? : Option (Array DiagnosticRelatedInformation) := none
   /-- A data entry field that is preserved between a `textDocument/publishDiagnostics` notification and `textDocument/codeAction` request. -/
diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index a19bb73a1e..846a4e0cdf 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -152,6 +152,8 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
     let mut toCheck : MessageLog := .empty
     let mut toPassthrough : MessageLog := .empty
     for msg in msgs.toList do
+      if msg.isSilent then
+        continue
       match specFn msg with
       | .check       => toCheck := toCheck.add msg
       | .drop        => pure ()
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index f15157c6bc..9cca94947d 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1068,6 +1068,47 @@ where
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"
 
+/--
+Logs a snapshot task that waits for the entire snapshot tree in `defsParsedSnap` and then logs a
+`goalsAccomplished` silent message for theorems and `Prop`-typed examples if the entire mutual block
+is error-free and contains no syntactical `sorry`s.
+-/
+private def logGoalsAccomplishedSnapshotTask (views : Array DefView)
+    (defsParsedSnap : DefsParsedSnapshot) : TermElabM Unit := do
+  let snaps := #[SnapshotTask.finished none (toSnapshotTree defsParsedSnap)] ++
+    (← getThe Core.State).snapshotTasks
+  let tree := SnapshotTree.mk { diagnostics := .empty } snaps
+  let logGoalsAccomplishedAct ← Term.wrapAsyncAsSnapshot (cancelTk? := none) fun () => do
+    -- NOTE: `waitAll` below ensures `getAll` will not block here
+    let logs := tree.getAll.map (·.diagnostics.msgLog)
+    let hasErrorOrSorry := logs.any fun log =>
+      log.reportedPlusUnreported.any fun msg =>
+        msg.severity matches .error || msg.data.hasTag (· == `hasSorry)
+    if hasErrorOrSorry then
+      return
+    for d in defsParsedSnap.defs, view in views do
+      let logGoalsAccomplished :=
+        let msgData := .tagged `goalsAccomplished m!"Goals accomplished!"
+        logAt view.ref msgData (severity := .information) (isSilent := true)
+      match view.kind with
+      | .theorem =>
+        logGoalsAccomplished
+      | .example =>
+        let some processedSnap := d.headerProcessedSnap.get
+          | continue
+        if ! (← isProp processedSnap.view.type) then
+          continue
+        logGoalsAccomplished
+      | _ => continue
+  let logGoalsAccomplishedTask ← BaseIO.mapTask (t := ← tree.waitAll) fun _ =>
+    logGoalsAccomplishedAct
+  Core.logSnapshotTask {
+    stx? := none
+    -- Use first line of the mutual block to avoid covering the progress of the whole mutual block
+    reportingRange? := (← getRef).getPos?.map fun pos => ⟨pos, pos⟩
+    task := logGoalsAccomplishedTask
+  }
+
 end Term
 namespace Command
 
@@ -1110,11 +1151,14 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
       }
       reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
     views := views.push view
+  let defsParsedSnap := { defs, diagnostics := .empty : DefsParsedSnapshot }
   if let some snap := snap? then
     -- no non-fatal diagnostics at this point
-    snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
+    snap.new.resolve <| .ofTyped defsParsedSnap
   let sc ← getScope
-  runTermElabM fun vars => Term.elabMutualDef vars sc views
+  runTermElabM fun vars => do
+    Term.elabMutualDef vars sc views
+    Term.logGoalsAccomplishedSnapshotTask views defsParsedSnap
 
 builtin_initialize
   registerTraceClass `Elab.definition.mkClosure
diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean
index 40acaa916b..3876b24e05 100644
--- a/src/Lean/Language/Basic.lean
+++ b/src/Lean/Language/Basic.lean
@@ -287,12 +287,13 @@ def reportMessages (msgLog : MessageLog) (opts : Options)
         {msg with severity}
       else
         msg
-    if json then
-      let j ← msg.toJson
-      IO.println j.compress
-    else
-      let s ← msg.toString includeEndPos
-      IO.print s
+    unless msg.isSilent do
+      if json then
+        let j ← msg.toJson
+        IO.println j.compress
+      else
+        let s ← msg.toString includeEndPos
+        IO.print s
     return hasErrors || msg.severity matches .error
 
 /--
diff --git a/src/Lean/Language/Util.lean b/src/Lean/Language/Util.lean
index 24751c4cb0..e9a1875758 100644
--- a/src/Lean/Language/Util.lean
+++ b/src/Lean/Language/Util.lean
@@ -22,7 +22,8 @@ where go range? s := do
   let mut desc := f!"{s.element.desc}"
   if let some range := range? then
     desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} "
-  desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString))
+  let msgs ← s.element.diagnostics.msgLog.toList.mapM (·.toString)
+  desc := desc ++ .prefixJoin "\n• " msgs
   withTraceNode `Elab.snapshotTree (fun _ => pure desc) do
     s.children.toList.forM fun c => go c.reportingRange? c.get
     if let some t := s.element.infoTree? then
diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean
index 6485e15a1f..d3a09b3ad5 100644
--- a/src/Lean/Log.lean
+++ b/src/Lean/Log.lean
@@ -58,7 +58,8 @@ Log the message `msgData` at the position provided by `ref` with the given `seve
 If `getRef` has position information but `ref` does not, we use `getRef`.
 We use the `fileMap` to find the line and column numbers for the error message.
 -/
-def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error) : m Unit :=
+def logAt (ref : Syntax) (msgData : MessageData)
+    (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : m Unit :=
   unless severity == .error && msgData.hasSyntheticSorry do
     let severity := if severity == .warning && warningAsError.get (← getOptions) then .error else severity
     let ref    := replaceRef ref (← MonadLog.getRef)
@@ -66,7 +67,14 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
     let endPos := ref.getTailPos?.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
+    logMessage {
+      fileName := (← getFileName)
+      pos := fileMap.toPosition pos
+      endPos := fileMap.toPosition endPos
+      data := msgData
+      severity
+      isSilent
+    }
 
 /-- Log a new error message using the given message data. The position is provided by `ref`. -/
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index e7e6bf8025..9730764f15 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -347,6 +347,12 @@ structure BaseMessage (α : Type u) where
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
   severity      : MessageSeverity := .error
+  /--
+  If `true`, filter this message from non-language server output.
+  In the language server, silent messages are served as silent diagnostics.
+  See also `DiagnosticWith.isSilent?`.
+  -/
+  isSilent      : Bool := false
   caption       : String          := ""
   /-- The content of the message. -/
   data          : α
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index fab55b498d..8486dcbe9d 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -268,7 +268,10 @@ This option can only be set on the command line, not in the lakefile or via `set
               return (← ref.get).bind (·.get? MemorizedInteractiveDiagnostics) then
             pure memorized.diags
           else
-            let diags ← node.element.diagnostics.msgLog.toArray.mapM
+            let mut msgs := node.element.diagnostics.msgLog.toArray
+            if ! ctx.initParams.capabilities.silentDiagnosticSupport then
+              msgs := msgs.filter (! ·.isSilent)
+            let diags ← msgs.mapM
               (Widget.msgToInteractiveDiagnostic doc.meta.text · ctx.clientHasWidgets)
             if let some cacheRef := node.element.diagnostics.interactiveDiagsRef? then
               cacheRef.set <| some <| .mk { diags : MemorizedInteractiveDiagnostics }
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 25d3d02801..c7fd6cbe28 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -234,14 +234,19 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool
     | .information => .information
     | .warning     => .warning
     | .error       => .error
+  let isSilent? := if m.isSilent then some true else none
   let source? := some "Lean 4"
   let tags? :=
     if m.data.isDeprecationWarning then some #[.deprecated]
     else if m.data.isUnusedVariableWarning then some #[.unnecessary]
     else none
+  let leanTags? :=
+    if m.data.hasTag (· == `Tactic.unsolvedGoals) then some #[.unsolvedGoals]
+    else if m.data.hasTag (· == `goalsAccomplished) then some #[.goalsAccomplished]
+    else none
   let message := match (← msgToInteractive m.data hasWidgets |>.toBaseIO) with
     | .ok msg => msg
     | .error ex => TaggedText.text s!"[error when printing message: {ex.toString}]"
-  pure { range, fullRange? := some fullRange, severity?, source?, message, tags? }
+  pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent? }
 
 end Lean.Widget
diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 356ecae7af..c8159f8570 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -56,7 +56,8 @@ def compileLeanModule
       if let .ok (msg : SerialMessage) := Json.parse ln >>= fromJson? then
         unless txt.isEmpty do
           logInfo s!"stdout:\n{txt}"
-        logSerialMessage msg
+        unless msg.isSilent do
+          logSerialMessage msg
         return txt
       else if txt.isEmpty && ln.isEmpty then
         return txt
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index e05aa21b29..bc9cf3e00b 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/src/lake/Lake/Load/Lean/Elab.lean
@@ -70,6 +70,8 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
 
   -- Log messages
   for msg in s.commandState.messages.toList do
+    if msg.isSilent then
+      continue
     match msg.severity with
     | MessageSeverity.information => logInfo (← msg.toString)
     | MessageSeverity.warning     => logWarning (← msg.toString)
diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out
index c98090e749..5ebca885ae 100644
--- a/tests/lean/interactive/4880.lean.expected.out
+++ b/tests/lean/interactive/4880.lean.expected.out
@@ -47,6 +47,7 @@
    {"start": {"line": 34, "character": 13},
     "end": {"line": 35, "character": 0}},
    "message": "unsolved goals\n⊢ A",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 34, "character": 13},
     "end": {"line": 36, "character": 0}}}]}
diff --git a/tests/lean/interactive/haveInfo.lean.expected.out b/tests/lean/interactive/haveInfo.lean.expected.out
index 786f0ecea5..7cb553e8e4 100644
--- a/tests/lean/interactive/haveInfo.lean.expected.out
+++ b/tests/lean/interactive/haveInfo.lean.expected.out
@@ -6,6 +6,7 @@
    "range":
    {"start": {"line": 4, "character": 17}, "end": {"line": 5, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 4, "character": 17}, "end": {"line": 7, "character": 8}}},
   {"source": "Lean 4",
@@ -14,6 +15,7 @@
    {"start": {"line": 11, "character": 17},
     "end": {"line": 12, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 11, "character": 17},
     "end": {"line": 14, "character": 8}}},
@@ -23,6 +25,7 @@
    {"start": {"line": 18, "character": 17},
     "end": {"line": 19, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 18, "character": 17},
     "end": {"line": 21, "character": 8}}},
@@ -32,6 +35,7 @@
    {"start": {"line": 25, "character": 17},
     "end": {"line": 26, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 25, "character": 17},
     "end": {"line": 28, "character": 8}}}]}
diff --git a/tests/lean/interactive/incrementalCombinator.lean.expected.out b/tests/lean/interactive/incrementalCombinator.lean.expected.out
index 23e110d3d7..8a4f7f9bb1 100644
--- a/tests/lean/interactive/incrementalCombinator.lean.expected.out
+++ b/tests/lean/interactive/incrementalCombinator.lean.expected.out
@@ -33,6 +33,7 @@ sh
    "range":
    {"start": {"line": 2, "character": 17}, "end": {"line": 3, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 17},
     "end": {"line": 6, "character": 18}}},
@@ -41,6 +42,7 @@ sh
    "range":
    {"start": {"line": 1, "character": 24}, "end": {"line": 2, "character": 0}},
    "message": "unsolved goals\nthis : True\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 1, "character": 24},
     "end": {"line": 6, "character": 18}}}]}
@@ -53,6 +55,7 @@ sh
    "range":
    {"start": {"line": 2, "character": 18}, "end": {"line": 3, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 18},
     "end": {"line": 6, "character": 18}}},
@@ -61,6 +64,7 @@ sh
    "range":
    {"start": {"line": 1, "character": 24}, "end": {"line": 2, "character": 0}},
    "message": "unsolved goals\nthis : True\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 1, "character": 24},
     "end": {"line": 6, "character": 18}}}]}
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index b429e40063..d80721785b 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -23,6 +23,7 @@ t 2
    "range":
    {"start": {"line": 2, "character": 22}, "end": {"line": 3, "character": 0}},
    "message": "unsolved goals\nthis : Nat → Nat → True\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 22},
     "end": {"line": 10, "character": 11}}}]}
@@ -52,6 +53,7 @@ t 2
    "range":
    {"start": {"line": 3, "character": 9}, "end": {"line": 3, "character": 16}},
    "message": "unsolved goals\n⊢ Nat",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 3, "character": 9},
     "end": {"line": 3, "character": 16}}}]}
@@ -83,6 +85,7 @@ s
    "range":
    {"start": {"line": 3, "character": 12}, "end": {"line": 3, "character": 16}},
    "message": "unsolved goals\ncase zero\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 3, "character": 12},
     "end": {"line": 3, "character": 16}}}]}
@@ -94,6 +97,7 @@ s
    "range":
    {"start": {"line": 2, "character": 6}, "end": {"line": 2, "character": 10}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 2, "character": 6}, "end": {"line": 2, "character": 10}}},
   {"source": "Lean 4",
diff --git a/tests/lean/interactive/issue4527.lean.expected.out b/tests/lean/interactive/issue4527.lean.expected.out
index 0a542d8842..2a9be78d5e 100644
--- a/tests/lean/interactive/issue4527.lean.expected.out
+++ b/tests/lean/interactive/issue4527.lean.expected.out
@@ -6,5 +6,6 @@
    "range":
    {"start": {"line": 1, "character": 2}, "end": {"line": 2, "character": 0}},
    "message": "unsolved goals\n⊢ True",
+   "leanTags": [1],
    "fullRange":
    {"start": {"line": 1, "character": 2}, "end": {"line": 3, "character": 8}}}]}