chore: regularize syntax and improve Verso.Syntax docs

doc/UsersGuide/Markup.lean

@@ -11,10 +11,10 @@ partial def preview [Monad m] [MonadError m] (stx : Syntax) : m String :=
   match stx with
   | `(inline| $s:str) => pure s.getString
   | `(inline| line! $s:str) => pure s.getString
-  | `(inline| _{ $s:inline* }) => do
+  | `(inline| _[ $s:inline* ]) => do
     let contents ← s.toList.mapM (preview ∘ TSyntax.raw)
     pure <| "<emph>" ++ String.join contents ++ "</emph>"
-  | `(inline| *{ $s:inline* }) => do
+  | `(inline| *[ $s:inline* ]) => do
     let contents ← s.toList.mapM (preview ∘ TSyntax.raw)
     pure <| "<bold>" ++ String.join contents ++ "</bold>"
   | `(inline| link[ $txt:inline* ]( $url:str )) => do
@@ -23,9 +23,9 @@ partial def preview [Monad m] [MonadError m] (stx : Syntax) : m String :=
   | `(inline| link[ $txt:inline* ][ $tgt:str ]) => do
     let contents ← txt.toList.mapM (preview ∘ TSyntax.raw)
     pure s!"<a href=\"(value of «{tgt.getString}»)\">{String.join contents}</a>"
-  | `(inline| code{ $code:str }) =>
+  | `(inline| code( $code:str )) =>
     pure s!"<code>{code.getString}</code>"
-  | `(block| para{ $i:inline* }) => do
+  | `(block| para[ $i:inline* ]) => do
     let contents ← i.toList.mapM (preview ∘ TSyntax.raw)
     pure <| String.join contents
   | `(block| [ $ref:str ]: $url:str) =>

src/verso-blog/VersoBlog.lean

@@ -279,7 +279,7 @@ def leanCommand : BlockRoleExpander
 def leanKw : RoleExpander
   | args, #[arg] => do
     ArgParse.run .done args
-    let `(inline|code{ $kw:str }) := arg
+    let `(inline|code( $kw:str )) := arg
       | throwErrorAt arg "Expected code literal with the keyword"
     let hl : SubVerso.Highlighting.Highlighted := .token ⟨.keyword none none none, kw.getString⟩
     pure #[← ``(Inline.other (Blog.InlineExt.customHighlight $(quote hl)) #[Inline.code $(quote kw.getString)])]
@@ -293,7 +293,7 @@ def leanKw : RoleExpander
 def leanTerm : RoleExpander
   | args, #[arg] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanTerm") <| do
     let project ← ArgParse.run (.positional `project .ident) args
-    let `(inline|code{ $name:str }) := arg
+    let `(inline|code( $name:str )) := arg
       | throwErrorAt arg "Expected code literal with the example name"
     let exampleName := name.getString.toName
     let projectExamples ← getSubproject project

src/verso-manual/VersoManual/Docstring.lean

@@ -969,7 +969,7 @@ def tacticInline : RoleExpander
     let {«show»} ← TacticInlineOptions.parse.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code{ $tac:str }) := arg
