diff --git a/doc/UsersGuide/Extensions.lean b/doc/UsersGuide/Extensions.lean
index d6f0970cb..9fa08d546 100644
--- a/doc/UsersGuide/Extensions.lean
+++ b/doc/UsersGuide/Extensions.lean
@@ -31,12 +31,14 @@ tag := "extension-syntax"
 All four extension points share a common syntax.
 They are invoked by name, with a sequence of arguments.
 These arguments may be positional or by name, and their values may be identifiers, string literals, or numbers.
+Boolean flags may be passed by preceding their name with `-` or `+` for {lean}`false` or {lean}`true`, respectively.
 
 :::paragraph
 In this example, the directive `syntax` is invoked with the positional argument `term` and the named argument `title` set to `"Example"`.
+The flag `check` is set to `false`.
 It contains a descriptive paragraph and the code block `grammar`, which is invoked with no arguments:
 ````
-:::syntax term (title := example)
+:::syntax term (title := example) -check
 This is an example grammar:
 ```grammar
 term ::= term "<+-+>" term
@@ -49,7 +51,7 @@ term ::= term "<+-+>" term
 More formally, an invocation of an extension should match this grammar:
 ```
 CALL := IDENT ARG*
-ARG := VAL | "(" IDENT ":=" VAL ")"
+ARG := VAL | "(" IDENT ":=" VAL ")" | "+" IDENT | "-" IDENT
 VAL := IDENT | STRING | NUM
 ```
 A `CALL` may occur after an opening fence on a code block.
diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean
index 316cb4fb2..d00047f58 100644
--- a/doc/UsersGuide/Markup.lean
+++ b/doc/UsersGuide/Markup.lean
@@ -97,7 +97,7 @@ partial def preview (stx : Syntax) : m Std.Format :=
   | `(block| command{$x $args*}) => do
     let args ← args.toList.mapM (preview ·.raw)
     pure s!"<{x.getId.toString} {Std.Format.prefixJoin " " args |>.pretty}/>"
-  | `(argument|$x:ident := $v) => do
+  | `(argument|($x:ident := $v)) | `(argument|$x:ident := $v) => do
     pure <| s!"{x.getId.toString}=\"{← preview v.raw}\""
   | `(argument|$v:arg_val) => preview v.raw
   | `(arg_val|$v:ident) => pure s!"{v.getId}"
@@ -419,6 +419,15 @@ Metadata blocks begin and end with `%%%`, and they contain any syntax that would
 ```
 :::
 
+:::markupPreview "Blah"
+```
+a b c
+```
+```
+<p> a b c </p>
+```
+:::
+
 
 ## Block Syntax
 %%%
diff --git a/doc/UsersGuide/Output.lean b/doc/UsersGuide/Output.lean
index 73bdba854..8a08e77c8 100644
--- a/doc/UsersGuide/Output.lean
+++ b/doc/UsersGuide/Output.lean
@@ -56,7 +56,7 @@ The differences are:
  * Interpolated Lean strings (with `s!`) may be used in any context that expects a string.
 
 For example, this definition creates a `<ul>` list:
-```lean (keep := false) (name := htmllist)
+```lean -keep (name := htmllist)
 open Verso.Output.Html
 
 def mkList (xs : List Html) : Html :=
@@ -100,7 +100,7 @@ The differences are:
  * Interpolated Lean strings (with `s!`) may be used in any context that expects a string.
 
 For example, this definition creates a bulleted list list:
-```lean (keep := false) (name := texlist)
+```lean -keep (name := texlist)
 open Verso.Output.TeX
 
 def mkList (xs : List TeX) : TeX :=
diff --git a/examples/package-manual/PackageManual.lean b/examples/package-manual/PackageManual.lean
index 14f14110b..27c927b01 100644
--- a/examples/package-manual/PackageManual.lean
+++ b/examples/package-manual/PackageManual.lean
@@ -205,12 +205,12 @@ If incorrect hovers are appearing locally, then try disabling caching in your br
 {index}[index]
 The index should contain an entry for “lorem ipsum”.
 {index}[lorem ipsum] foo
-{index subterm:="of lorem"}[ipsum]
-{index subterm:="per se"}[ipsum]
+{index (subterm:="of lorem")}[ipsum]
+{index (subterm:="per se")}[ipsum]
 {index}[ipsum]
 Lorem ipsum dolor {index}[dolor] sit amet, consectetur adipiscing elit, sed {index}[sed] do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris {index}[laboris] {see "lorem ipsum"}[laboris] {seeAlso "dolor"}[laboris] nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
 
-This is done using the `{index}[term]` syntax. Sub-terms {index subterm:="sub-term"}[entry] can be added using the `subterm` parameter to `index`.
+This is done using the `{index}[term]` syntax. Sub-terms {index (subterm:="sub-term")}[entry] can be added using the `subterm` parameter to `index`.
 
 Multiple index {index}[index] targets for a term also work.
 
diff --git a/examples/package-manual/PackageManual/DocFeatures.lean b/examples/package-manual/PackageManual/DocFeatures.lean
index 4bd827518..a23ebea01 100644
--- a/examples/package-manual/PackageManual/DocFeatures.lean
+++ b/examples/package-manual/PackageManual/DocFeatures.lean
@@ -34,7 +34,7 @@ The example project must depend on the same version of `subverso` that the docum
 Within the example project, examples are drawn from a module.
 Sometimes, the entire module is the example, while other cases use just some part of the module.
 To set a default module, use the option {option}`verso.exampleModule`.
-When there is no default set, or to override it, the example code features all accept a keyword argument `module`.{index subterm:="keyword argument"}[`module`]
+When there is no default set, or to override it, the example code features all accept a keyword argument `module`.{index (subterm:="keyword argument")}[`module`]
 
 {optionDocs verso.exampleModule}
 
@@ -82,7 +82,7 @@ The comments themselves are removed, and there is no requirement that anchors be
 :::
 
 :::paragraph
-Anchors can be specified using the `(anchor := anAnchor)`{index subterm:="keyword agument"}[`anchor`] parameter to each module form.
+Anchors can be specified using the `(anchor := anAnchor)`{index (subterm:="keyword agument")}[`anchor`] parameter to each module form.
 Additionally, there are macro versions that take anchor names positionally, so for example
 ````
 ```anchor anAnchor
diff --git a/examples/textbook/DemoTextbook.lean b/examples/textbook/DemoTextbook.lean
index 5fd0460b7..f300156b6 100644
--- a/examples/textbook/DemoTextbook.lean
+++ b/examples/textbook/DemoTextbook.lean
@@ -78,7 +78,7 @@ It can be both checked and included in the document using {lean}`leanOutput`:
 ```
 
 Expected error messages must be indicated explicitly:
-```lean (error := true) (name := yVal)
+```lean +error (name := yVal)
 #eval y
 ```
 ```leanOutput yVal
@@ -138,12 +138,12 @@ If incorrect hovers are appearing locally, then try disabling caching in your br
 {index}[index]
 The index should contain an entry for “lorem ipsum”.
 {index}[lorem ipsum] foo
-{index subterm:="of lorem"}[ipsum]
-{index subterm:="per se"}[ipsum]
+{index (subterm:="of lorem")}[ipsum]
+{index (subterm:="per se")}[ipsum]
 {index}[ipsum]
 Lorem ipsum dolor {index}[dolor] sit amet, consectetur adipiscing elit, sed {index}[sed] do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris {index}[laboris] {see "lorem ipsum"}[laboris] {seeAlso "dolor"}[laboris] nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
 
-This is done using the `{index}[term]` syntax. Sub-terms {index subterm:="sub-term"}[entry] can be added using the `subterm` parameter to `index`.
+This is done using the `{index}[term]` syntax. Sub-terms {index (subterm:="sub-term")}[entry] can be added using the `subterm` parameter to `index`.
 
 Multiple index {index}[index] targets for a term also work.
 
