doc: document Command.Scope (#4748)

Also extends existing definition for `getScope`/`getScopes` and
clarifies that the `end` command is optional at the end of a file.

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/Lean/Elab/Command.lean

@@ -12,17 +12,62 @@ import Lean.Language.Basic
 
 namespace Lean.Elab.Command
 
+/--
+A `Scope` records the part of the `CommandElabM` state that respects scoping,
+such as the data for `universe`, `open`, and `variable` declarations, the current namespace,
+and currently enabled options.
+The `CommandElabM` state contains a stack of scopes, and only the top `Scope`
+on the stack is read from or modified. There is always at least one `Scope` on the stack,
+even outside any `section` or `namespace`, and each new pushed `Scope`
+starts as a modified copy of the previous top scope.
+-/
 structure Scope where
+  /--
+  The component of the `namespace` or `section` that this scope is associated to.
+  For example, `section a.b.c` and `namespace a.b.c` each create three scopes with headers
+  named `a`, `b`, and `c`.
+  This is used for checking the `end` command. The "base scope" has `""` as its header.
+  -/
   header        : String
+  /--
+  The current state of all set options at this point in the scope. Note that this is the
+  full current set of options and does *not* simply contain the options set
+  while this scope has been active.
+  -/
   opts          : Options := {}
+  /-- The current namespace. The top-level namespace is represented by `Name.anonymous`. -/
   currNamespace : Name := Name.anonymous
+  /-- All currently `open`ed namespaces and names. -/
   openDecls     : List OpenDecl := []
+  /-- The current list of names for universe level variables to use for new declarations. This is managed by the `universe` command. -/
   levelNames    : List Name := []
-  /-- section variables -/
+  /--
+  The current list of binders to use for new declarations.
+  This is managed by the `variable` command.
+  Each binder is represented in `Syntax` form, and it is re-elaborated
+  within each command that uses this information.
+
+  This is also used by commands, such as `#check`, to create an initial local context,
+  even if they do not work with binders per se.
+  -/
   varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
-  /-- Globally unique internal identifiers for the `varDecls` -/
+  /--
+  Globally unique internal identifiers for the `varDecls`.
+  There is one identifier per variable introduced by the binders
+  (recall that a binder such as `(a b c : Ty)` can produce more than one variable),
+  and each identifier is the user-provided variable name with a macro scope.
+  This is used by `TermElabM` in `Lean.Elab.Term.Context` to help with processing macros
+  that capture these variables.
+  -/
   varUIds       : Array Name := #[]
-  /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
+  /--
+  If true (default: false), all declarations that fail to compile
+  automatically receive the `noncomputable` modifier.
+  A scope with this flag set is created by `noncomputable section`.
+
+  Recall that a new scope inherits all values from its parent scope,
+  so all sections and namespaces nested within a `noncomputable` section also have this flag set.
+  -/
   isNoncomputable : Bool := false
   deriving Inhabited
 
@@ -230,6 +275,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
 instance : MonadLiftT IO CommandElabM where
   monadLift := liftIO
 
+/-- Return the current scope. -/
 def getScope : CommandElabM Scope := do pure (← get).scopes.head!
 
 instance : MonadResolveName CommandElabM where
@@ -612,6 +658,11 @@ Interrupt and abort exceptions are caught but not logged.
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
   liftCoreM x
 
+/--
+Return the stack of all currently active scopes:
+the base scope always comes last; new scopes are prepended in the front.
+In particular, the current scope is always the first element.
+-/
 def getScopes : CommandElabM (List Scope) := do
   pure (← get).scopes
 

src/Lean/Parser/Command.lean

@@ -269,7 +269,7 @@ corresponding `end <id>` or the end of the file.
   "namespace " >> checkColGt >> ident
 /--
 `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
-with `end <id>`.
+with `end <id>`. The `end` command is optional at the end of a file.
 -/
 @[builtin_command_parser] def «end»          := leading_parser
   "end" >> optional (ppSpace >> checkColGt >> ident)