+    let `(inline|code( $tac:str )) := arg
       | throwErrorAt arg "Expected code literal with the tactic name"
     let tacTok := tac.getString
     let tacName := tac.getString.toName

src/verso/Verso/Doc/Elab.lean

@@ -59,13 +59,13 @@ def _root_.linebreak.expand : InlineExpander
 
 @[inline_expander Verso.Syntax.emph]
 def _root_.Verso.Syntax.emph.expand : InlineExpander
-  | `(inline| _{ $args* }) => do
+  | `(inline| _[ $args* ]) => do
     ``(Inline.emph #[$[$(← args.mapM elabInline)],*])
   | _ => throwUnsupportedSyntax
 
 @[inline_expander Verso.Syntax.bold]
 def _root_.Verso.Syntax.bold.expand : InlineExpander
-  | `(inline| *{ $args* }) => do
+  | `(inline| *[ $args* ]) => do
     ``(Inline.bold #[$[$(← args.mapM elabInline)],*])
   | _ => throwUnsupportedSyntax
 
@@ -153,15 +153,15 @@ def _root_.Verso.Syntax.link.expand : InlineExpander
 
 @[inline_expander Verso.Syntax.footnote]
 def _root_.Verso.Syntax.link.footnote : InlineExpander
-  | `(inline| [^ $name:str ]) => do
+  | `(inline| footnote( $name:str )) => do
     ``(Inline.footnote $name $(← addFootnoteRef name))
   | _ => throwUnsupportedSyntax
 
 
 @[inline_expander Verso.Syntax.image]
 def _root_.Verso.Syntax.image.expand : InlineExpander
-  | `(inline| image[ $alt:str* ] $dest:link_target) => do
-    let altText := String.join (alt.map (·.getString) |>.toList)
+  | `(inline| image( $alt:str ) $dest:link_target) => do
+    let altText := alt.getString
     let url : TSyntax `term ←
       match dest with
       | `(link_target| ( $url )) =>
@@ -176,20 +176,20 @@ def _root_.Verso.Syntax.image.expand : InlineExpander
 
 @[inline_expander Verso.Syntax.code]
 def _root_.Verso.Syntax.code.expand : InlineExpander
-  |  `(inline| code{ $s }) =>
+  |  `(inline| code( $s )) =>
     ``(Inline.code $s)
   | _ => throwUnsupportedSyntax
 
 
 @[inline_expander Verso.Syntax.inline_math]
 def _root_.Verso.Syntax.inline_math.expand : InlineExpander
-  |  `(inline| ${ code{ $s } }) =>
+  |  `(inline| \math code( $s )) =>
     ``(Inline.math MathMode.inline $s)
   | _ => throwUnsupportedSyntax
 
 @[inline_expander Verso.Syntax.display_math]
 def _root_.Verso.Syntax.display_math.expand : InlineExpander
-  |  `(inline| $${ code{ $s } }) =>
+  |  `(inline| \displaymath code( $s )) =>
     ``(Inline.math MathMode.display $s)
   | _ => throwUnsupportedSyntax
 
@@ -356,7 +356,7 @@ def _root_.Verso.Syntax.block_role.expand : BlockExpander := fun block =>
 
 @[block_expander Verso.Syntax.para]
 partial def _root_.Verso.Syntax.para.expand : BlockExpander
-  | `(block| para{ $args:inline* }) => do
+  | `(block| para[ $args:inline* ]) => do
     ``(Block.para #[$[$(← args.mapM elabInline)],*])
   | _ =>
     throwUnsupportedSyntax
@@ -390,7 +390,7 @@ def _root_.Verso.Syntax.ul.expand : BlockExpander
 
 @[block_expander Verso.Syntax.ol]
 def _root_.Verso.Syntax.ol.expand : BlockExpander
-  | `(block|ol{ $start:num $itemStxs*}) => do
+  | `(block|ol($start:num){$itemStxs*}) => do
     let mut bullets : Array Syntax := #[]
     let mut items : Array (TSyntax `term) := #[]
     for i in itemStxs do
@@ -432,7 +432,7 @@ def _root_.Verso.Syntax.dl.expand : BlockExpander
 
 @[block_expander Verso.Syntax.blockquote]
 def _root_.Verso.Syntax.blockquote.expand : BlockExpander