diff --git a/examples/website/DemoSite/Blog/AnchorBased.lean b/examples/website/DemoSite/Blog/AnchorBased.lean
index 839943c5b..f1a131046 100644
--- a/examples/website/DemoSite/Blog/AnchorBased.lean
+++ b/examples/website/DemoSite/Blog/AnchorBased.lean
@@ -83,7 +83,7 @@ branch l v r ih1 ih2
 ```
 
 This rendering of the same proof doesn't have proof states:
-```anchor proof1 (showProofStates := false)
+```anchor proof1 -showProofStates
 theorem Tree.flip_flip_eq_id :
     flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
diff --git a/examples/website/DemoSite/Blog/Conditionals.lean b/examples/website/DemoSite/Blog/Conditionals.lean
index 81eaff40c..802e24f5b 100644
--- a/examples/website/DemoSite/Blog/Conditionals.lean
+++ b/examples/website/DemoSite/Blog/Conditionals.lean
@@ -37,7 +37,7 @@ Here are some examples:
 ```
 
 
-```lean demo (error := true) (name := fst)
+```lean demo +error (name := fst)
 example := if true then 1 else 2
 example := if True then 1 else 2
 example : Int := if True then 1 else 2
@@ -82,7 +82,7 @@ theorem lt_4 (b : Bool) : (if b then 1 else 2) < 4 := by
 ```
 
 And hide proof states:
-```lean demo (showProofStates := false)
+```lean demo -showProofStates
 theorem lt_4' (b : Bool) : (if b then 1 else 2) < 4 := by
   split
   . skip; decide
@@ -221,7 +221,7 @@ elab "%more_info(" t:term ")" : term => do
   elabTerm t none
 ```
 
-````lean demo error:=true
+````lean demo +error
 example := %much_info(22)
 
 example := %more_info(25)
@@ -230,7 +230,7 @@ example := %more_info(25)
 The info gets stacked up, with the greatest severity highlighting the range in question.
 
 Here's some hoverable info:
-```lean demo (error := true) (name := typeErr)
+```lean demo +error (name := typeErr)
 example : Nat := "Not a number"
 ```
 ```leanOutput typeErr
@@ -244,7 +244,7 @@ but is expected to have type
 
 
 Here's some traces:
-```lean demo (error := true) (name := traces)
+```lean demo +error (name := traces)
 set_option trace.compiler.ir.result true in
 def f' (xs : List Nat) := xs.foldl (init := 0) (· + ·)
 
diff --git a/examples/website/DemoSite/Blog/Subprojects.lean b/examples/website/DemoSite/Blog/Subprojects.lean
index 1b64f438b..f49110a61 100644
--- a/examples/website/DemoSite/Blog/Subprojects.lean
+++ b/examples/website/DemoSite/Blog/Subprojects.lean
@@ -56,7 +56,7 @@ Version is:
 {leanCommand examples Examples.version}
 
 that is,
-```leanOutput Examples.version severity := information
+```leanOutput Examples.version (severity := information)
 "4.5.0"
 ```
 
@@ -70,7 +70,7 @@ Tree.branch
 ```
 
 lax:
-```leanOutput Examples.basic whitespace := lax
+```leanOutput Examples.basic (whitespace := lax)
 Tree.branch
   (Tree.branch
     (Tree.leaf)
@@ -81,7 +81,7 @@ Tree.branch
 ```
 
 and normalized matching:
-```leanOutput Examples.basic whitespace := normalized
+```leanOutput Examples.basic (whitespace := normalized)
 Tree.branch   (Tree.branch (Tree.leaf) 4 (Tree.branch (Tree.leaf) 3 (Tree.leaf)))
   2   (Tree.branch (Tree.leaf) 1 (Tree.leaf))
 ```
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index 6abfcf54f..db85e08c7 100644
--- a/src/verso-blog/VersoBlog.lean
+++ b/src/verso-blog/VersoBlog.lean
@@ -310,7 +310,7 @@ variable [Monad m] [MonadError m] [MonadLiftT CoreM m]
 
 instance : FromArgs LeanCommandConfig m where
   fromArgs :=
-    LeanCommandConfig.mk <$> .positional `project .ident <*> .positional `exampleName .ident <*> .namedD `showProofStates .bool true
+    LeanCommandConfig.mk <$> .positional `project .ident <*> .positional `exampleName .ident <*> .flag `showProofStates true
 end
 
 @[block_command]
@@ -385,7 +385,7 @@ instance : FromArgs LeanTermArgs DocElabM where
   fromArgs :=
     LeanTermArgs.mk <$>
       .positional `project .ident <*>
-      .namedD `showProofStates .bool true
+      .flag `showProofStates true
 
 @[role]
 def leanTerm : RoleExpanderOf LeanTermArgs
@@ -406,18 +406,38 @@ def leanTerm : RoleExpanderOf LeanTermArgs
 
 structure LeanBlockConfig where
   exampleContext : Ident
-  «show» : Option Bool := none
-  keep : Option Bool := none
+  «show» : Bool
+  keep : Bool
   name : Option Name := none
-  error : Option Bool := none
+  error : Bool
   /-- Whether to render proof states -/
-  showProofStates : Bool := true
+  showProofStates : Bool
 
 instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanBlockConfig m where
-  fromArgs := LeanBlockConfig.mk <$> .positional `exampleContext .ident <*> .named `show .bool true <*> .named `keep .bool true <*> .named `name .name true <*> .named `error .bool true <*> .namedD `showProofStates .bool true
+  fromArgs :=
+    LeanBlockConfig.mk <$>
+      .positional `exampleContext .ident <*>
+      .flag `show true "Include in rendered page?" <*>
+      .flag `keep true "Keep environment changes from this block?" <*>
+      .named `name .name true <*>
+      .flag `error false "Error expected in code?" <*>
+      .flag `showProofStates true "Show proof states in rendered page?"
+
+def LeanInitBlockConfig := LeanBlockConfig
+
+instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanInitBlockConfig m where
+  fromArgs :=
+    LeanBlockConfig.mk <$>
+      .positional `exampleContext .ident <*>
+      .flag `show false "Include in rendered page?" <*>
+      .flag `keep true "Keep environment changes from this block?" <*>
+      .named `name .name true <*>
+      .flag `error false "Error expected in code?" <*>
+      .flag `showProofStates true "Show proof states in rendered page?"
+
 
 @[code_block]
-def leanInit : CodeBlockExpanderOf LeanBlockConfig
+def leanInit : CodeBlockExpanderOf LeanInitBlockConfig
   | config , str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanInit") <| do
     let context := Parser.mkInputContext (← parserInputString str) (← getFileName)
     let (header, state, msgs) ← Parser.parseHeader context
@@ -440,7 +460,7 @@ def leanInit : CodeBlockExpanderOf LeanBlockConfig
         let commandState := configureCommandState env {}
         let commandState := { commandState with scopes := [{ header := "", opts := pp.tagAppFns.set {} true }] }
         modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState state)}
-    if config.show.getD false then
+    if config.show then
       ``(Block.code $(quote str.getString)) -- TODO highlighting hack
     else
       ``(Block.concat #[])
@@ -466,29 +486,22 @@ def lean : CodeBlockExpanderOf LeanBlockConfig
     for t in s.commandState.infoState.trees do
       pushInfoTree t
 
-    match config.error with
-    | none =>
-      for msg in s.commandState.messages.toArray do
-        -- These errors break the build! Silence everything else to clean up output, but keep these.
-        if msg.severity != .error then
-          logMessage {msg with isSilent := true}
-        else
-          logMessage msg
-    | some true =>
+    if config.error then
       if s.commandState.messages.hasErrors then
         -- Nothing breaks the build here, so silence them all
         for msg in s.commandState.messages.errorsToWarnings.toArray do
           logMessage {msg with isSilent := true}
       else
         throwErrorAt str "Error expected in code block, but none occurred"
-    | some false =>
+    else
       for msg in s.commandState.messages.toArray do
-        -- Nothing breaks the build here, so silence them all
-        logMessage {msg with isSilent := true}
-      if s.commandState.messages.hasErrors then
-        throwErrorAt str "No error expected in code block, one occurred"
+        -- These errors break the build! Silence everything else to clean up output, but keep these.
+        if msg.severity != .error then
+          logMessage {msg with isSilent := true}
+        else
+          logMessage msg
 
-    if config.keep.getD true && !(config.error.getD false) then
+    if config.keep && !config.error then
       modifyEnv fun env => exampleContextExt.modifyState env fun st => {st with
         contexts := st.contexts.insert x.getId (.inline {s.commandState with messages := {} } s.parserState)
       }
@@ -511,7 +524,7 @@ def lean : CodeBlockExpanderOf LeanBlockConfig
       finally
         setInfoState infoSt
         setEnv env
-      if config.show.getD true then
+      if config.show then
         `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote x.getId), showProofStates := $(quote config.showProofStates) } $(quote hls)) #[Block.code $(quote str.getString)])
       else
         ``(Block.concat [])
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 7af16537b..bb266f68a 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -1391,7 +1391,7 @@ structure DocstringConfig where
   /--
   Ignores the option `verso.docstring.allowMissing` and allows _this_ docstring to be missing.
   -/
