feat: improve argument syntax

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.

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
 %%%

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 :=

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.
 

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

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.
 

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

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) (· + ·)
 

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))
 ```

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 [])

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"