max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: test quotations in command elab

Browse source
This commit is contained in:
Sebastian Ullrich 2020-01-06 18:12:17 +01:00 • committed by Leonardo de Moura
parent 9b6eeacc0f
commit bc0802d76c
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Lean/Elab/Command.lean
View file

@ -275,14 +275,15 @@ private def addNamespace (ref : Syntax) (header : Name) : CommandElabM Unit :=
addScopes ref "namespace" true header
@[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
fun stx => addNamespace stx.val (stx.getIdAt 1)
fun stx => match_syntax stx.val with
| `(namespace $n) => addNamespace stx.val n.getId
| _ => throwUnexpectedSyntax stx.val "namespace"
@[builtinCommandElab «section»] def elabSection : CommandElab :=
fun stx => do
let header? := (stx.getArg 1).getOptionalIdent?;
match header? with
| some header => addScopes stx.val "section" false header
| none => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
fun stx => match_syntax stx.val with
| `(section $header:ident) => addScopes stx.val "section" false header.getId
| `(section) => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
| _ => throwUnexpectedSyntax stx.val "section"
def getScopes : CommandElabM (List Scope) := do
s ← get; pure s.scopes