Info tree absence fixes

src/Lean/Elab/BuiltinCommand.lean

@@ -438,4 +438,7 @@ opaque elabEval : CommandElab
 @[builtin_command_elab Parser.Command.import] def elabImport : CommandElab := fun _ =>
   throwError "invalid 'import' command, it must be used in the beginning of the file"
 
+@[builtin_command_elab Parser.Command.eoi] def elabEoi : CommandElab := fun _ =>
+  return
+
 end Lean.Elab.Command

src/Lean/Elab/Command.lean

@@ -289,7 +289,9 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
             withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <|
               throwError "elaboration function for '{k}' has not been implemented"
           | elabFns => elabCommandUsing s stx elabFns
-    | _ => throwError "unexpected command"
+    | _ =>
+      withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <|
+        throwError "unexpected command"
 
 builtin_initialize registerTraceClass `Elab.input
 

src/Lean/Elab/Frontend.lean

@@ -62,11 +62,8 @@ def processCommand : FrontendM Bool := do
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps
     setMessages messages
-    if Parser.isEOI cmd then
-      pure true -- Done
-    else
-      profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
-      pure (Parser.isTerminalCommand cmd)
+    profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
+    pure (Parser.isTerminalCommand cmd)
 
 partial def processCommands : FrontendM Unit := do
   let done ← processCommand

src/Lean/Parser/Command.lean

@@ -273,6 +273,12 @@ def initializeKeyword := leading_parser
 @[builtin_command_parser] def genInjectiveTheorems := leading_parser
   "gen_injective_theorems% " >> ident
 
+/-- No-op parser used as syntax kind for attaching remaining whitespace to at the end of the input. -/
+@[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser ""
+
+builtin_initialize
+  registerBuiltinNodeKind ``eoi
+
 @[run_builtin_parser_attribute_hooks] abbrev declModifiersF := declModifiers false
 @[run_builtin_parser_attribute_hooks] abbrev declModifiersT := declModifiers true
 

src/Lean/Parser/Module.lean

@@ -51,13 +51,10 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
 
 private def mkEOI (pos : String.Pos) : Syntax :=
   let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""
-  mkNode `Lean.Parser.Module.eoi #[atom]
-
-def isEOI (s : Syntax) : Bool :=
-  s.isOfKind `Lean.Parser.Module.eoi
+  mkNode ``Command.eoi #[atom]
 
 def isTerminalCommand (s : Syntax) : Bool :=
-  s.isOfKind ``Command.exit || s.isOfKind ``Command.import
+  s.isOfKind ``Command.exit || s.isOfKind ``Command.import || s.isOfKind ``Command.eoi
 
 private def consumeInput (inputCtx : InputContext) (pmctx : ParserModuleContext) (pos : String.Pos) : String.Pos :=
   let s : ParserState := { cache := initCacheForInput inputCtx.input, pos := pos }
@@ -114,7 +111,7 @@ partial def testParseModuleAux (env : Environment) (inputCtx : InputContext) (s
   let rec parse (state : ModuleParserState) (msgs : MessageLog) (stxs : Array Syntax) :=
     match parseCommand inputCtx { env := env, options := {} } state msgs with
     | (stx, state, msgs) =>
-      if isEOI stx then
+      if isTerminalCommand stx then
         if msgs.isEmpty then
           pure stxs
         else do

src/Lean/Server/Snapshots.lean

@@ -59,7 +59,7 @@ def infoTree (s : Snapshot) : InfoTree :=
   s.cmdState.infoState.trees[0]!
 
 def isAtEnd (s : Snapshot) : Bool :=
-  Parser.isEOI s.stx || Parser.isTerminalCommand s.stx
+  Parser.isTerminalCommand s.stx
 
 open Command in
 /-- Use the command state in the given snapshot to run a `CommandElabM`.-/
@@ -110,54 +110,43 @@ def compileNextCmd (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidget
   let (cmdStx, cmdParserState, msgLog) :=
     Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
   let cmdPos := cmdStx.getPos?.get!
-  if Parser.isEOI cmdStx then
-    let endSnap : Snapshot := {
-      beginPos := cmdPos
-      stx := cmdStx
-      mpState := cmdParserState
-      cmdState := snap.cmdState
-      interactiveDiags := ← withNewInteractiveDiags msgLog
-      tacticCache := snap.tacticCache
-    }
-    return endSnap
-  else
-    let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
-    /- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive
-       access to the cache, we create a fresh reference here. Before this change, the
-       following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/
-    let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get)
-    let cmdCtx : Elab.Command.Context := {
-      cmdPos       := snap.endPos
-      fileName     := inputCtx.fileName
-      fileMap      := inputCtx.fileMap
-      tacticCache? := some tacticCacheNew
-    }
-    let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
-      Elab.Command.catchExceptions
-        (getResetInfoTrees *> Elab.Command.elabCommandTopLevel cmdStx)
-        cmdCtx cmdStateRef
-    let postNew := (← tacticCacheNew.get).post
-    snap.tacticCache.modify fun _ => { pre := postNew, post := {} }
-    let mut postCmdState ← cmdStateRef.get
-    if !output.isEmpty then
-      postCmdState := {
-        postCmdState with
-        messages := postCmdState.messages.add {
-          fileName := inputCtx.fileName
-          severity := MessageSeverity.information
-          pos      := inputCtx.fileMap.toPosition snap.endPos
-          data     := output
-        }
+  let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
+  /- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive
+      access to the cache, we create a fresh reference here. Before this change, the
+      following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/
+  let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get)
+  let cmdCtx : Elab.Command.Context := {
+    cmdPos       := snap.endPos
+    fileName     := inputCtx.fileName
+    fileMap      := inputCtx.fileMap
+    tacticCache? := some tacticCacheNew
+  }
+  let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
+    Elab.Command.catchExceptions
+      (getResetInfoTrees *> Elab.Command.elabCommandTopLevel cmdStx)
+      cmdCtx cmdStateRef
+  let postNew := (← tacticCacheNew.get).post
+  snap.tacticCache.modify fun _ => { pre := postNew, post := {} }
+  let mut postCmdState ← cmdStateRef.get
+  if !output.isEmpty then
+    postCmdState := {
+      postCmdState with
+      messages := postCmdState.messages.add {
+        fileName := inputCtx.fileName
+        severity := MessageSeverity.information
+        pos      := inputCtx.fileMap.toPosition snap.endPos
+        data     := output
       }
-    let postCmdSnap : Snapshot := {
-      beginPos := cmdPos
-      stx := cmdStx
-      mpState := cmdParserState
-      cmdState := postCmdState
-      interactiveDiags := ← withNewInteractiveDiags postCmdState.messages
-      tacticCache := (← IO.mkRef {})
     }
-    return postCmdSnap
+  let postCmdSnap : Snapshot := {
+    beginPos := cmdPos
+    stx := cmdStx
+    mpState := cmdParserState
+    cmdState := postCmdState
+    interactiveDiags := ← withNewInteractiveDiags postCmdState.messages
+    tacticCache := (← IO.mkRef {})
+  }
+  return postCmdSnap
 
 where
   /-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -80,3 +80,4 @@ a : α
           • [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
       • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
+[Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi

tests/lean/interactive/1525.lean

@@ -0,0 +1,3 @@
+-- should not produce any server panics
+structure Foo where
+  /--/-/

tests/lean/syntaxPrec.lean.expected.out

@@ -7,3 +7,4 @@ syntaxPrec.lean:1:18: error: expected ':'
           (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
             ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
               (ParserDescr.symbol✝ ", ") Bool.false✝)))
+[Elab.command]