pub fn parse_command_prefix_in_ctx(
ctx: &Context,
surface: &Surface,
input: &str,
) -> Result<(Command, usize), ParseError>Expand description
Parse ONE command off the FRONT of input with the kernel CONTEXT available, returning it
with the number of bytes consumed.
This is the primitive the context-aware doors are built from, exactly as
command_parser::parse_command_prefix_in is the primitive the text-only ones are built from:
parse_command_in_ctx adds “and nothing followed”, and a document splitter loops it.
One surface cannot be read from text alone. A literate Consider’s equation set has to be
compiled against the discriminant’s inductive, and the constructor list, its REGISTRATION
ORDER and their arities live in the kernel context; a parser holding only a &str can only
push one case per clause in SOURCE order — which silently computes a different function for
every equal-arity inductive, and cannot express a nested pattern or a catch-all at all.
## Theorem: is routed too, for the other fact text cannot carry: how many constructors
Proof: induction <v>. is eliminating over, so a bullet-count mistake is reported as one.
Both literate doors read their names in the surface’s NAMESPACE SCOPE and through the
context’s shadow table — the resolution every other door gets from the REPL — because they
must know what a name MEANS while they read: a clause is compiled against the constructors of
the inductive its discriminant really has, and a ## Theorem’s statement is reflected into
syntax naming the constants it really mentions. What they hand back is re-spelled
(surface::respell_names), so the REPL’s own resolution of it changes nothing.
Every other surface is routed to the context-free door untouched: this is a pre-dispatch on
two prefixes, not a second copy of the dispatcher. Repl reads every command through this
door when it runs it; the document splitter only measures, through
measure_command_prefix, since a block cannot be read against the context the blocks before
it have not built yet.