From bc0802d76ca3296abb71ab086392d16b2dd803b5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 6 Jan 2020 18:12:17 +0100 Subject: [PATCH] refactor: test quotations in command elab --- src/Init/Lean/Elab/Command.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index f2a5420acf..e95618d2ba 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/src/Init/Lean/Elab/Command.lean @@ -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