-  | `(block|blockquote{$innerBlocks*}) => do
+  | `(block|> $innerBlocks*) => do
     ``(Block.blockquote #[$[$(← innerBlocks.mapM elabBlock)],*])
   | _ =>
     throwUnsupportedSyntax
@@ -463,7 +463,7 @@ def _root_.Verso.Syntax.codeblock.expand : BlockExpander
 
 @[block_expander Verso.Syntax.directive]
 def _root_.Verso.Syntax.directive.expand : BlockExpander
-  | `(block|directive{$nameStx $argsStx*}[$contents*]) => do
+  | `(block| ::: $nameStx:ident $argsStx* { $contents:block* } ) => do
     let name ← realizeGlobalConstNoOverloadWithInfo nameStx
     let exp ← directiveExpandersFor name
     let args ← parseArgs argsStx

src/verso/Verso/Doc/Elab/Monad.lean

@@ -37,19 +37,19 @@ def _root_.Verso.Syntax.linebreak.inline_to_string : InlineToString
 
 @[inline_to_string Verso.Syntax.emph]
 def _root_.Verso.Syntax.emph.inline_to_string : InlineToString
-  | env, `(inline| _{ $args* }) =>
+  | env, `(inline| _[ $args* ]) =>
     some <| String.intercalate " " (Array.map (inlineToString env) args).toList
   | _, _ => none
 
 @[inline_to_string Verso.Syntax.bold]
 def _root_.Verso.Syntax.bold.inline_to_string : InlineToString
-  | env, `(inline| *{ $args* }) =>
+  | env, `(inline| *[ $args* ]) =>
     some <| String.intercalate " " (Array.map (inlineToString env) args).toList
   | _, _ => none
 
 @[inline_to_string Verso.Syntax.code]
 def _root_.Verso.Syntax.code.inline_to_string : InlineToString
-  | _, `(inline| code{ $str }) =>
+  | _, `(inline| code( $str )) =>
     some str.getString
   | _, _ => none
 
@@ -184,7 +184,7 @@ partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m] [MonadEnv m]
     -- Adding type annotations works around a limitation in list and array elaboration, where intermediate
     -- let bindings introduced by "chunking" the elaboration may fail to infer types
     let typedBlocks ← blocks.mapM fun b => `(($b : Block $genre))
-    let body ← ``(Part.mk #[$[$titleInlines],*] $(quote titleString) $metaStx #[$typedBlocks,*] #[$[$subStx],*])
+    let body ← ``(Part.mk #[$titleInlines,*] $(quote titleString) $metaStx #[$typedBlocks,*] #[$subStx,*])
     bindFootnotes footnoteDefs (← bindLinks linkDefs body)
   | .included name => pure name
 where

src/verso/Verso/Doc/Lsp.lean

@@ -208,20 +208,22 @@ where
   syntactic (text : FileMap) (pos : String.Pos) (stx : Syntax) : Option (Array Syntax) := do
     if includes stx pos |>.getD true then
       match stx with
-        | `(block|directive{%$opener $_name $_args*}[$_contents*]%$closer )
+        | `(block|:::%$opener $_name $_args* {$_contents*}%$closer )
         | `(block|```%$opener | $_contents ```%$closer)
         | `(block|```%$opener $_name $_args* | $_contents ```%$closer) =>
           if (includes opener pos).getD false || (includes closer pos).getD false then
             return #[opener, closer]
         | _ =>
           match stx with
-          | `(inline| ${%$opener1 code{%$opener2 $_ }%$closer1 }%$closer2)
-          | `(inline| $${%$opener1 code{%$opener2 $_ }%$closer1 }%$closer2)
+          | `(inline| \math%$opener1 code(%$opener2 $_ )%$closer1)
+          | `(inline| \displaymath%$opener1 code(%$opener2 $_ )%$closer1) =>
+            if (includes opener1 pos).getD false || (includes closer1 pos).getD false || (includes opener2 pos).getD false then
+              return #[opener1, closer1, opener2]
           | `(inline| link[%$opener1 $_* ]%$closer1 (%$opener2 $_ )%$closer2)
           | `(inline| link[%$opener1 $_* ]%$closer1 [%$opener2 $_ ]%$closer2) =>
             if (includes opener1 pos).getD false || (includes closer1 pos).getD false || (includes opener2 pos).getD false || (includes closer2 pos).getD false then
               return #[opener1, closer1, opener2, closer2]
-          |  `(inline| code{%$opener $_ }%$closer) =>
+          |  `(inline| code(%$opener $_ )%$closer) =>
             if (includes opener pos).getD false || (includes closer pos).getD false then
               return #[opener, closer]
           | `(inline| role{%$opener1 $name $_* }%$closer1 [%$opener2 $subjects ]%$closer2) =>
@@ -586,7 +588,7 @@ partial def directiveResizings
     (parents : Array (Syntax × Syntax))
     (subject : Syntax) :
     StateM (Array (Bool × Syntax × Syntax × TextEditBatch)) Unit := do
-  if let `(block|directive{%$opener $_name $_args*}[$contents*]%$closer ) := subject then
+  if let `(block|:::%$opener $_name $_args* { $contents* }%$closer ) := subject then
     let parents := parents.push (opener, closer)
     if onLine opener || onLine closer then
       if let some edit := parents.flatMapM getIncreases then
@@ -634,7 +636,7 @@ where
     pure (outer ++ inner)
 
   getDecreasesIn (stx : Syntax) : Option TextEditBatch :=
-    if let `(block|directive{%$opener $_name $_args*}[$contents*]%$closer) := stx then
+    if let `(block|:::%$opener $_name $_args* {$contents*}%$closer) := stx then
       getDecreases (opener, closer) contents
     else if let .node _ _ children := stx then children.flatMapM getDecreasesIn
     else pure #[]