-  allowMissing : Option Bool := none
+  allowMissing : Bool
   /-- Suppress the fields of a structure. -/
   hideFields : Bool := false
   /-- Suppress the constructor of a structure or class. -/
@@ -1406,9 +1406,10 @@ variable [MonadLog m] [AddMessageContext m] [Elab.MonadInfoTree m]
 def DocstringConfig.parse : ArgParse m DocstringConfig :=
   DocstringConfig.mk <$>
     .positional `name .documentableName <*>
-    .named `allowMissing .bool true <*>
-    .namedD `hideFields .bool false <*>
-    .namedD `hideStructureConstructor .bool false <*>
+    .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions)
+      "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)" <*>
+    .flag `hideFields false <*>
+    .flag `hideStructureConstructor false <*>
     .named `label .string true
 
 instance : FromArgs DocstringConfig m := ⟨DocstringConfig.parse⟩
@@ -1418,7 +1419,7 @@ end
 @[block_command]
 def docstring : BlockCommandOf DocstringConfig
   | ⟨(x, name), allowMissing, hideFields, hideCtor, customLabel⟩ => do
-    let opts : Options → Options := allowMissing.map (fun b opts => verso.docstring.allowMissing.set opts b) |>.getD id
+    let opts : Options → Options := (verso.docstring.allowMissing.set · allowMissing)
 
     withOptions opts do
       Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation")
@@ -1506,7 +1507,7 @@ structure IncludeDocstringOpts where
   elaborate : Bool
 
 def IncludeDocstringOpts.parse : ArgParse m IncludeDocstringOpts :=
-  IncludeDocstringOpts.mk <$> (.positional `name .documentableName <&> (·.2)) <*> .namedD `elab .bool true
+  IncludeDocstringOpts.mk <$> (.positional `name .documentableName <&> (·.2)) <*> .flag `elab true
 
 instance : FromArgs IncludeDocstringOpts m where
   fromArgs := IncludeDocstringOpts.parse
@@ -1644,18 +1645,19 @@ structure TacticDocsOptions where
   name : StrLit ⊕ Ident
   «show» : Option String
   replace : Bool
-  allowMissing : Option Bool
+  allowMissing : Bool
 
 section
 
-variable [Monad m] [MonadError m] [MonadLiftT CoreM m]
+variable [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadOptions m]
 
 def TacticDocsOptions.parse  : ArgParse m TacticDocsOptions :=
   TacticDocsOptions.mk <$>
     .positional `name strOrName <*>
     .named `show .string true <*>
-    .namedD `replace .bool false <*>
-    .named `allowMissing .bool true
+    .flag `replace false <*>
+    .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions)
+      "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)"
 where
   strOrName : ValDesc m (StrLit ⊕ Ident) := {
     description := "First token in tactic, or canonical parser name"
diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean
index 564108607..38f087f6c 100644
--- a/src/verso-manual/VersoManual/Glossary.lean
+++ b/src/verso-manual/VersoManual/Glossary.lean
@@ -24,7 +24,7 @@ section
 variable [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m]
 
 def TechArgs.parse  : ArgParse m TechArgs :=
-  TechArgs.mk <$> .named `key .string true <*> .namedD `normalize .bool true
+  TechArgs.mk <$> .named `key .string true <*> .flag `normalize true
 
 instance : FromArgs TechArgs m := ⟨TechArgs.parse⟩
 
diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index b56a64575..83b4c98c7 100644
--- a/src/verso-manual/VersoManual/InlineLean.lean
+++ b/src/verso-manual/VersoManual/InlineLean.lean
@@ -77,14 +77,14 @@ section Config
 variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
 
 structure LeanBlockConfig where
-  «show» : Option Bool := none
-  keep : Option Bool := none
-  name : Option Name := none
-  error : Option Bool := none
-  fresh : Bool := false
+  «show» : Bool
+  keep : Bool
+  name : Option Name
+  error : Bool
+  fresh : Bool
 
 def LeanBlockConfig.parse : ArgParse m LeanBlockConfig :=
-  LeanBlockConfig.mk <$> .named `show .bool true <*> .named `keep .bool true <*> .named `name .name true <*> .named `error .bool true <*> .namedD `fresh .bool false
+  LeanBlockConfig.mk <$> .flag `show true <*> .flag `keep true <*> .named `name .name true <*> .flag `error false <*> .flag `fresh false
 
 instance : FromArgs LeanBlockConfig m := ⟨LeanBlockConfig.parse⟩
 
@@ -120,9 +120,9 @@ private def abbrevFirstLine (width : Nat) (str : String) : String :=
 def LeanBlockConfig.outlineMeta : LeanBlockConfig → String
   | {«show», error, ..} =>
     match «show», error with
-    | some true, true | none, true => " (error)"
-    | some false, true => " (hidden, error)"
-    | some false, false => " (hidden)"
+    | true, true => " (error)"
+    | false, true => " (hidden, error)"
+    | false, false => " (hidden)"
     | _, _ => " "
 
 def firstToken? (stx : Syntax) : Option Syntax :=
@@ -226,14 +226,14 @@ def lean : CodeBlockExpanderOf LeanBlockConfig
       if let some col := col? then
         hls := hls.deIndent col
 
-      if config.show.getD true then
+      if config.show then
         let range := Syntax.getRange? str
         let range := range.map (← getFileMap).utf8RangeToLspRange
         ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])
       else
         ``(Block.concat #[])
     finally
-      if !config.keep.getD true then
+      if !config.keep then
         setEnv origEnv
 
       if let some name := config.name then
@@ -247,7 +247,7 @@ def lean : CodeBlockExpanderOf LeanBlockConfig
 
       reportMessages config.error str cmdState.messages
 
-      if config.show.getD true then
+      if config.show then
         warnLongLines col? str
 where
   withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str
@@ -331,21 +331,15 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig
 
       pushInfoTree tree
 
-      match config.error with
-      | none =>
-        for msg in newMsgs.toArray do
-          logMessage msg
-      | some true =>
+      if config.error then
         if newMsgs.hasErrors then
           for msg in newMsgs.errorsToWarnings.toArray do
             logMessage msg
         else
           throwErrorAt str "Error expected in code, but none occurred"
-      | some false =>
+      else
         for msg in newMsgs.toArray do
           logMessage msg
-        if newMsgs.hasErrors then
-          throwErrorAt str "No error expected in code, one occurred"
 
       let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
       let hls :=
@@ -353,7 +347,7 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig
           hls.deIndent col
         else hls
 
-      if config.show.getD true then
+      if config.show then
         let range := Syntax.getRange? str
         let range := range.map (← getFileMap).utf8RangeToLspRange
         ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])
@@ -448,30 +442,23 @@ def leanInline : RoleExpanderOf LeanInlineConfig
         Hover.addCustomHover (mkNullNode #[s, e]) type
         Hover.addCustomHover f type
 
-      match config.error with
-      | none =>
-        for msg in newMsgs.toArray do
-          logMessage {msg with
-            isSilent := msg.isSilent || msg.severity != .error
-          }
-      | some true =>
+      if config.error then
         if newMsgs.hasErrors then
           for msg in newMsgs.errorsToWarnings.toArray do
             logMessage {msg with isSilent := true}
         else
           throwErrorAt term "Error expected in code block, but none occurred"
-      | some false =>
+      else
         for msg in newMsgs.toArray do
-          logMessage {msg with isSilent := msg.isSilent || msg.severity != .error}
-        if newMsgs.hasErrors then
-          throwErrorAt term "No error expected in code block, one occurred"
+          logMessage {msg with
+            isSilent := msg.isSilent || msg.severity != .error
+          }
 
       reportMessages config.error term newMsgs
 
       let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
 
-
-      if config.show.getD true then
+      if config.show then
         ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])
       else
         ``(Block.concat #[])
@@ -541,7 +528,7 @@ def inst : RoleExpanderOf LeanBlockConfig
 
       let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
 
-      if config.show.getD true then
+      if config.show then
         ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])
       else
         ``(Block.concat #[])
@@ -568,7 +555,7 @@ Elaborates the contained document in a new section.
 def leanSection : DirectiveExpander
   | args, contents => do
     let name? ← ArgParse.run ((some <$> .positional `name .string) <|> pure none) args
-    let arg ← `(argument| «show» := false)
+    let arg ← `(argument| -«show»)
     let code := name?.map (s!"section {·}") |>.getD "section"
     let start ← `(block|```lean $arg | $(quote code) ```)
     let code := name?.map (s!"end {·}") |>.getD "end"
@@ -620,11 +607,11 @@ variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr
 def LeanOutputConfig.parser : ArgParse m LeanOutputConfig :=
   LeanOutputConfig.mk <$>
     .positional `name output <*>
-    ((·.getD true) <$> .named `show .bool true) <*>
+    .flag `show true <*>
     .named `severity .messageSeverity true <*>
-    ((·.getD false) <$> .named `summarize .bool true) <*>
-    ((·.getD .exact) <$> .named `whitespace .whitespaceMode true) <*>
-    .namedD `normalizeMetas .bool true <*>
+    .flag `summarize false <*>
+    .namedD `whitespace .whitespaceMode .exact <*>
+    .flag `normalizeMetas true <*>
     .namedD `allowDiff .nat 0 <*>
     .many (.named `expandTrace .name false) <*>
     .named `startAt .string true <*>
diff --git a/src/verso-manual/VersoManual/InlineLean/IO.lean b/src/verso-manual/VersoManual/InlineLean/IO.lean
index c6ad1554b..e3781ef49 100644
--- a/src/verso-manual/VersoManual/InlineLean/IO.lean
+++ b/src/verso-manual/VersoManual/InlineLean/IO.lean
@@ -74,7 +74,7 @@ section
 variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
 
 def ExampleFileConfig.parse  : ArgParse m ExampleFileConfig :=
-  ExampleFileConfig.mk <$> FileType.parse <*> ((·.getD true) <$> .named `show .bool true)
+  ExampleFileConfig.mk <$> FileType.parse <*> (.flag `show true)
 
 def IOExample.exampleFileSyntax [Monad m] [MonadQuotation m] (type : FileType) (contents : String) : m Term := do
   `(Block.other (Block.exampleFile $(quote type)) #[Block.code $(quote contents)])
@@ -409,7 +409,7 @@ structure Config where
   «show» : Bool := true
 
 def Config.parse : ArgParse m Config :=
-  Config.mk <$> .named `tag .string true <*> ((·.getD true) <$> .named `show .bool true)
+  Config.mk <$> .named `tag .string true <*> (.flag `show true)
 
 instance : FromArgs Config m := ⟨Config.parse⟩
 
diff --git a/src/verso-manual/VersoManual/InlineLean/Signature.lean b/src/verso-manual/VersoManual/InlineLean/Signature.lean
index c48527dd4..6a2fd0b52 100644
--- a/src/verso-manual/VersoManual/InlineLean/Signature.lean
+++ b/src/verso-manual/VersoManual/InlineLean/Signature.lean
@@ -53,7 +53,7 @@ variable [Monad m] [MonadError m] [MonadLiftT CoreM m]
 
 def SignatureConfig.parse  : ArgParse m SignatureConfig :=
   SignatureConfig.mk <$>
-    ((·.getD true) <$> .named `show .bool true)
+    (.flag `show true)
 
 instance : FromArgs SignatureConfig m where
   fromArgs := SignatureConfig.parse
diff --git a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
index da64f3aa6..9e7d0eed2 100644
--- a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
+++ b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
@@ -126,7 +126,7 @@ variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr
 def SyntaxErrorConfig.parse : ArgParse m SyntaxErrorConfig :=
   SyntaxErrorConfig.mk <$>
     .positional `name (ValDesc.name.as "name for later reference") <*>
-    .namedD `show .bool true <*>
+    .flag `show true <*>
     .namedD `category (ValDesc.name.as "syntax category (default `command`)") `command <*>
     .namedD `precedence .nat 0
 
diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean
index 61d083c3e..ab2d9c48d 100644
--- a/src/verso-manual/VersoManual/Table.lean
+++ b/src/verso-manual/VersoManual/Table.lean
@@ -136,7 +136,7 @@ section
 variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m]
 
 def TableConfig.parse : ArgParse m TableConfig :=
-  TableConfig.mk <$> .named `tag .string true <*> ((·.getD false) <$> .named `header .bool true) <*> .named `align alignment true
+  TableConfig.mk <$> .named `tag .string true <*> .flag `header true <*> .named `align alignment true
 where
   alignment := {
     description := "Alignment of the table ('left', 'right', or 'center')"
diff --git a/src/verso/Verso/Code/External.lean b/src/verso/Verso/Code/External.lean
index 31d96d942..2a924b54d 100644
--- a/src/verso/Verso/Code/External.lean
+++ b/src/verso/Verso/Code/External.lean
@@ -127,7 +127,7 @@ structure CodeModuleContext extends CodeConfig where
   project : StrLit
 
 instance : FromArgs CodeModuleContext m where
-  fromArgs := ((·, ·, ·, ·) <$> moduleOrDefault <*> projectOrDefault <*> .namedD `showProofStates .bool true <*> .named `defSite .bool true) <&> fun (m, p, s, d) =>
+  fromArgs := ((·, ·, ·, ·) <$> moduleOrDefault <*> projectOrDefault <*> .flag `showProofStates true <*> .flag `defSite true) <&> fun (m, p, s, d) =>
     ({module := m, project := p, showProofStates := s, defSite := d})
 
 /--
diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean
index 96ac8d5c9..98f2ac9fc 100644
--- a/src/verso/Verso/Doc.lean
+++ b/src/verso/Verso/Doc.lean
@@ -340,12 +340,14 @@ open Lean in
 inductive Arg where
   | anon (value : ArgVal)
   | named (stx : Syntax) (name : Ident) (value : ArgVal)
+  | flag (stx : Syntax) (name : Ident) (value : Bool)
 deriving Repr, Inhabited, BEq
 
 open Lean in
 def Arg.syntax : Arg → Syntax
   | .anon v => v.syntax
-  | .named stx _ _ => stx
+  | .named stx .. | .flag stx .. => stx
+
 
 structure ListItem (α : Type u) where
   contents : Array α
diff --git a/src/verso/Verso/Doc/ArgParse.lean b/src/verso/Verso/Doc/ArgParse.lean
index 26fe2f196..9a388bd89 100644
--- a/src/verso/Verso/Doc/ArgParse.lean
+++ b/src/verso/Verso/Doc/ArgParse.lean
@@ -172,6 +172,14 @@ inductive ArgParse (m : Type → Type) : Type → Type 1 where
   -/
   | anyNamed (name : Name) (val : ValDesc m α) (doc? : Option SigDoc := none) : ArgParse m (Ident × α)
   /--
+  Matches a flag with the provided name.
+  -/
+  | flag (name : Name) (default : Bool) (doc? : Option SigDoc := none) : ArgParse m Bool
+  /--
+  Matches a flag with the provided name, deriving a default value from the monad
+  -/
+  | flagM (name : Name) (default : m Bool) (doc? : Option SigDoc := none) : ArgParse m Bool
+  /--
   No further arguments are allowed.
   -/
   | done : ArgParse m Unit
@@ -192,7 +200,7 @@ inductive ArgParse (m : Type → Type) : Type → Type 1 where
 
 namespace ArgParse
 section
-variable (m) [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m]
+variable (m) [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] [MonadLiftT CoreM m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
 
 /--
 A canonical way to convert a sequence of Verso arguments into a given type.
@@ -259,6 +267,7 @@ def describe : ArgParse m α → SigDoc
   | .positional _x v _ => v.description
   | .named x v opt _ => if opt then "[" else "" ++ x.toString ++ doc!" : " ++ v.description ++ if opt then "]" else ""
   | .anyNamed x v _ => s!"{x}: a named " ++ v.description
+  | .flag x .. | .flagM x .. => s!"the flag {x}"
   | .done => "no arguments remaining"
   | .orElse p1 p2 => p1.describe ++ " or " ++ (p2 ()).describe
   | .seq p1 p2 => p1.describe ++ " then " ++ (p2 ()).describe
@@ -268,6 +277,7 @@ def describe : ArgParse m α → SigDoc
 structure SimpleDesc where
   positional : Array (Name × CanMatch × SigDoc) := {}
   byName : Array (Name × CanMatch × Bool × SigDoc) := {}
+  flags : Array (Name × Option Bool × SigDoc) := {}
   keyVals : Option (Name × CanMatch × SigDoc) := none
 
 def toSimpleDesc {m} (p : ArgParse m α) : Option SimpleDesc :=
@@ -285,6 +295,10 @@ where
     if (← get).keyVals.isNone then
       modify fun sd => { sd with keyVals := some (x, v.signature, doc?.getD v.description) }
     else failure
+  | .flag x default doc? => do
+    modify fun sd => { sd with flags := sd.flags.push (x, some default, doc?.getD "Flag") }
+  | .flagM x _ doc? => do
+    modify fun sd => { sd with flags := sd.flags.push (x, none, doc?.getD "Flag") }
   | .seq p1 p2 => do
     go p1
     go (p2 ())
@@ -293,11 +307,11 @@ where
 
 
 def SimpleDesc.markdown (d : SimpleDesc) : SigDoc :=
-  let {positional, byName, keyVals} := d
-  if positional.isEmpty && byName.isEmpty && keyVals.isNone then
+  let {positional, byName, flags, keyVals} := d
+  if positional.isEmpty && byName.isEmpty && flags.isEmpty && keyVals.isNone then
     "No parameters"
   else
-    posList positional ++ nameList byName ++ kv keyVals
+    posList positional ++ nameList byName ++ flagList flags ++ kv keyVals
 where
   posList (pos : Array (Name × CanMatch × SigDoc)) : SigDoc :=
     if pos.isEmpty then ""
@@ -319,6 +333,11 @@ where
           s ++ doc!"* `" ++ x.toString ++ " : " ++ t.toString ++
             "` (" ++ (if opt then "optional" else "required") ++ ") — " ++ doc ++ "\n"
       args ++ "\n"
+  flagList (fs : Array (Name × Option Bool × SigDoc)) : SigDoc :=
+    if fs.isEmpty then ""
+    else
+      fs.foldl (init := doc!"Flag" ++ if fs.size = 1 then "" else "s" ++ ":\n") fun s (x, default, doc) =>
+        s ++ doc!"* `" ++ x.toString ++ (default.map (s!"` (default `{·}`) - ")).getD "" ++ doc ++ "\n"
   kv : Option (Name × CanMatch × SigDoc) → SigDoc
     | none => ""
     | some (x, t, doc) =>
@@ -338,6 +357,8 @@ def signature' {m} (prec : Nat) (p : ArgParse m α) : Option Std.Format :=
     let d := v.signature.format
     let s := .group <| .nest 2 <| .text s!"{x} :" ++ .line ++ d ++ .line ++ "(key/value)"
     return withParen 2 s
+  | .flag x .. | .flagM x .. => do
+    return s!"[+/-]{x}"
   | .orElse p1 p2 => do
     let s1 := p1.signature' 2
     let s2 := (p2 ()).signature' 3
@@ -382,6 +403,7 @@ instance : ToMessageData Arg where
   toMessageData
     | .anon v => toMessageData v
     | .named _ x v => m!"({x.getId} := {v})"
+    | .flag _ x v => m!"{if v then "+" else "-"}{x.getId}"
 
 structure ParseState where
   remaining : Array Arg
@@ -397,7 +419,7 @@ partial def parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (Stat
   | .fail stx? msg? => do
     let stx ← stx?.getDM getRef
     let msg := msg?.getD "failed"
-    throw ((← get).remaining, .error stx msg.toMessageData)
+    throwThe (Array Arg × Exception) ((← get).remaining, Lean.Exception.error stx msg.toMessageData)
   | .pure x => Pure.pure x
   | .lift desc act => act
   | .positional x vp doc? => do
@@ -420,8 +442,8 @@ partial def parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (Stat
         else
           modify fun s => {s with info := s.info.push (v.syntax, x, vp.description)}
         Pure.pure val
-      | .error e => throw e
-    else throw ((← get).remaining, .error (← getRef) m!"Positional argument '{x}' ({vp.description}) not found")
+      | .error e => throwThe (Array Arg × Exception) e
+    else throwThe (Array Arg × Exception) ((← get).remaining, .error (← getRef) m!"Positional argument '{x}' ({vp.description}) not found")
   | .named x vp optional doc? => do
     let initArgs := (← get).remaining
     if let some (stx, n, v, args') := getNamed initArgs x then
@@ -441,16 +463,18 @@ partial def parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (Stat
         Pure.pure <| match optional with
           | true => some val
           | false => val
-      | .error e => throw e
+      | .error e => throwThe (Array Arg × Exception) e
     else match optional with
       | true => Pure.pure none
-      | false => throw ((← get).remaining, .error (← getRef) m!"Named argument '{x}' ({vp.description}) not found")
+      | false => throwThe (Array Arg × Exception) ((← get).remaining, .error (← getRef) m!"Named argument '{x}' ({vp.description}) not found")
   | .anyNamed x vp doc? => do
     let initArgs := (← get).remaining
     if h : initArgs.size > 0 then
       match initArgs[0] with
       | .anon _ =>
-        throw ((← get).remaining, .error (← getRef) m!"Name-argument pair '{x}' ({vp.description}) expected, got anonymous argument")
+        throwThe (Array Arg × Exception) ((← get).remaining, .error (← getRef) m!"Name-argument pair '{x}' ({vp.description}) expected, got anonymous argument")
+      | .flag _ x v =>
+        throwThe (Array Arg × Exception) ((← get).remaining, .error (← getRef) m!"Name-argument pair '{x}' ({vp.description}) expected, got flag `{if v then "+" else "-"}{x.getId}`")
       | .named stx y v =>
         let val? : Except (Array Arg × Exception) _ ← liftM <|
           try
@@ -464,35 +488,103 @@ partial def parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (Stat
             modify fun s => {s with info := s.info.push (stx, x, vp.description)}
           modify fun s => {s with remaining := initArgs.extract 1 initArgs.size}
           Pure.pure (y, val)
-        | .error e => throw e
-    else throw ((← get).remaining, .error (← getRef) m!"Name-argument pair '{x}' ({vp.description}) not found")
+        | .error e => throwThe (Array Arg × Exception) e
+    else throwThe (Array Arg × Exception) ((← get).remaining, .error (← getRef) m!"Name-argument pair '{x}' ({vp.description}) not found")
+  | .flag x default doc? => do
+    let initArgs := (← get).remaining
+    if let some (stx, n, v, args') := getFlag initArgs x then
+      -- This is needed to apply hovers correctly when a macro expands a positional argument into a named one
+      let pos := firstOriginal #[stx, n]
+      modify fun s => {s with remaining := args'}
+      if let some d := doc? then
+        modify fun s => {s with info := s.info.push (pos, x, d)}
+      else
+        modify fun s => {s with info := s.info.push (pos, x, "Flag")}
+      pure v
+    else if let some (stx, n, v, args') := getNamed initArgs x then
+      let val? : Except (Array Arg × Exception) _ ← liftM <|
+        try
+          Except.ok <$> withRef v.syntax (do
+            match v with
+            | .name x =>
+              let x' ← realizeGlobalConstNoOverloadWithInfo x
+              if x' == ``true then pure true else if x' == ``false then pure false else throwError "Expected Boolean"
+            | _ => throwError "Expected Boolean")
+        catch exn => Pure.pure <| Except.error (initArgs, exn)
+      -- This is needed to apply hovers correctly when a macro expands a positional argument into a named one
+      let pos := firstOriginal #[stx, n, v.syntax]
+      match val? with
+      | .ok val =>
+        modify fun s => {s with remaining := args'}
+        if let some d := doc? then
+          modify fun s => {s with info := s.info.push (pos, x, d)}
+        else
+          modify fun s => {s with info := s.info.push (pos, x, "Flag")}
+        if let some (.original ..) := stx.getInfo? then
+          let hint ← MessageData.hint m!"Replace with the updated syntax:" #[s!"{if val then "+" else "-"}{x.toString}"] (ref? := some stx)
+          logWarningAt stx m!"Deprecated flag syntax.{hint}"
+        Pure.pure val
+      | .error e => throwThe (Array Arg × Exception) e
+    else
+      pure default
+  | .flagM x default doc? => do
+    let initArgs := (← get).remaining
+    if let some (stx, n, v, args') := getFlag initArgs x then
+      -- This is needed to apply hovers correctly when a macro expands a positional argument into a named one
+      let pos := firstOriginal #[stx, n]
+      modify fun s => {s with remaining := args'}
+      if let some d := doc? then
+        modify fun s => {s with info := s.info.push (pos, x, d)}
+      else
+        modify fun s => {s with info := s.info.push (pos, x, "Flag")}
+      pure v
+    else if let some (stx, n, v, args') := getNamed initArgs x then
+      let val? : Except (Array Arg × Exception) _ ← liftM <|
+        try
+          Except.ok <$> withRef v.syntax (do
+            match v with
+            | .name x =>
+              let x' ← realizeGlobalConstNoOverloadWithInfo x
+              if x' == ``true then pure true else if x' == ``false then pure false else throwError "Expected Boolean"
+            | _ => throwError "Expected Boolean")
+        catch exn => Pure.pure <| Except.error (initArgs, exn)
+      -- This is needed to apply hovers correctly when a macro expands a positional argument into a named one
+      let pos := firstOriginal #[stx, n, v.syntax]
+      match val? with
+      | .ok val =>
+        modify fun s => {s with remaining := args'}
+        if let some d := doc? then
+          modify fun s => {s with info := s.info.push (pos, x, d)}
+        else
+          modify fun s => {s with info := s.info.push (pos, x, "Flag")}
+        if let some (.original ..) := stx.getInfo? then
+          let hint ← MessageData.hint m!"Replace with the updated syntax:" #[s!"{if val then "+" else "-"}{x.toString}"] (ref? := some stx)
+          logWarningAt stx m!"Deprecated flag syntax.{hint}"
+        Pure.pure val
+      | .error e => throwThe (Array Arg × Exception) e
+    else
+      default
   | .done => do
     let args := (← get).remaining
     if h : args.size > 0 then
       match args[0] with
-      | .anon v => throw (args, .error v.syntax m!"Unexpected argument {v}")
-      | .named stx x _ => throw (args, .error stx m!"Unexpected named argument '{x.getId}'")
+      | .anon v => throwThe (Array Arg × Exception) (args, .error v.syntax m!"Unexpected argument {v}")
+      | .flag stx x v => throwThe (Array Arg × Exception) (args, .error stx m!"Unexpected flag {if v then "+" else "-"}{x.getId}")
+      | .named stx x _ => throwThe (Array Arg × Exception) (args, .error stx m!"Unexpected named argument '{x.getId}'")
     else Pure.pure ()
   | .orElse p1 p2 => do
     let s ← get
-    try
-      p1.parseArgs
-    catch
-      | e1@(args1, _) =>
-        try
-          set s
-          (p2 ()).parseArgs
-        catch
+    tryCatchThe (Array Arg × Exception) p1.parseArgs fun
+      | e1@((args1 : Array Arg), _) =>
+        tryCatchThe (Array Arg × Exception) (set s *> (p2 ()).parseArgs) fun
           | e2@(args2, _) =>
-            if args2.size < args1.size then throw e1 else throw e2
+            if args2.size < args1.size then throwThe (Array Arg × Exception) e1 else throwThe (Array Arg × Exception) e2
   | .seq p1 p2 => Seq.seq p1.parseArgs (fun () => p2 () |>.parseArgs)
   | .many p => do
-    let x ←
-      try
-        p.parseArgs
-      catch | _ => return []
-    let xs ← ArgParse.many p |>.parseArgs
-    return (x :: xs)
+    if let some x ← tryCatchThe (Array Arg × Exception) (some <$> p.parseArgs) fun _ => pure none then
+      let xs ← ArgParse.many p |>.parseArgs
+      return (x :: xs)
+    else return []
   | .remaining => modifyGet fun s =>
     let r := s.remaining
     (r, {s with remaining := #[]})
@@ -502,6 +594,11 @@ where
       if let .named stx y v := args[i] then
         if y.getId.eraseMacroScopes == x then return some (stx, y, v, args.extract 0 i ++ args.extract (i+1) args.size)
     return none
+  getFlag (args : Array Arg) (x : Name) : Option (Syntax × Ident × Bool × Array Arg) := Id.run do
+    for h : i in [0:args.size] do
+      if let .flag stx y v := args[i] then
+        if y.getId.eraseMacroScopes == x then return some (stx, y, v, args.extract 0 i ++ args.extract (i+1) args.size)
+    return none
   getPositional (args : Array Arg) : Option (ArgVal × Array Arg) := Id.run do
     for h : i in [0:args.size] do
       if let .anon v := args[i] then
@@ -526,6 +623,7 @@ def ValDesc.bool : ValDesc m Bool where
 instance : FromArgVal Bool m where
   fromArgVal := .bool
 
+
 def ValDesc.string : ValDesc m String where
   description := doc!"a string"
   signature := .String
@@ -682,7 +780,9 @@ def ValDesc.strLit [Monad m] [MonadError m] : ValDesc m StrLit where
 instance : FromArgVal StrLit m where
   fromArgVal := .strLit
 
-def run [MonadLiftT BaseIO m] (p : ArgParse m α) (args : Array Arg) : m α := do
+variable [MonadLiftT BaseIO m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
+
+def run (p : ArgParse m α) (args : Array Arg) : m α := do
   match ← p.parseArgs _ ⟨args, #[]⟩ with
   | (.ok v, ⟨more, info⟩) =>
     if more.size = 0 then
@@ -698,8 +798,8 @@ def run [MonadLiftT BaseIO m] (p : ArgParse m α) (args : Array Arg) : m α := d
   | (.error e, st) =>
     throw e.snd
 
-def parse [MonadLiftT BaseIO m] [FromArgs α m] (args : Array Arg) : m α := do
+def parse [FromArgs α m] (args : Array Arg) : m α := do
   ArgParse.run fromArgs args
 
-def parseThe (α) [MonadLiftT BaseIO m] [FromArgs α m] (args : Array Arg) : m α := do
+def parseThe (α) [FromArgs α m] (args : Array Arg) : m α := do
   ArgParse.run fromArgs args
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index c21673098..5d9f98f2e 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -91,8 +91,19 @@ def parseArgs (argStx : TSyntaxArray `argument) : DocElabM (Array Arg) := do
     match arg with
     | `(argument|$v:arg_val) =>
       argVals := argVals.push (.anon (← parseArgVal v))
-    | `(argument|$x:ident := $v) =>
+    | `(argument|$x:ident := $v) => do
+      let src := (← getFileMap).source
+      if let some ⟨s, e⟩ := x.raw.getRange? (canonicalOnly := true) then
+        if let some ⟨s', e'⟩ := v.raw.getRange? (canonicalOnly := true) then
+          let hint ← MessageData.hint m!"Replace with the updated syntax:" #[s!"({src.extract s e} := {src.extract s' e'})"] (ref? := some arg)
+          logWarningAt arg m!"Deprecated named argument syntax for `{x}`{hint}"
       argVals := argVals.push (.named arg x (← parseArgVal v))
+    | `(argument|($x:ident := $v)) =>
+      argVals := argVals.push (.named arg x (← parseArgVal v))
+    | `(argument|+$x) =>
+      argVals := argVals.push (.flag arg x true)
+    | `(argument|-$x) =>
+      argVals := argVals.push (.flag arg x false)
     | other => throwErrorAt other "Can't decode argument '{repr other}'"
   pure argVals
 
@@ -111,6 +122,7 @@ def appFallback
   let argStx : Array Syntax ← argVals.mapM fun
     | .anon v => valStx v
     | .named _orig y v => do `(namedArgument|($y := $(← valStx v))) -- TODO location
+    | .flag _orig y v => `(namedArgument|($y := $(quote v))) -- TODO location
   let subs ← subjectArr.mapM (·.mapM elabInline)
   let arrArg ← match subs with
     | some ss => (#[·]) <$> `(#[$ss,*])
diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean
index 12f8aeaa5..2474978a1 100644
--- a/src/verso/Verso/Parser.lean
+++ b/src/verso/Verso/Parser.lean
@@ -757,6 +757,13 @@ def recoverWs (p : ParserFn) : ParserFn :=
   recoverFn p fun _ =>
     ignoreFn <| takeUntilFn (fun c =>  c == ' ' || c == '\n')
 
+def recoverNonSpace (p : ParserFn) : ParserFn :=
+  recoverFn p fun rctx =>
+    ignoreFn (takeUntilFn (fun c => c != ' ')) >>
+    show ParserFn from
+      fun _ s => s.shrinkStack rctx.initialSize
+
+
 /--
 info: Failure @4 (⟨1, 4⟩): unterminated string literal; expected identifier or numeral
 Final stack:
@@ -803,20 +810,31 @@ def recoverHereWithKeeping (stxs : Array Syntax) (keep : Nat) (p : ParserFn) : P
 
 def arg : ParserFn :=
     withCurrentStackSize fun iniSz =>
-      withParens iniSz <|> potentiallyNamed iniSz <|> (val >> mkAnon iniSz)
+      flag <|> withParens iniSz <|> potentiallyNamed iniSz <|> (val >> mkAnon iniSz)
 where
   mkNamed (iniSz : Nat) : ParserFn := fun _ s => s.mkNode ``Verso.Syntax.named iniSz
+  mkNamedNoParen (iniSz : Nat) : ParserFn := fun _ s => s.mkNode ``Verso.Syntax.named_no_paren iniSz
   mkAnon (iniSz : Nat) : ParserFn := fun _ s => s.mkNode ``Verso.Syntax.anon iniSz
   mkIdent (iniSz : Nat) : ParserFn := fun _ s => s.mkNode ``Verso.Syntax.arg_ident iniSz
+  flag : ParserFn :=
+    nodeFn ``Verso.Syntax.flag_on (asStringFn (strFn  "+") >> recoverNonSpace noSpace >> recoverWs (docIdentFn (reportAs := "flag name"))) <|>
+    nodeFn ``Verso.Syntax.flag_off (asStringFn (strFn "-") >> recoverNonSpace noSpace >> recoverWs (docIdentFn (reportAs := "flag name")))
+  noSpace : ParserFn := fun c s =>
+    if h : c.input.atEnd s.pos then s
+    else
+      let ch := c.input.get' s.pos h
+      if ch == ' ' then
+        s.mkError "no space before"
+      else s
   potentiallyNamed iniSz :=
       atomicFn docIdentFn >> eatSpaces >>
-       ((atomicFn (strFn ":=") >> eatSpaces >> val >> eatSpaces >> mkNamed iniSz) <|> (mkIdent iniSz >> mkAnon iniSz))
+       ((atomicFn (asStringFn <| strFn ":=") >> eatSpaces >> val >> eatSpaces >> mkNamedNoParen iniSz) <|> (mkIdent iniSz >> mkAnon iniSz))
   withParens iniSz :=
-    atomicFn (ignoreFn (strFn "(")) >> eatSpaces >>
+    atomicFn (asStringFn <| strFn "(") >> eatSpaces >>
     recoverWs (docIdentFn (reportAs := "argument name"))  >> eatSpaces >>
-    recoverWs (strFn ":=") >> eatSpaces >>
+    recoverWs (asStringFn <| strFn ":=") >> eatSpaces >>
     recoverWs val >> eatSpaces >>
-    recoverEol (ignoreFn (strFn ")")) >> eatSpaces >>
+    recoverEol (asStringFn <| strFn ")") >> eatSpaces >>
     mkNamed iniSz
 
 /--
@@ -830,7 +848,7 @@ All input consumed.
 
 /--
 info: Success! Final stack:
-  (Verso.Syntax.named
+  (Verso.Syntax.named_no_paren
    `x
    ":="
    (Verso.Syntax.arg_num (num "1")))
@@ -842,9 +860,11 @@ All input consumed.
 /--
 info: Success! Final stack:
   (Verso.Syntax.named
+   "("
    `x
    ":="
-   (Verso.Syntax.arg_num (num "1")))
+   (Verso.Syntax.arg_num (num "1"))
+   ")")
 All input consumed.
 -/
 #guard_msgs in
@@ -852,7 +872,7 @@ All input consumed.
 
 /--
 info: Failure @0 (⟨1, 0⟩): '
-'; expected '(', identifier or numeral
+'; expected '(', '+', '-', identifier or numeral
 Final stack:
   (Verso.Syntax.arg_str <missing>)
 Remaining: "\n(x:=1)"
@@ -860,12 +880,39 @@ Remaining: "\n(x:=1)"
 #guard_msgs in
 #eval arg.test! "\n(x:=1)"
 
+/--
+info: Success! Final stack:
+  (Verso.Syntax.flag_on "+" `foo)
+All input consumed.
+-/
+#guard_msgs in
+#eval arg.test! "+foo"
+
+/--
+info: Success! Final stack:
+  (Verso.Syntax.flag_off "-" `other)
+All input consumed.
+-/
+#guard_msgs in
+#eval arg.test! "-other"
+
+/--
+info: Failure @2 (⟨1, 2⟩): expected no space before
+Final stack:
+  (Verso.Syntax.flag_off "-" `other)
+Remaining: "other"
+-/
+#guard_msgs in
+#eval arg.test! "- other"
+
 /--
 info: Success! Final stack:
   (Verso.Syntax.named
+   "("
    `x
    ":="
-   (Verso.Syntax.arg_num (num "1")))
+   (Verso.Syntax.arg_num (num "1"))
+   ")")
 Remaining:
 "\n"
 -/
@@ -874,7 +921,7 @@ Remaining:
 
 /--
 info: Success! Final stack:
-  (Verso.Syntax.named
+  (Verso.Syntax.named_no_paren
    `x
    ":="
    (Verso.Syntax.arg_ident `y))
@@ -886,9 +933,11 @@ All input consumed.
 /--
 info: Success! Final stack:
   (Verso.Syntax.named
+   "("
    `x
    ":="
-   (Verso.Syntax.arg_ident `y))
+   (Verso.Syntax.arg_ident `y)
+   ")")
 All input consumed.
 -/
 #guard_msgs in
@@ -896,7 +945,7 @@ All input consumed.
 
 /--
 info: Success! Final stack:
-  (Verso.Syntax.named
+  (Verso.Syntax.named_no_paren
    `x
    ":="
    (Verso.Syntax.arg_str (str "\"y\"")))
@@ -926,9 +975,11 @@ info: 2 failures:
 
 Final stack:
   (Verso.Syntax.named
+   "("
    `x
    ":="
-   (Verso.Syntax.arg_str <missing>))
+   (Verso.Syntax.arg_str <missing>)
+   <missing>)
 -/
 #guard_msgs in
 #eval arg.test! "(x:=\"y)"
@@ -956,9 +1007,11 @@ info: 4 failures:
 
 Final stack:
   (Verso.Syntax.named
+   "("
    <missing>
    <missing>
-   (Verso.Syntax.arg_str <missing>))
+   (Verso.Syntax.arg_str <missing>)
+   <missing>)
 -/
 #guard_msgs in
 #eval arg.test! "(42)"
@@ -974,9 +1027,11 @@ info: 3 failures:
 
 Final stack:
   (Verso.Syntax.named
+   "("
    `x
    <missing>
-   (Verso.Syntax.arg_str <missing>))
+   (Verso.Syntax.arg_str <missing>)
+   <missing>)
 -/
 #guard_msgs in
 #eval arg.test! "(x 42)"
@@ -985,9 +1040,11 @@ Final stack:
 info: Failure @8 (⟨1, 8⟩): expected ')'
 Final stack:
   (Verso.Syntax.named
+   "("
    `x
    ":="
-   (Verso.Syntax.arg_num (num "42")))
+   (Verso.Syntax.arg_num (num "42"))
+   <missing>)
 Remaining: "\n)"
 -/
 #guard_msgs in
@@ -997,9 +1054,11 @@ Remaining: "\n)"
 info: Failure @8 (⟨1, 8⟩): expected ')'
 Final stack:
   (Verso.Syntax.named
+   "("
    `x
    ":="
-   (Verso.Syntax.arg_num (num "42")))
+   (Verso.Syntax.arg_num (num "42"))
+   <missing>)
 Remaining: "\na"
 -/
 #guard_msgs in
@@ -1046,7 +1105,7 @@ def nameAndArgs (multiline : Option Nat := none) (reportNameAs : String := "iden
 /--
 info: Success! Final stack:
  • `leanExample
- • [(Verso.Syntax.named
+ • [(Verso.Syntax.named_no_paren
       `context
       ":="
       (Verso.Syntax.arg_num (num "2")))]
@@ -1059,7 +1118,7 @@ All input consumed.
 /--
 info: Success! Final stack:
  • `scheme
- • [(Verso.Syntax.named
+ • [(Verso.Syntax.named_no_paren
       `dialect
       ":="
       (Verso.Syntax.arg_str (str "\"chicken\"")))
@@ -1071,6 +1130,56 @@ All input consumed.
 #guard_msgs in
 #eval nameAndArgs.test! "scheme dialect:=\"chicken\" 43"
 
+/--
+info: Success! Final stack:
+ • `scheme
+ • [(Verso.Syntax.named_no_paren
+      `dialect
+      ":="
+      (Verso.Syntax.arg_str (str "\"chicken\"")))
+     (Verso.Syntax.anon
+      (Verso.Syntax.arg_num (num "43")))
+     (Verso.Syntax.flag_on "+" `foo)]
+
+All input consumed.
+-/
+#guard_msgs in
+#eval nameAndArgs.test! "scheme dialect:=\"chicken\" 43 +foo"
+
+/--
+info: Failure @29 (⟨1, 29⟩): expected flag name
+Final stack:
+ • `scheme
+ • [(Verso.Syntax.named_no_paren
+      `dialect
+      ":="
+      (Verso.Syntax.arg_str (str "\"chicken\"")))
+     (Verso.Syntax.flag_on "+" <missing>)
+     (Verso.Syntax.anon
+      (Verso.Syntax.arg_num (num "99")))]
+
+Remaining: " 99"
+-/
+#guard_msgs in
+#eval nameAndArgs.test! "scheme dialect:=\"chicken\" +43 99"
+
+
+/--
+info: Failure @28 (⟨1, 28⟩): expected no space before
+Final stack:
+ • `scheme
+ • [(Verso.Syntax.named_no_paren
+      `dialect
+      ":="
+      (Verso.Syntax.arg_str (str "\"chicken\"")))
+     (Verso.Syntax.flag_on "+" `x)
+     (Verso.Syntax.anon
+      (Verso.Syntax.arg_num (num "99")))]
+
+Remaining: "x 99"
+-/
+#guard_msgs in
+#eval nameAndArgs.test! "scheme dialect:=\"chicken\" + x 99"
 
 /--
 info: Success! Final stack:
@@ -1084,7 +1193,7 @@ Remaining:
 
 /--
 info: Success! Final stack:
-  [(Verso.Syntax.named
+  [(Verso.Syntax.named_no_paren
     `dialect
     ":="
     (Verso.Syntax.arg_str (str "\"chicken\"")))
@@ -1098,7 +1207,7 @@ Remaining:
 
 /--
 info: Success! Final stack:
-  [(Verso.Syntax.named
+  [(Verso.Syntax.named_no_paren
     `dialect
     ":="
     (Verso.Syntax.arg_str (str "\"chicken\"")))
@@ -1113,7 +1222,7 @@ Remaining:
 /--
 info: Success! Final stack:
  • `scheme
- • [(Verso.Syntax.named
+ • [(Verso.Syntax.named_no_paren
       `dialect
       ":="
       (Verso.Syntax.arg_str (str "\"chicken\"")))
@@ -1153,7 +1262,7 @@ info: Success! Final stack:
  • `leanExample
  • [(Verso.Syntax.anon
       (Verso.Syntax.arg_ident `context))
-     (Verso.Syntax.named
+     (Verso.Syntax.named_no_paren
       `more
       ":="
       (Verso.Syntax.arg_str (str "\"stuff\"")))]
@@ -1169,7 +1278,7 @@ info: Success! Final stack:
  • `leanExample
  • [(Verso.Syntax.anon
       (Verso.Syntax.arg_ident `context))
-     (Verso.Syntax.named
+     (Verso.Syntax.named_no_paren
       `more
       ":="
       (Verso.Syntax.arg_str (str "\"stuff\"")))]
@@ -1836,7 +1945,7 @@ info: Success! Final stack:
   (Verso.Syntax.role
    "{"
    `hello
-   [(Verso.Syntax.named
+   [(Verso.Syntax.named_no_paren
      `world
      ":="
      (Verso.Syntax.arg_ident `gaia))]
@@ -1854,7 +1963,7 @@ info: Success! Final stack:
   (Verso.Syntax.role
    "{"
    `hello
-   [(Verso.Syntax.named
+   [(Verso.Syntax.named_no_paren
      `world
      ":="
      (Verso.Syntax.arg_ident `gaia))]
@@ -3874,7 +3983,7 @@ info: Success! Final stack:
   (Verso.Syntax.codeblock
    "```"
    [`scheme
-    [(Verso.Syntax.named
+    [(Verso.Syntax.named_no_paren
       `dialect
       ":="
       (Verso.Syntax.arg_str (str "\"chicken\"")))
@@ -3898,10 +4007,11 @@ info: Success! Final stack:
    "```"
    [`scheme
     [(Verso.Syntax.named
+      "("
       `dialect
       ":="
-      (Verso.Syntax.arg_str
-       (str "\"chicken\"")))]]
+      (Verso.Syntax.arg_str (str "\"chicken\""))
+      ")")]]
    "\n"
    (str "\"(define x 4)\\nx\\n\"")
    "```")
@@ -3921,10 +4031,11 @@ Final stack:
    "```"
    [`scheme
     [(Verso.Syntax.named
+      "("
       `dialect
       ":="
-      (Verso.Syntax.arg_str
-       (str "\"chicken\"")))]]
+      (Verso.Syntax.arg_str (str "\"chicken\""))
+      <missing>)]]
    "\n"
    (str "\"(define x 4)\\nx\\n\"")
    "```")
@@ -4398,7 +4509,7 @@ info: Success! Final stack:
   (Verso.Syntax.directive
    ":::"
    `multiPara
-   [(Verso.Syntax.named
+   [(Verso.Syntax.named_no_paren
      `greatness
      ":="
      (Verso.Syntax.arg_str (str "\"amazing!\"")))]
@@ -4939,7 +5050,7 @@ info: [Error pretty printing syntax: format: uncaught backtrack exception. Falli
 /--
 info: lean
 ---
-info: hasArg:=true
+info: (hasArg := true)
 ---
 info: "Code\n"
 -/
diff --git a/src/verso/Verso/Syntax.lean b/src/verso/Verso/Syntax.lean
index 3f3792e8a..a41b526b0 100644
--- a/src/verso/Verso/Syntax.lean
+++ b/src/verso/Verso/Syntax.lean
@@ -58,7 +58,11 @@ declare_syntax_cat argument
 /-- Anonymous positional arguments -/
 syntax (name:=anon) arg_val : argument
 /-- Named arguments -/
-syntax (name:=named) ident ":=" arg_val : argument
+syntax (name:=named) "(" ident " := " arg_val ")": argument
+syntax (name:=named_no_paren) ident " := " arg_val : argument
+/-- Boolean flags -/
+syntax (name:=flag_on) "+" ident : argument
+syntax (name:=flag_off) "-" ident : argument
 
 /-- Link targets, which may be URLs or named references -/
 declare_syntax_cat link_target