` element with the provided `class`.
+-/
+@[role]
+def htmlSpan : RoleExpanderOf ClassArgs
+ | {«class»}, stxs => do
let contents ← stxs.mapM elabInline
- let val ← ``(Inline.other (Blog.InlineExt.htmlSpan $(quote classes)) #[$contents,*])
- pure #[val]
+ ``(Inline.other (Blog.InlineExt.htmlSpan $(quote «class»)) #[$contents,*])
+
-@[directive_expander htmlDiv]
-def htmlDiv : DirectiveExpander
- | args, stxs => do
- let classes ← classArgs.run args
+/--
+Wraps the contents in an HTML `` element with the provided `class`.
+-/
+@[directive]
+def htmlDiv : DirectiveExpanderOf ClassArgs
+ | {«class»}, stxs => do
let contents ← stxs.mapM elabBlock
- let val ← ``(Block.other (Blog.BlockExt.htmlDiv $(quote classes)) #[ $contents,* ])
- pure #[val]
+ ``(Block.other (Blog.BlockExt.htmlDiv $(quote «class»)) #[ $contents,* ])
+
-private partial def attrs : ArgParse DocElabM (Array (String × String)) := List.toArray <$> remaining attr
+private partial def attrs : ArgParse DocElabM (Array (String × String)) := List.toArray <$> .many attr
where
- remaining {m} {α} (p : ArgParse m α) : ArgParse m (List α) :=
- (.done *> pure []) <|> ((· :: ·) <$> p <*> remaining p)
attr : ArgParse DocElabM (String × String) :=
(fun (k, v) => (k.getId.toString (escape := false), v)) <$> .anyNamed `attribute .string
-@[directive_expander html]
-def html : DirectiveExpander
- | args, stxs => do
- let (name, attrs) ← ArgParse.run ((·, ·) <$> .positional `name .name <*> attrs) args
+structure HtmlArgs where
+ name : Name
+ attrs : Array (String × String)
+
+instance : FromArgs HtmlArgs DocElabM where
+ fromArgs := HtmlArgs.mk <$> .positional `name .name <*> attrs
+
+
+@[directive]
+def html : DirectiveExpanderOf HtmlArgs
+ | {name, attrs}, stxs => do
let tag := name.toString (escape := false)
let contents ← stxs.mapM elabBlock
- let val ← ``(Block.other (Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs)) #[ $contents,* ])
- pure #[val]
+ ``(Block.other (Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs)) #[ $contents,* ])
-@[directive_expander blob]
-def blob : DirectiveExpander
- | #[.anon (.name blobName)], stxs => do
+structure BlobArgs where
+ blobName : Ident
+
+instance : FromArgs BlobArgs DocElabM where
+ fromArgs := BlobArgs.mk <$> .positional `blobName .ident
+
+@[directive]
+def blob : DirectiveExpanderOf BlobArgs
+ | {blobName}, stxs => do
if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
let actualName ← realizeGlobalConstNoOverloadWithInfo blobName
- let val ← ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
- pure #[val]
- | _, _ => throwUnsupportedSyntax
+ ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
-@[role_expander blob]
-def inlineBlob : RoleExpander
- | #[.anon (.name blobName)], stxs => do
+@[role blob]
+def inlineBlob : RoleExpanderOf BlobArgs
+ | {blobName}, stxs => do
if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
let actualName ← realizeGlobalConstNoOverloadWithInfo blobName
- let val ← ``(Inline.other (Blog.InlineExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
- pure #[val]
- | _, _ => throwUnsupportedSyntax
+ ``(Inline.other (Blog.InlineExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
+
+structure LabelArgs where
+ label : Name
-@[role_expander label]
-def label : RoleExpander
- | #[.anon (.name l)], stxs => do
+instance : FromArgs LabelArgs DocElabM where
+ fromArgs := LabelArgs.mk <$> .positional `blobName .name
+
+@[role]
+def label : RoleExpanderOf LabelArgs
+ | {label}, stxs => do
let args ← stxs.mapM elabInline
- let val ← ``(Inline.other (Blog.InlineExt.label $(quote l.getId)) #[ $[ $args ],* ])
- pure #[val]
- | _, _ => throwUnsupportedSyntax
+ ``(Inline.other (Blog.InlineExt.label $(quote label)) #[ $[ $args ],* ])
-@[role_expander ref]
-def ref : RoleExpander
- | #[.anon (.name l)], stxs => do
+@[role]
+def ref : RoleExpanderOf LabelArgs
+ | {label}, stxs => do
let args ← stxs.mapM elabInline
- let val ← ``(Inline.other (Blog.InlineExt.ref $(quote l.getId)) #[ $[ $args ],* ])
- pure #[val]
- | _, _ => throwUnsupportedSyntax
+ ``(Inline.other (Blog.InlineExt.ref $(quote label)) #[ $[ $args ],* ])
+structure PageLinkArgs where
+ page : Name
+ id? : Option String
-@[role_expander page_link]
-def page_link : RoleExpander
- | args, stxs => do
- let (page, id?) ← ArgParse.run ((·, ·) <$> .positional `page .name <*> (some <$> .positional `id .string <|> pure none)) args
- let inls ← stxs.mapM elabInline
- let val ← ``(Inline.other (Blog.InlineExt.pageref $(quote page) $(quote id?)) #[ $[ $inls ],* ])
- pure #[val]
+instance : FromArgs PageLinkArgs DocElabM where
+ fromArgs :=
+ PageLinkArgs.mk <$>
+ .positional `page .name <*>
+ (some <$> .positional `id .string <|> pure none)
+@[role]
+def page_link : RoleExpanderOf PageLinkArgs
+ | {page, id?}, stxs => do
+ let inls ← stxs.mapM elabInline
+ ``(Inline.other (Blog.InlineExt.pageref $(quote page) $(quote id?)) #[ $[ $inls ],* ])
-- The assumption here is that suffixes are _mostly_ unique, so the arrays will likely be very
@@ -192,11 +219,15 @@ initialize messageContextExt : EnvExtension ExampleMessages ← registerEnvExten
initialize registerTraceClass `Elab.Verso.block.lean
+def leanExampleProject.Args := Name × String
+
+instance : FromArgs leanExampleProject.Args DocElabM :=
+ ⟨(·, ·) <$> .positional `name .name <*> .positional `projectDir .string⟩
+
open System in
-@[block_role_expander leanExampleProject]
-def leanExampleProject : BlockRoleExpander
- | args, #[] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Loading example project") <| do
- let (name, projectDir) ← ArgParse.run ((·, ·) <$> .positional `name .name <*> .positional `projectDir .string) args
+@[block_command]
+def leanExampleProject : BlockCommandOf leanExampleProject.Args
+ | (name, projectDir) => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Loading example project") <| do
if exampleContextExt.getState (← getEnv) |>.contexts |>.contains name then
throwError "Example context '{name}' already defined in this module"
let path : FilePath := ⟨projectDir⟩
@@ -214,19 +245,16 @@ def leanExampleProject : BlockRoleExpander
for (name, ex) in savedExamples.toArray do
modifyEnv fun env => messageContextExt.modifyState env fun s => {s with messages := s.messages.insert name (.inr ex.messages) }
Verso.Hover.addCustomHover (← getRef) <| "Contains:\n" ++ String.join (savedExamples.toList.map (s!" * `{toString ·.fst}`\n"))
- pure #[]
- | _, more =>
- if h : more.size > 0 then
- throwErrorAt more[0] "Unexpected contents"
- else
- throwError "Unexpected contents"
+ ``(Block.concat #[])
+
+def leanExampleModule.Args := Name × String × Name
+instance : FromArgs leanExampleModule.Args DocElabM :=
+ ⟨(·, ·, ·) <$> .positional `name .name <*> .positional `projectDir .string <*> .positional `module .name⟩
open System in
-@[block_role_expander leanExampleModule]
-def leanExampleModule : BlockRoleExpander
- | args, #[] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Loading example project") <| do
- let (name, projectDir, module) ←
- ArgParse.run ((·, ·, ·) <$> .positional `name .name <*> .positional `projectDir .string <*> .positional `module .name) args
+@[block_command]
+def leanExampleModule : BlockCommandOf leanExampleModule.Args
+ | (name, projectDir, module) => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Loading example project") <| do
if exampleContextExt.getState (← getEnv) |>.contexts |>.contains name then
throwError "Example context '{name}' already defined in this module"
let path : FilePath := ⟨projectDir⟩
@@ -237,12 +265,7 @@ def leanExampleModule : BlockRoleExpander
modifyEnv fun env => exampleContextExt.modifyState env fun s => {s with
contexts := s.contexts.insert name (.module loadedExamples)
}
- pure #[]
- | _, more =>
- if h : more.size > 0 then
- throwErrorAt more[0] "Unexpected contents"
- else
- throwError "Unexpected contents"
+ ``(Block.concat #[])
private def getSubproject (project : Ident) : TermElabM (NameSuffixMap Example) := do
@@ -291,19 +314,13 @@ instance : FromArgs LeanCommandConfig m where
LeanCommandConfig.mk <$> .positional `project .ident <*> .positional `exampleName .ident <*> .namedD `showProofStates .bool true
end
-@[block_role_expander leanCommand]
-def leanCommand : BlockRoleExpander
- | args, #[] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanCommand") <| do
- let { project, exampleName, showProofStates } ← parseThe LeanCommandConfig args
+@[block_command]
+def leanCommand : BlockCommandOf LeanCommandConfig
+ | { project, exampleName, showProofStates } => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanCommand") <| do
let projectExamples ← getSubproject project
let (_, {highlighted := hls, original := str, ..}) ← projectExamples.getOrSuggest exampleName
Verso.Hover.addCustomHover exampleName s!"```lean\n{str}\n```"
- pure #[← `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote project.getId), showProofStates := $(quote showProofStates) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Block.code $(quote str)])]
- | _, more =>
- if h : more.size > 0 then
- throwErrorAt more[0] "Unexpected contents"
- else
- throwError "Unexpected contents"
+ `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote project.getId), showProofStates := $(quote showProofStates) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Block.code $(quote str)])
structure LeanCommandAtArgs where
project : Ident
@@ -321,10 +338,9 @@ private def useRange (startLine : Nat) (endLine? : Option Nat) (range : Position
else
startLine ≥ startLine' && startLine ≤ endLine' -- point is in region
-@[block_role_expander leanCommandAt]
-def leanCommandAt : BlockRoleExpander
- | args, #[] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanCommand") <| do
- let {project, line, endLine?} ← parseThe LeanCommandAtArgs args
+@[block_command]
+def leanCommandAt : BlockCommandOf LeanCommandAtArgs
+ | {project, line, endLine?} => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanCommand") <| do
let projectExamples ← getModule project
let mut hls := #[]
@@ -341,38 +357,47 @@ def leanCommandAt : BlockRoleExpander
ranges.map (fun (l, l') => s!"{l}–{l'}") |>.toList |> (.group <| Std.Format.joinSep · ("," ++ .line))
Lean.logError m!"No example found on line {line}. Valid lines are: {indentD rangeDoc}"
- pure #[← `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote project.getId) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[])]
- | _, more =>
- if h : more.size > 0 then
- throwErrorAt more[0] "Unexpected contents"
- else
- throwError "Unexpected contents"
+ `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote project.getId) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[])
+
+
+structure NoArgs where
-@[role_expander leanKw]
-def leanKw : RoleExpander
- | args, #[arg] => do
- ArgParse.run .done args
+instance : FromArgs NoArgs m where
+ fromArgs := pure ⟨⟩
+
+@[role]
+def leanKw : RoleExpanderOf NoArgs
+ | ⟨⟩, #[arg] => do
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)])]
+ ``(Inline.other (Blog.InlineExt.customHighlight $(quote hl)) #[Inline.code $(quote kw.getString)])
| _, more =>
if h : more.size > 0 then
throwErrorAt more[0] "Unexpected contents"
else
throwError "Unexpected arguments"
-@[role_expander leanTerm]
-def leanTerm : RoleExpander
- | args, #[arg] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanTerm") <| do
- let (project, showProofStates) ← ArgParse.run ((·, ·) <$> .positional `project .ident <*> .namedD `showProofStates .bool true) args
+structure LeanTermArgs where
+ project : Ident
+ showProofStates : Bool
+
+instance : FromArgs LeanTermArgs DocElabM where
+ fromArgs :=
+ LeanTermArgs.mk <$>
+ .positional `project .ident <*>
+ .namedD `showProofStates .bool true
+
+@[role]
+def leanTerm : RoleExpanderOf LeanTermArgs
+ | {project, showProofStates}, #[arg] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanTerm") <| do
let `(inline|code( $name:str )) := arg
| throwErrorAt arg "Expected code literal with the example name"
let exampleName := name.getString.toName
let projectExamples ← getSubproject project
let (_, {highlighted := hls, original := str, ..}) ← projectExamples.getOrSuggest <| mkIdentFrom name exampleName
Verso.Hover.addCustomHover arg s!"```lean\n{str}\n```"
- pure #[← `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote project.getId) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Inline.code $(quote str)])]
+ `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote project.getId) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Inline.code $(quote str)])
| _, more =>
if h : more.size > 0 then
throwErrorAt more[0] "Unexpected contents"
@@ -392,10 +417,9 @@ structure LeanBlockConfig where
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
-@[code_block_expander leanInit]
-def leanInit : CodeBlockExpander
- | args , str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanInit") <| do
- let config ← parseThe LeanBlockConfig args
+@[code_block]
+def leanInit : CodeBlockExpanderOf LeanBlockConfig
+ | 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
if !header.raw[0].isNone then
@@ -418,17 +442,17 @@ def leanInit : CodeBlockExpander
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
- pure #[← ``(Block.code $(quote str.getString))] -- TODO highlighting hack
- else pure #[]
+ ``(Block.code $(quote str.getString)) -- TODO highlighting hack
+ else
+ ``(Block.concat #[])
where
configureCommandState (env : Environment) (msg : MessageLog) : Command.State :=
{ Command.mkState env msg with infoState := { enabled := true } }
open SubVerso.Highlighting Highlighted in
-@[code_block_expander lean]
-def lean : CodeBlockExpander
- | args, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| withoutAsync do
- let config ← parseThe LeanBlockConfig args
+@[code_block]
+def lean : CodeBlockExpanderOf LeanBlockConfig
+ | config, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| withoutAsync do
let x := config.exampleContext
let (commandState, state) ← match exampleContextExt.getState (← getEnv) |>.contexts.find? x.getId with
| some (.inline commandState state) => pure (commandState, state)
@@ -489,9 +513,9 @@ def lean : CodeBlockExpander
setInfoState infoSt
setEnv env
if config.show.getD true then
- pure #[← `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote x.getId), showProofStates := $(quote config.showProofStates) } $(quote hls)) #[Block.code $(quote str.getString)])]
+ `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote x.getId), showProofStates := $(quote config.showProofStates) } $(quote hls)) #[Block.code $(quote str.getString)])
else
- pure #[]
+ ``(Block.concat [])
structure LeanInlineConfig where
@@ -506,6 +530,7 @@ instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr
where
strLit : ValDesc m StrLit := {
description := "string literal containing an expected type",
+ signature := .String
get
| .str s => pure s
| other => throwError "Expected string, got {repr other}"
@@ -564,10 +589,9 @@ where
modifyInfoState fun s => { s with trees := f s.trees }
open SubVerso.Highlighting Highlighted in
-@[role_expander lean]
-def leanInline : RoleExpander
- | args, elts => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| do
- let config ← parseThe LeanInlineConfig args
+@[role]
+def leanInline : RoleExpanderOf LeanInlineConfig
+ | config, elts => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| do
let #[code] := elts
| throwError "Expected precisely one code element"
let `(inline|code( $str:str )) := code
@@ -639,7 +663,7 @@ def leanInline : RoleExpander
}
let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
- pure #[← `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote config.exampleContext.getId) } $(quote hls)) #[Inline.code $(quote str.getString)])]
+ `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote config.exampleContext.getId) } $(quote hls)) #[Inline.code $(quote str.getString)])
open Lean.Elab.Tactic.GuardMsgs
export WhitespaceMode (exact lax normalized)
@@ -654,40 +678,19 @@ instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr
fromArgs :=
LeanOutputConfig.mk <$>
.positional `name output <*>
- .named `severity sev true <*>
+ .named `severity .messageSeverity true <*>
((·.getD false) <$> .named `summarize .bool true) <*>
- ((·.getD .exact) <$> .named `whitespace ws true)
+ ((·.getD .exact) <$> .named `whitespace .whitespaceMode true)
where
output : ValDesc m Ident := {
description := "output name",
+ signature := .Ident
get := fun
| .name x => pure x
| other => throwError "Expected output name, got {repr other}"
}
opt {α} (p : ArgParse m α) : ArgParse m (Option α) := (some <$> p) <|> pure none
optDef {α} (fallback : α) (p : ArgParse m α) : ArgParse m α := p <|> pure fallback
- sev : ValDesc m MessageSeverity := {
- description := open MessageSeverity in m!"The expected severity: '{``error}', '{``warning}', or '{``information}'",
- get := open MessageSeverity in fun
- | .name b => do
- let b' ← realizeGlobalConstNoOverloadWithInfo b
- if b' == ``MessageSeverity.error then pure MessageSeverity.error
- else if b' == ``MessageSeverity.warning then pure MessageSeverity.warning
- else if b' == ``MessageSeverity.information then pure MessageSeverity.information
- else throwErrorAt b "Expected '{``error}', '{``warning}', or '{``information}'"
- | other => throwError "Expected severity, got {repr other}"
- }
- ws : ValDesc m WhitespaceMode := {
- description := open WhitespaceMode in m!"The expected whitespace mode: '{``exact}', '{``normalized}', or '{``lax}'",
- get := open WhitespaceMode in fun
- | .name b => do
- let b' ← realizeGlobalConstNoOverloadWithInfo b
- if b' == ``WhitespaceMode.exact then pure WhitespaceMode.exact
- else if b' == ``WhitespaceMode.normalized then pure WhitespaceMode.normalized
- else if b' == ``WhitespaceMode.lax then pure WhitespaceMode.lax
- else throwErrorAt b "Expected '{``exact}', '{``normalized}', or '{``lax}'"
- | other => throwError "Expected whitespace mode, got {repr other}"
- }
open SubVerso.Highlighting in
private def leanOutputBlock [bg : BlogGenre genre] (message : Highlighted.Message) (summarize := false) (expandTraces : List Name := []) : Block genre :=
@@ -700,11 +703,9 @@ private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Messa
else
Inline.other (bg.inline_eq ▸ InlineExt.message message expandTraces) #[Inline.code message.toString]
-@[code_block_expander leanOutput]
-def leanOutput : Doc.Elab.CodeBlockExpander
- | args, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanOutput") <| do
- let config ← parseThe LeanOutputConfig args
-
+@[code_block]
+def leanOutput : CodeBlockExpanderOf LeanOutputConfig
+ | config, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanOutput") <| do
let (_, savedInfo) ← messageContextExt.getState (← getEnv) |>.messages |>.getOrSuggest config.name
let messages ← match savedInfo with
| .inl (env, log) =>
@@ -729,7 +730,7 @@ def leanOutput : Doc.Elab.CodeBlockExpander
SubVerso.Highlighting.highlightMessage m
finally setEnv myEnv
``(Block.other (Blog.BlockExt.message false $(quote m') ([] : List Lean.Name)) #[Block.code $(quote str.getString)])
- return #[content]
+ return content
pure messages
| .inr msgs =>
let messages := msgs.toArray.map Prod.snd
@@ -746,7 +747,7 @@ def leanOutput : Doc.Elab.CodeBlockExpander
``(Block.other (Blog.BlockExt.htmlDetails $(quote (sevStr sev)) $(quote preHtml)) #[Block.code $(quote post)])
else
``(Block.other (Blog.BlockExt.htmlDiv $(quote (sevStr sev))) #[Block.code $(quote str.getString)])
- return #[content]
+ return content
pure messages
for m in messages do
@@ -770,19 +771,18 @@ where
open Lean Elab Command in
elab "define_lexed_text" blockName:ident " ← " lexerName:ident : command => do
let lexer ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo lexerName
- elabCommand <| ← `(@[code_block_expander $blockName]
- def $blockName : Doc.Elab.CodeBlockExpander
- | #[], str => do
+ elabCommand <| ← `(@[code_block]
+ def $blockName : Doc.Elab.CodeBlockExpanderOf NoArgs
+ | ⟨⟩, str => do
let out ← Verso.Genre.Blog.LexedText.highlight $(mkIdentFrom lexerName lexer) str.getString
- return #[← ``(Block.other (Blog.BlockExt.lexedText $$(quote out)) #[])]
- | _, str => throwErrorAt str "Expected no arguments")
- elabCommand <| ← `(@[role_expander $blockName]
- def $(mkIdent <| blockName.getId ++ `role) : Doc.Elab.RoleExpander
- | #[], #[inl] => do
+ ``(Block.other (Blog.BlockExt.lexedText $$(quote out)) #[]))
+ elabCommand <| ← `(@[role]
+ def $(mkIdent <| blockName.getId ++ `role) : Doc.Elab.RoleExpanderOf NoArgs
+ | ⟨⟩, #[inl] => do
let `(inline|code($$str)) := inl
| throwErrorAt inl "Expected code"
let out ← Verso.Genre.Blog.LexedText.highlight $(mkIdentFrom lexerName lexer) str.getString
- return #[← ``(Inline.other (Blog.InlineExt.lexedText $$(quote out)) #[])]
+ ``(Inline.other (Blog.InlineExt.lexedText $$(quote out)) #[])
| _, str => throwError "Expected no arguments and a single code element")
diff --git a/src/verso-blog/VersoBlog/Component.lean b/src/verso-blog/VersoBlog/Component.lean
index 58534c151..e3cc344a6 100644
--- a/src/verso-blog/VersoBlog/Component.lean
+++ b/src/verso-blog/VersoBlog/Component.lean
@@ -298,20 +298,21 @@ elab_rules : command
elabCommand cmd1
elabCommand cmd2
if dirTok.isSome then
+
let argPat : Term ← argNames.foldrM (init := ← `(Unit.unit)) fun (x, _) y =>
`(($x, $y))
- let argP : Term ← argNames.foldrM (init := ← `(.done)) fun (x, t) y =>
- `((·, ·) <$> .positional $(quote x.getId) (FromArgVal.fromArgVal (α := $t)) <*> $y)
+ let argP : Term ← argNames.foldrM (init := ← ``(ArgParse.done)) fun (x, t) y =>
+ ``((·, ·) <$> ArgParse.positional $(quote x.getId) (FromArgVal.fromArgVal (α := $t)) <*> $y)
+ let argT ← argNames.foldrM (init := ← `(Unit)) fun (_, t) y => `($t × $y)
+ elabCommand (← `(def T := $argT))
+ elabCommand (← `(instance : FromArgs T DocElabM := ⟨$argP⟩))
let qArgs : Term ← argNames.foldlM (init := x) fun tm (x, _) =>
`($tm $$(quote $x))
let cmd3 ←
`(command|
- @[directive_expander $x]
- def $dirName : DirectiveExpander
- | args, blocks => do
- let $argPat:term ← ArgParse.run $argP args
- pure #[← `($qArgs #[$$(← blocks.mapM elabBlock),*])]
- )
+ @[directive $x]
+ def $dirName : DirectiveExpanderOf T
+ | $argPat, blocks => do `($qArgs #[$$(← blocks.mapM elabBlock),*]))
elabCommand cmd3
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 3ec46cfe0..a32f751b7 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -127,6 +127,7 @@ instance : FromArgs RoleArgs m where
where
stringOrName : ValDesc m String := {
description := "remote name (string or identifier)"
+ signature := .String ∪ .Ident
get
| .str s => pure s.getString
| .name n => pure n.getId.toString
@@ -136,12 +137,11 @@ end
/--
Inserts a reference to the provided tag.
-/
-@[role_expander ref]
-def ref : RoleExpander
- | args, content => do
- let {canonicalName, domain, remote} ← parseThe RoleArgs args
+@[role]
+def ref : RoleExpanderOf RoleArgs
+ | {canonicalName, domain, remote}, content => do
let content ← content.mapM elabInline
- return #[← ``(Inline.other (Inline.ref $(quote canonicalName) $(quote domain) $(quote remote)) #[$content,*])]
+ ``(Inline.other (Inline.ref $(quote canonicalName) $(quote domain) $(quote remote)) #[$content,*])
block_extension Block.paragraph where
traverse := fun _ _ _ => pure none
@@ -159,14 +159,11 @@ Indicates that all the block-level elements contained within the directive are a
paragraph. In HTML output, they are rendered with less space between them, and LaTeX renders them as
a single paragraph (e.g. without extraneous indentation).
-/
-@[directive_expander paragraph]
-def paragraph : DirectiveExpander
- | #[], stxs => do
+@[directive]
+def paragraph : DirectiveExpanderOf Unit
+ | (), stxs => do
let args ← stxs.mapM elabBlock
- let val ← ``(Block.other Block.paragraph #[ $[ $args ],* ])
- pure #[val]
- | _, _ => Lean.Elab.throwUnsupportedSyntax
-
+ ``(Block.other Block.paragraph #[ $[ $args ],* ])
structure Config where
destination : System.FilePath := "_out"
diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean
index 71f51aedd..400d8c081 100644
--- a/src/verso-manual/VersoManual/Bibliography.lean
+++ b/src/verso-manual/VersoManual/Bibliography.lean
@@ -265,11 +265,18 @@ inline_extension Inline.cite (citations : List Citable) (style : Style := .paren
structure CiteConfig where
citations : List Name
-partial def CiteConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] : ArgParse m CiteConfig :=
+section
+variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m]
+
+partial def CiteConfig.parse : ArgParse m CiteConfig :=
CiteConfig.mk <$> many1 (.positional `citation .resolvedName)
where
- many1 p := (· :: ·) <$> p <*> many p
- many p := (· :: ·) <$> p <*> many p <|> pure []
+ many1 p := (· :: ·) <$> p <*> .many p
+
+instance : FromArgs CiteConfig m where
+ fromArgs := CiteConfig.parse
+
+end
end Bibliography
@@ -277,23 +284,20 @@ export Verso.Genre.Manual.Bibliography (InProceedings Thesis ArXiv Article)
open Bibliography
-@[role_expander citep]
-def citep : RoleExpander
- | args, extra => do
- let config ← CiteConfig.parse.run args
+@[role]
+def citep : RoleExpanderOf CiteConfig
+ | config, extra => do
let xs := config.citations.map mkIdent |>.toArray
- return #[← ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.parenthetical) #[$(← extra.mapM elabInline),*])]
+ ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.parenthetical) #[$(← extra.mapM elabInline),*])
-@[role_expander citet]
-def citet : RoleExpander
- | args, extra => do
- let config ← CiteConfig.parse.run args
+@[role]
+def citet : RoleExpanderOf CiteConfig
+ | config, extra => do
let xs := config.citations.map mkIdent |>.toArray
- return #[← ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.textual) #[$(← extra.mapM elabInline),*])]
+ ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.textual) #[$(← extra.mapM elabInline),*])
-@[role_expander citehere]
-def citehere : RoleExpander
- | args, extra => do
- let config ← CiteConfig.parse.run args
+@[role]
+def citehere : RoleExpanderOf CiteConfig
+ | config, extra => do
let xs := config.citations.map mkIdent |>.toArray
- return #[← ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.here) #[$(← extra.mapM elabInline),*])]
+ ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.here) #[$(← extra.mapM elabInline),*])
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 4debd3912..5ca72ff5d 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -40,7 +40,8 @@ open Verso.Doc.Suggestion
variable {m} [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadInfoTree m]
def ValDesc.documentableName : ValDesc m (Ident × Name) where
- description := m!"a name with documentation"
+ description := "a name with documentation"
+ signature := .Ident
get
| .name n => do
let x ← realizeGlobalConstNoOverloadWithInfo n
@@ -1410,13 +1411,13 @@ def DocstringConfig.parse : ArgParse m DocstringConfig :=
.namedD `hideStructureConstructor .bool false <*>
.named `label .string true
-end
+instance : FromArgs DocstringConfig m := ⟨DocstringConfig.parse⟩
-@[block_role_expander docstring]
-def docstring : BlockRoleExpander
- | args, #[] => do
- let ⟨(x, name), allowMissing, hideFields, hideCtor, customLabel⟩ ← DocstringConfig.parse.run args
+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
withOptions opts do
@@ -1439,8 +1440,7 @@ def docstring : BlockRoleExpander
let signature ← Signature.forName name
let extras ← getExtras name declType
- pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature) $(quote customLabel)) #[$(blockStx ++ extras),*])]
- | _, more => throwErrorAt more[0]! "Unexpected block argument"
+ ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature) $(quote customLabel)) #[$(blockStx ++ extras),*])
where
getExtras (name : Name) (declType : Block.Docstring.DeclType) : DocElabM (Array Term) :=
match declType with
@@ -1508,13 +1508,14 @@ structure IncludeDocstringOpts where
def IncludeDocstringOpts.parse : ArgParse m IncludeDocstringOpts :=
IncludeDocstringOpts.mk <$> (.positional `name .documentableName <&> (·.2)) <*> .namedD `elab .bool true
-end
+instance : FromArgs IncludeDocstringOpts m where
+ fromArgs := IncludeDocstringOpts.parse
-@[block_role_expander includeDocstring]
-def includeDocstring : BlockRoleExpander
- | args, #[] => do
- let {name, elaborate} ← IncludeDocstringOpts.parse.run args
+end
+@[block_command]
+def includeDocstring : BlockCommandOf IncludeDocstringOpts
+ | {name, elaborate} => do
let fromMd :=
if elaborate then
blockFromMarkdownWithLean [name]
@@ -1529,9 +1530,7 @@ def includeDocstring : BlockRoleExpander
| throwError "Failed to parse docstring as Markdown"
ast.blocks.mapM fromMd
- pure blockStx
-
- | _args, more => throwErrorAt more[0]! "Unexpected block argument"
+ ``(Doc.Block.concat #[$blockStx,*])
def Block.optionDocs (name : Name) (defaultValue : Option Highlighted) : Block where
name := `Verso.Genre.Manual.optionDocs
@@ -1568,19 +1567,18 @@ def highlightDataValue (v : DataValue) : Highlighted :=
| .ofSyntax (v : Syntax) => ⟨.unknown, toString v⟩ -- TODO
-@[block_role_expander optionDocs]
-def optionDocs : BlockRoleExpander
- | args, #[] => do
- let #[.anon (.name x)] := args
- | throwError "Expected exactly one positional argument that is a name"
+def optionDocs.Args := Ident
+instance : FromArgs optionDocs.Args DocElabM := ⟨.positional `name .ident "The option name"⟩
+
+@[block_command]
+def optionDocs : BlockCommandOf optionDocs.Args
+ | x => do
let optDecl ← getOptionDecl x.getId
- Doc.PointOfInterest.save x optDecl.declName.toString
+ Doc.PointOfInterest.save x.raw optDecl.declName.toString
let some mdAst := MD4Lean.parse optDecl.descr
- | throwErrorAt x "Failed to parse docstring as Markdown"
+ | throwErrorAt x.raw "Failed to parse docstring as Markdown"
let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean [])
- pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.optionDocs $(quote x.getId) $(quote <| highlightDataValue optDecl.defValue)) #[$contents,*])]
-
- | _, more => throwErrorAt more[0]! "Unexpected block argument"
+ ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.optionDocs $(quote x.getId) $(quote <| highlightDataValue optDecl.defValue)) #[$contents,*])
open Verso.Search in
def optionDomainMapper : DomainMapper :=
@@ -1648,7 +1646,11 @@ structure TacticDocsOptions where
replace : Bool
allowMissing : Option Bool
-def TacticDocsOptions.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgParse m TacticDocsOptions :=
+section
+
+variable [Monad m] [MonadError m] [MonadLiftT CoreM m]
+
+def TacticDocsOptions.parse : ArgParse m TacticDocsOptions :=
TacticDocsOptions.mk <$>
.positional `name strOrName <*>
.named `show .string true <*>
@@ -1656,13 +1658,17 @@ def TacticDocsOptions.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgP
.named `allowMissing .bool true
where
strOrName : ValDesc m (String ⊕ Name) := {
- description := m!"First token in tactic, or canonical parser name"
+ description := "First token in tactic, or canonical parser name"
+ signature := .Ident ∪ .String
get := fun
| .name x => pure (.inr x.getId)
| .str s => pure (.inl s.getString)
| .num n => throwErrorAt n "Expected tactic name (either first token as string, or internal parser name)"
}
+instance : FromArgs TacticDocsOptions m := ⟨TacticDocsOptions.parse⟩
+
+end
open Lean Elab Term Parser Tactic Doc in
private def getTactic (name : String ⊕ Name) : TermElabM TacticDoc := do
@@ -1682,10 +1688,9 @@ private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) :
return some t
return none
-@[directive_expander tactic]
-def tactic : DirectiveExpander
- | args, more => do
- let opts ← TacticDocsOptions.parse.run args
+@[directive]
+def tactic : DirectiveExpanderOf TacticDocsOptions
+ | opts, more => do
let tactic ← getTactic opts.name
Doc.PointOfInterest.save (← getRef) tactic.userName
if tactic.userName == tactic.internalName.toString && opts.show.isNone then
@@ -1697,9 +1702,7 @@ def tactic : DirectiveExpander
| throwError "Failed to parse docstring as Markdown"
mdAst.blocks.mapM (blockFromMarkdownWithLean [])
let userContents ← more.mapM elabBlock
- pure #[← ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])]
-
-
+ ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])
def Inline.tactic : Inline where
name := `Verso.Genre.Manual.tacticInline
@@ -1772,13 +1775,19 @@ def tactic.descr : BlockDescr := withHighlighting {
structure TacticInlineOptions where
«show» : Option String
-def TacticInlineOptions.parse [Monad m] [MonadError m] : ArgParse m TacticInlineOptions :=
+section
+variable [Monad m] [MonadError m]
+
+def TacticInlineOptions.parse : ArgParse m TacticInlineOptions :=
TacticInlineOptions.mk <$> .named `show .string true
-@[role_expander tactic]
-def tacticInline : RoleExpander
- | args, inlines => do
- let {«show»} ← TacticInlineOptions.parse.run args
+instance : FromArgs TacticInlineOptions m where
+ fromArgs := TacticInlineOptions.parse
+end
+
+@[role tactic]
+def tacticInline : RoleExpanderOf TacticInlineOptions
+ | {«show»}, inlines => do
let #[arg] := inlines
| throwError "Expected exactly one argument"
let `(inline|code( $tac:str )) := arg
@@ -1790,7 +1799,7 @@ def tacticInline : RoleExpander
let hl : Highlighted := tacToken tacticDoc «show»
- pure #[← `(Verso.Doc.Inline.other {Inline.tactic with data := ToJson.toJson $(quote hl)} #[Verso.Doc.Inline.code $(quote tacticDoc.userName)])]
+ `(Verso.Doc.Inline.other {Inline.tactic with data := ToJson.toJson $(quote hl)} #[Verso.Doc.Inline.code $(quote tacticDoc.userName)])
where
tacToken (t : Lean.Elab.Tactic.Doc.TacticDoc) (overrideStr : Option String) : Highlighted :=
.token ⟨.keyword t.internalName none t.docString, overrideStr.getD t.userName⟩
@@ -1838,10 +1847,9 @@ def getConvTactic (name : String ⊕ Name) (allowMissing : Option Bool) : TermEl
return ⟨k, ← getDocString? (← getEnv) k⟩
throwError m!"Conv tactic not found: {kind}"
-@[directive_expander conv]
-def conv : DirectiveExpander
- | args, more => do
- let opts ← TacticDocsOptions.parse.run args
+@[directive]
+def conv : DirectiveExpanderOf TacticDocsOptions
+ | opts, more => do
let tactic ← getConvTactic opts.name opts.allowMissing
Doc.PointOfInterest.save (← getRef) tactic.name.toString
let contents ← if let some d := tactic.docs? then
@@ -1852,7 +1860,7 @@ def conv : DirectiveExpander
let userContents ← more.mapM elabBlock
let some toShow := opts.show
| throwError "An explicit 'show' is mandatory for conv docs (for now)"
- pure #[← ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*])]
+ ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*])
open Verso.Search in
def convDomainMapper : DomainMapper := {
diff --git a/src/verso-manual/VersoManual/Docstring/Progress.lean b/src/verso-manual/VersoManual/Docstring/Progress.lean
index affceb52f..ab6755f47 100644
--- a/src/verso-manual/VersoManual/Docstring/Progress.lean
+++ b/src/verso-manual/VersoManual/Docstring/Progress.lean
@@ -58,16 +58,14 @@ open Lean Elab Command in
names := names.qsort (·.toString < ·.toString)
elabCommand <| ← `(private def $(mkIdent `allRootNames) : Array Name := #[$(names.map (quote · : Name → Term)),*])
-@[directive_expander progress]
-def progress : DirectiveExpander
- | args, blocks => do
- if h : args.size > 0 then
- throwErrorAt args[0].syntax "Expected 0 arguments"
+@[directive]
+def progress : DirectiveExpanderOf Unit
+ | (), blocks => do
let mut namespaces : NameSet := {}
let mut exceptions : NameSet := {}
for block in blocks do
match block with
- | `(block|```$nameStx:ident $argsStx* | $contents```) =>
+ | `(block|```$nameStx:ident $_argsStx* | $contents```) =>
let contents := contents.getString
match nameStx.getId with
| `namespace =>
@@ -81,7 +79,6 @@ def progress : DirectiveExpander
| _ => throwErrorAt nameStx "Expected 'namespace' or 'exceptions'"
| _ => throwErrorAt block "Expected code block named 'namespace' or 'exceptions'"
let mut present : NameMap NameSet := {}
- let mut rootPresent : NameSet := {}
for ns in namespaces do
present := present.insert ns {}
@@ -93,7 +90,7 @@ def progress : DirectiveExpander
| .ctorInfo _ => continue -- constructors are documented as children of their types
| _ => pure ()
if ← Meta.isInstance x then continue
- if let .str .anonymous s := x then
+ if let .str .anonymous _ := x then
if let some v := present.find? `_root_ then
present := present.insert `_root_ (v.insert x)
else
@@ -108,7 +105,7 @@ def progress : DirectiveExpander
let present' := present.toList.map (fun x => (x.1, String.intercalate " " (x.2.toList.map Name.toString)))
let allTactics : Array Name := (← Elab.Tactic.Doc.allTacticDocs).map (fun t => t.internalName)
- pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.progress $(quote namespaces.toArray) $(quote exceptions.toArray) $(quote present') $(quote allTactics)) #[])]
+ ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.progress $(quote namespaces.toArray) $(quote exceptions.toArray) $(quote present') $(quote allTactics)) #[])
@[block_extension Block.progress]
def progress.descr : BlockDescr where
diff --git a/src/verso-manual/VersoManual/Draft.lean b/src/verso-manual/VersoManual/Draft.lean
index 064986bdc..1d185cb73 100644
--- a/src/verso-manual/VersoManual/Draft.lean
+++ b/src/verso-manual/VersoManual/Draft.lean
@@ -45,15 +45,13 @@ block_extension Block.draft where
content.mapM goB
/-- Hide draft-only content when in not in draft mode -/
-@[role_expander draft]
-def draft : RoleExpander
- | args, contents => do
- ArgParse.done.run args
- pure #[← ``(Verso.Doc.Inline.other Inline.draft #[$[$(← contents.mapM elabInline)],*])]
+@[role]
+def draft : RoleExpanderOf Unit
+ | (), contents => do
+ ``(Verso.Doc.Inline.other Inline.draft #[$[$(← contents.mapM elabInline)],*])
/-- Hide draft-only content when in not in draft mode -/
-@[directive_expander draft]
-def draftBlock : DirectiveExpander
- | args, contents => do
- ArgParse.done.run args
- pure #[← ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlock)],*])]
+@[directive draft]
+def draftBlock : DirectiveExpanderOf Unit
+ | (), contents => do
+ ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlock)],*])
diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean
index 6651c6593..564108607 100644
--- a/src/verso-manual/VersoManual/Glossary.lean
+++ b/src/verso-manual/VersoManual/Glossary.lean
@@ -20,9 +20,15 @@ structure TechArgs where
key : Option String
normalize : Bool
-def TechArgs.parse [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] : ArgParse m TechArgs :=
+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
+instance : FromArgs TechArgs m := ⟨TechArgs.parse⟩
+
+end
private def glossaryState := `Verso.Genre.Manual.glossary
@@ -64,10 +70,9 @@ of the automatically-derived key.
Uses of `tech` use the same process to derive a key, and the key is matched against the `deftech` table.
-/
-@[role_expander deftech]
-def deftech : RoleExpander
- | args, content => do
- let {key, normalize} ← TechArgs.parse.run args
+@[role]
+def deftech : RoleExpanderOf TechArgs
+ | {key, normalize}, content => do
-- Heuristically guess at the string and key (usually works)
let str := inlineToString (← getEnv) <| mkNullNode content
@@ -79,12 +84,11 @@ def deftech : RoleExpander
let content ← content.mapM elabInline
- let stx ←
- `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
- let asString : String := techString (Doc.Inline.concat content)
- let k : String := ($(quote key) : Option String).getD asString
- Doc.Inline.other {Inline.deftech with data := ToJson.toJson (if $(quote normalize) then normString k else k, asString)} content)
- return #[stx]
+ `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
+ let asString : String := techString (Doc.Inline.concat content)
+ let k : String := ($(quote key) : Option String).getD asString
+ Doc.Inline.other {Inline.deftech with data := ToJson.toJson (if $(quote normalize) then normString k else k, asString)} content)
+
/-- Adds an internal identifier as a target for a given glossary entry -/
def Glossary.addEntry [Monad m] [MonadState TraverseState m] [MonadLiftT IO m] [MonadReaderOf TraverseContext m]
@@ -163,10 +167,9 @@ information from the arguments in `args`, and then normalizing the resulting str
Call with `(normalize := false)` to disable normalization, and `(key := some k)` to use `k` instead
of the automatically-derived key.
-/
-@[role_expander tech]
-def tech : RoleExpander
- | args, content => do
- let {key, normalize} ← TechArgs.parse.run args
+@[role]
+def tech : RoleExpanderOf TechArgs
+ | {key, normalize}, content => do
-- Heuristically guess at the string and key (usually works)
let str := inlineToString (← getEnv) <| mkNullNode content
@@ -182,11 +185,11 @@ def tech : RoleExpander
let content ← content.mapM elabInline
- let stx ←
- `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
- let k := ($(quote key) : Option String).getD (techString (Doc.Inline.concat content))
- Doc.Inline.other {Inline.tech with data := Json.arr #[Json.str (if $(quote normalize) then normString k else k), Json.str $(quote loc)]} content)
- return #[stx]
+
+ `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
+ let k := ($(quote key) : Option String).getD (techString (Doc.Inline.concat content))
+ Doc.Inline.other {Inline.tech with data := Json.arr #[Json.str (if $(quote normalize) then normString k else k), Json.str $(quote loc)]} content)
+
@[inline_extension tech]
def tech.descr : InlineDescr where
diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index 691b025de..b56a64575 100644
--- a/src/verso-manual/VersoManual/InlineLean.lean
+++ b/src/verso-manual/VersoManual/InlineLean.lean
@@ -86,6 +86,8 @@ structure LeanBlockConfig where
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
+instance : FromArgs LeanBlockConfig m := ⟨LeanBlockConfig.parse⟩
+
structure LeanInlineConfig extends LeanBlockConfig where
/-- The expected type of the term -/
type : Option StrLit
@@ -97,11 +99,14 @@ def LeanInlineConfig.parse : ArgParse m LeanInlineConfig :=
where
strLit : ValDesc m StrLit := {
description := "string literal containing an expected type",
+ signature := .String
get
| .str s => pure s
| other => throwError "Expected string, got {repr other}"
}
+instance : FromArgs LeanInlineConfig m := ⟨LeanInlineConfig.parse⟩
+
end Config
@@ -165,10 +170,9 @@ def reportMessages {m} [Monad m] [MonadLog m] [MonadError m]
/--
Elaborates the provided Lean command in the context of the current Verso module.
-/
-@[code_block_expander lean]
-def lean : CodeBlockExpander
- | args, str => withoutAsync <| do
- let config ← LeanBlockConfig.parse.run args
+@[code_block]
+def lean : CodeBlockExpanderOf LeanBlockConfig
+ | config, str => withoutAsync <| do
PointOfInterest.save (← getRef) ((config.name.map (·.toString)).getD (abbrevFirstLine 20 str.getString))
(kind := Lsp.SymbolKind.file)
@@ -225,9 +229,9 @@ def lean : CodeBlockExpander
if config.show.getD true then
let range := Syntax.getRange? str
let range := range.map (← getFileMap).utf8RangeToLspRange
- pure #[← ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])]
+ ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])
else
- pure #[]
+ ``(Block.concat #[])
finally
if !config.keep.getD true then
setEnv origEnv
@@ -268,10 +272,9 @@ where
/--
Elaborates the provided Lean term in the context of the current Verso module.
-/
-@[code_block_expander leanTerm]
-def leanTerm : CodeBlockExpander
- | args, str => withoutAsync <| do
- let config ← LeanInlineConfig.parse.run args
+@[code_block]
+def leanTerm : CodeBlockExpanderOf LeanInlineConfig
+ | config, str => withoutAsync <| do
let altStr ← parserInputString str
@@ -353,9 +356,9 @@ def leanTerm : CodeBlockExpander
if config.show.getD true then
let range := Syntax.getRange? str
let range := range.map (← getFileMap).utf8RangeToLspRange
- pure #[← ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])]
+ ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])
else
- pure #[]
+ ``(Block.concat #[])
where
withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str
@@ -375,11 +378,10 @@ where
/--
Elaborates the provided Lean term in the context of the current Verso module.
-/
-@[role_expander lean]
-def leanInline : RoleExpander
+@[role lean]
+def leanInline : RoleExpanderOf LeanInlineConfig
-- Async elab is turned off to make sure that info trees and messages are available when highlighting
- | args, inlines => withoutAsync do
- let config ← LeanInlineConfig.parse.run args
+ | config, inlines => withoutAsync do
let #[arg] := inlines
| throwError "Expected exactly one argument"
let `(inline|code( $term:str )) := arg
@@ -470,9 +472,9 @@ def leanInline : RoleExpander
if config.show.getD true then
- pure #[← ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])]
+ ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])
else
- pure #[]
+ ``(Block.concat #[])
where
withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str
@@ -493,10 +495,9 @@ where
/--
Elaborates the provided term in the current Verso context, then ensures that it's a type class that has an instance.
-/
-@[role_expander inst]
-def inst : RoleExpander
- | args, inlines => withoutAsync <| do
- let config ← LeanBlockConfig.parse.run args
+@[role]
+def inst : RoleExpanderOf LeanBlockConfig
+ | config, inlines => withoutAsync <| do
let #[arg] := inlines
| throwError "Expected exactly one argument"
let `(inline|code( $term:str )) := arg
@@ -541,9 +542,9 @@ def inst : RoleExpander
let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
if config.show.getD true then
- pure #[← ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])]
+ ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(quote hls)) #[Inline.code $(quote term.getString)])
else
- pure #[]
+ ``(Block.concat #[])
where
withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str
@@ -616,9 +617,6 @@ structure LeanOutputConfig where
section
variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
-partial def many (p : ArgParse m α) : ArgParse m (List α) :=
- ((· :: ·) <$> p <*> many p) <|> pure []
-
def LeanOutputConfig.parser : ArgParse m LeanOutputConfig :=
LeanOutputConfig.mk <$>
.positional `name output <*>
@@ -628,12 +626,13 @@ def LeanOutputConfig.parser : ArgParse m LeanOutputConfig :=
((·.getD .exact) <$> .named `whitespace .whitespaceMode true) <*>
.namedD `normalizeMetas .bool true <*>
.namedD `allowDiff .nat 0 <*>
- many (.named `expandTrace .name false) <*>
+ .many (.named `expandTrace .name false) <*>
.named `startAt .string true <*>
.named `stopAt .string true
where
output : ValDesc m Ident := {
description := "output name",
+ signature := .Ident
get := fun
| .name x => pure x
| other => throwError "Expected output name, got {repr other}"
@@ -641,16 +640,17 @@ where
opt {α} (p : ArgParse m α) : ArgParse m (Option α) := (some <$> p) <|> pure none
optDef {α} (fallback : α) (p : ArgParse m α) : ArgParse m α := p <|> pure fallback
+instance : FromArgs LeanOutputConfig m := ⟨LeanOutputConfig.parser⟩
+
end
private def withNl (s : String) : String :=
if s.endsWith "\n" then s else s ++ "\n"
open SubVerso.Examples.Messages in
-@[code_block_expander leanOutput]
-def leanOutput : CodeBlockExpander
- | args, str => do
- let config ← LeanOutputConfig.parser.run args
+@[code_block]
+def leanOutput : CodeBlockExpanderOf LeanOutputConfig
+ | config, str => do
PointOfInterest.save (← getRef) (config.name.getId.toString)
(kind := Lsp.SymbolKind.file)
@@ -696,8 +696,8 @@ def leanOutput : CodeBlockExpander
throwErrorAt str s!"Expected severity {sevStr s}, but got {sevStr msg.severity.toSeverity}"
if config.show then
let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize), ($(quote config.expandTraces) : List Name))} #[Block.code $(quote str.getString)])
- return #[content]
- else return #[]
+ return content
+ else return (← ``(Block.concat #[]))
else
let mut best : Option (Nat × String × Highlighted.Message) := none
for msg in msgs do
@@ -720,8 +720,8 @@ def leanOutput : CodeBlockExpander
Log.logSilentInfo m!"Diff is {d} lines:\n{d'}"
if config.show then
let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize), ($(quote config.expandTraces) : List Name))} #[Block.code $(quote str.getString)])
- return #[content]
- else return #[]
+ return content
+ else return (← ``(Block.concat #[]))
let suggs : Array (Nat × Meta.Hint.Suggestion) := texts.map fun (sev, msg) =>
((diffSize config.whitespace msg str.getString).1, {
@@ -778,11 +778,15 @@ inline_extension Inline.name where
structure NameConfig where
full : Option Name
-def NameConfig.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadLiftT TermElabM m] : ArgParse m NameConfig :=
+section
+variable [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadLiftT TermElabM m]
+
+def NameConfig.parse : ArgParse m NameConfig :=
NameConfig.mk <$> ((fun _ => none) <$> .done <|> .positional `name ref)
where
ref : ValDesc m (Option Name) := {
- description := m!"reference name"
+ description := "reference name"
+ signature := .Ident
get := fun
| .name x =>
try
@@ -794,6 +798,9 @@ where
| other => throwError "Expected reference name, got {repr other}"
}
+instance : FromArgs NameConfig m := ⟨NameConfig.parse⟩
+end
+
def constTok [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m]
(name : Name) (str : String) :
m Highlighted := do
@@ -801,10 +808,9 @@ def constTok [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m]
let sig := toString (← (PrettyPrinter.ppSignature name)).1
pure <| .token ⟨.const name sig docs false, str⟩
-@[role_expander name]
-def name : RoleExpander
- | args, #[arg] => do
- let cfg ← NameConfig.parse.run args
+@[role]
+def name : RoleExpanderOf NameConfig
+ | cfg, #[arg] => do
let `(inline|code( $name:str )) := arg
| throwErrorAt arg "Expected code literal with the example name"
let exampleName := name.getString.toName
@@ -818,10 +824,10 @@ def name : RoleExpander
let hl : Highlighted ← constTok resolvedName name.getString
- pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])]
+ `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])
catch e =>
logErrorAt identStx e.toMessageData
- pure #[← `(Inline.code $(quote name.getString))]
+ `(Inline.code $(quote name.getString))
| _, more =>
if h : more.size > 0 then
throwErrorAt more[0] "Unexpected contents"
@@ -830,15 +836,14 @@ def name : RoleExpander
-- Placeholder for module names (eventually hyperlinking these will be important, so better to tag them now)
-@[role_expander module]
-def module : RoleExpander
- | args, #[arg] => do
- let cfg ← ArgParse.done.run args
+@[role]
+def module : RoleExpanderOf Unit
+ | (), #[arg] => do
let `(inline|code( $name:str )) := arg
| throwErrorAt arg "Expected code literal with the module's name"
let exampleName := name.getString.toName
let identStx := mkIdentFrom arg exampleName (canonical := true)
- pure #[← ``(Doc.Inline.code $(quote name.getString))]
+ ``(Doc.Inline.code $(quote name.getString))
| _, more =>
if h : more.size > 0 then
throwErrorAt more[0] "Expected code literal with the module's name"
diff --git a/src/verso-manual/VersoManual/InlineLean/IO.lean b/src/verso-manual/VersoManual/InlineLean/IO.lean
index 8985d1ff1..c6ad1554b 100644
--- a/src/verso-manual/VersoManual/InlineLean/IO.lean
+++ b/src/verso-manual/VersoManual/InlineLean/IO.lean
@@ -50,13 +50,6 @@ structure ExampleFileConfig where
type : FileType
«show» : Bool := true
--- TODO: upstream
-instance [Functor m] : Functor (ValDesc m) where
- map f d := {
- description := d.description
- get := fun v => f <$> d.get v
- }
-
def FileType.parse [Monad m] [MonadError m] : ArgParse m FileType :=
(.positional `type (literally `stdin) *> pure .stdin) <|>
(.positional `type (literally `stdout) *> pure .stdout) <|>
@@ -70,30 +63,34 @@ where
literally (n : Name) : ValDesc m Unit := {
description := n
+ signature := .Ident
get := fun
| .name x => if x.getId == n then pure () else throwErrorAt x m!"Expected '{toString n}', got '{toString x.getId}'"
| nonName => throwError m!"Expected '{toString n}', got {repr nonName}"
}
+section
-def ExampleFileConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m ExampleFileConfig :=
- ExampleFileConfig.mk <$> FileType.parse <*> ((·.getD true) <$> .named `show .bool true)
+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)
def IOExample.exampleFileSyntax [Monad m] [MonadQuotation m] (type : FileType) (contents : String) : m Term := do
`(Block.other (Block.exampleFile $(quote type)) #[Block.code $(quote contents)])
+instance : FromArgs ExampleFileConfig m := ⟨ExampleFileConfig.parse⟩
-@[code_block_expander exampleFile]
-def exampleFile : CodeBlockExpander
- | args, str => do
- let config ← ExampleFileConfig.parse.run args
- let s := str.getString
+end
+@[code_block]
+def exampleFile : CodeBlockExpanderOf ExampleFileConfig
+ | config, str => do
+ let s := str.getString
if config.show then
- return #[← IOExample.exampleFileSyntax config.type s]
+ IOExample.exampleFileSyntax config.type s
else
- return #[]
+ `(Block.concat #[])
@[block_extension Block.exampleFile]
@@ -404,107 +401,107 @@ def endExample (body : TSyntax `term) : DocElabM (TSyntax `term) := do
`(let $leanCodeName : Highlighted := $(quote hlLean)
$body)
+section
+variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
+
structure Config where
tag : Option String := none
«show» : Bool := true
-def Config.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m Config :=
+def Config.parse : ArgParse m Config :=
Config.mk <$> .named `tag .string true <*> ((·.getD true) <$> .named `show .bool true)
+instance : FromArgs Config m := ⟨Config.parse⟩
+
structure FileConfig extends Config where
name : String
-def FileConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m FileConfig :=
+def FileConfig.parse : ArgParse m FileConfig :=
FileConfig.mk <$> Config.parse <*> .positional `name .string
+instance : FromArgs FileConfig m := ⟨FileConfig.parse⟩
+
+end
+
end IOExample
open IOExample in
-@[code_block_expander inputFile]
-def inputFile : CodeBlockExpander
- | args, str => do
- let opts ← FileConfig.parse.run args
+@[code_block]
+def inputFile : CodeBlockExpanderOf FileConfig
+ | opts, str => do
saveInputFile opts.name str
-- The quote step here is to prevent the editor from showing document AST internals when the
-- cursor is on the code block
if opts.show then
- pure #[← exampleFileSyntax (.input opts.name) str.getString]
+ exampleFileSyntax (.input opts.name) str.getString
else
- pure #[]
+ ``(Block.concat #[])
open IOExample in
-@[code_block_expander outputFile]
-def outputFile : CodeBlockExpander
- | args, str => do
- let opts ← FileConfig.parse.run args
+@[code_block]
+def outputFile : CodeBlockExpanderOf FileConfig
+ | opts, str => do
saveOutputFile opts.name str
-- The quote step here is to prevent the editor from showing document AST internals when the
-- cursor is on the code block
if opts.show then
- pure #[← exampleFileSyntax (.output opts.name) str.getString]
+ exampleFileSyntax (.output opts.name) str.getString
else
- pure #[]
+ ``(Block.concat #[])
open IOExample in
-@[code_block_expander stdin]
-def stdin : CodeBlockExpander
- | args, str => do
- let opts ← Config.parse.run args
+@[code_block]
+def stdin : CodeBlockExpanderOf Config
+ | opts, str => do
saveStdin str
-- The quote step here is to prevent the editor from showing document AST internals when the
-- cursor is on the code block
if opts.show then
- pure #[← exampleFileSyntax .stdin str.getString]
+ exampleFileSyntax .stdin str.getString
else
- pure #[]
+ ``(Block.concat #[])
open IOExample in
-@[code_block_expander stdout]
-def stdout : CodeBlockExpander
- | args, str => do
- let opts ← Config.parse.run args
+@[code_block]
+def stdout : CodeBlockExpanderOf Config
+ | opts, str => do
saveStdout str
-- The quote step here is to prevent the editor from showing document AST internals when the
-- cursor is on the code block
if opts.show then
- pure #[← exampleFileSyntax .stdout str.getString]
+ exampleFileSyntax .stdout str.getString
else
- pure #[]
+ ``(Block.concat #[])
open IOExample in
-@[code_block_expander stderr]
-def stderr : CodeBlockExpander
- | args, str => do
- let opts ← Config.parse.run args
+@[code_block]
+def stderr : CodeBlockExpanderOf Config
+ | opts, str => do
saveStderr str
-- The quote step here is to prevent the editor from showing document AST internals when the
-- cursor is on the code block
if opts.show then
- pure #[← exampleFileSyntax .stderr str.getString]
+ exampleFileSyntax .stderr str.getString
else
- pure #[]
+ ``(Block.concat #[])
open IOExample in
-@[code_block_expander ioLean]
-def ioLean : CodeBlockExpander
- | args, str => do
- let opts ← Config.parse.run args
+@[code_block]
+def ioLean : CodeBlockExpanderOf Config
+ | opts, str => do
let x ← saveLeanCode str
if opts.show then
let range := Syntax.getRange? str
let range := range.map (← getFileMap).utf8RangeToLspRange
- pure #[← ``(Block.other (Block.lean $x (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])]
+ ``(Block.other (Block.lean $x (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])
else
- pure #[]
-
+ ``(Block.concat #[])
open IOExample in
-@[directive_expander ioExample]
-def ioExample : DirectiveExpander
- | args, blocks => do
- ArgParse.done.run args
+@[directive ioExample]
+def ioExample : DirectiveExpanderOf Unit
+ | (), blocks => do
startExample
let body ← blocks.mapM elabBlock
- let body' ← `(Verso.Doc.Block.concat #[$body,*]) >>= endExample
- pure #[body']
+ ``(Verso.Doc.Block.concat #[$body,*]) >>= endExample
diff --git a/src/verso-manual/VersoManual/InlineLean/Option.lean b/src/verso-manual/VersoManual/InlineLean/Option.lean
index 8b932c786..44c49d4b1 100644
--- a/src/verso-manual/VersoManual/InlineLean/Option.lean
+++ b/src/verso-manual/VersoManual/InlineLean/Option.lean
@@ -17,10 +17,9 @@ namespace Verso.Genre.Manual.InlineLean
def Inline.option : Inline where
-@[role_expander option]
-def option : RoleExpander
- | args, inlines => withoutAsync do
- let () ← ArgParse.done.run args
+@[role]
+def option : RoleExpanderOf Unit
+ | (), inlines => withoutAsync do
let #[arg] := inlines
| throwError "Expected exactly one argument"
let `(inline|code( $optName:str )) := arg
@@ -29,7 +28,7 @@ def option : RoleExpander
let optDecl ← getOptionDecl optName
let hl : Highlighted := optTok optName optDecl.declName optDecl.descr
- pure #[← `(Inline.other {Inline.option with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote optName.toString)])]
+ `(Inline.other {Inline.option with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote optName.toString)])
where
optTok (name declName : Name) (descr : String) : Highlighted :=
.token ⟨.option name declName descr , name.toString⟩
diff --git a/src/verso-manual/VersoManual/InlineLean/Signature.lean b/src/verso-manual/VersoManual/InlineLean/Signature.lean
index acb4f1ef5..c48527dd4 100644
--- a/src/verso-manual/VersoManual/InlineLean/Signature.lean
+++ b/src/verso-manual/VersoManual/InlineLean/Signature.lean
@@ -47,15 +47,21 @@ syntax ("def" <|> "theorem")? declId declSig : signature_spec
structure SignatureConfig where
«show» : Bool := true
-def SignatureConfig.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgParse m SignatureConfig :=
+section
+
+variable [Monad m] [MonadError m] [MonadLiftT CoreM m]
+
+def SignatureConfig.parse : ArgParse m SignatureConfig :=
SignatureConfig.mk <$>
((·.getD true) <$> .named `show .bool true)
+instance : FromArgs SignatureConfig m where
+ fromArgs := SignatureConfig.parse
+end
-@[code_block_expander signature]
-def signature : CodeBlockExpander
- | args, str => withoutAsync do
- let {«show»} ← SignatureConfig.parse.run args
+@[code_block]
+def signature : CodeBlockExpanderOf SignatureConfig
+ | {«show»}, str => withoutAsync do
let altStr ← parserInputString str
let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
@@ -93,6 +99,6 @@ def signature : CodeBlockExpander
else hls
if «show» then
- pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])]
+ `(Block.other {Block.signature with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])
else
- pure #[]
+ ``(Block.concat #[])
diff --git a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
index 215d08d63..da64f3aa6 100644
--- a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
+++ b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
@@ -120,18 +120,24 @@ structure SyntaxErrorConfig where
category : Name := `command
prec : Nat := 0
-def SyntaxErrorConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m SyntaxErrorConfig :=
+section
+variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
+
+def SyntaxErrorConfig.parse : ArgParse m SyntaxErrorConfig :=
SyntaxErrorConfig.mk <$>
- .positional `name (ValDesc.name.as m!"name for later reference") <*>
+ .positional `name (ValDesc.name.as "name for later reference") <*>
.namedD `show .bool true <*>
- .namedD `category (ValDesc.name.as m!"syntax category (default 'command')") `command <*>
+ .namedD `category (ValDesc.name.as "syntax category (default `command`)") `command <*>
.namedD `precedence .nat 0
+instance : FromArgs SyntaxErrorConfig m := ⟨SyntaxErrorConfig.parse⟩
+
+end
+
open Lean.Parser in
-@[code_block_expander syntaxError]
-def syntaxError : CodeBlockExpander
- | args, str => withoutAsync do
- let config ← SyntaxErrorConfig.parse.run args
+@[code_block]
+def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig
+ | config, str => withoutAsync do
PointOfInterest.save (← getRef) config.name.toString
(kind := Lsp.SymbolKind.file)
@@ -148,7 +154,7 @@ def syntaxError : CodeBlockExpander
saveOutputs config.name msgs
Hover.addCustomHover (← getRef) <| MessageData.joinSep (msgs.map fun ⟨sev, msg⟩ => m!"{sevStr sev.toSeverity}:{indentD msg.toString}") Format.line
- return #[← `(Block.other {Block.syntaxError with data := ToJson.toJson ($(quote s), $(quote es))} #[Block.code $(quote s)])]
+ `(Block.other {Block.syntaxError with data := ToJson.toJson ($(quote s), $(quote es))} #[Block.code $(quote s)])
where
sevStr : MessageSeverity → String
| .information => "info"
diff --git a/src/verso-manual/VersoManual/License.lean b/src/verso-manual/VersoManual/License.lean
index 10d18dedd..87087246c 100644
--- a/src/verso-manual/VersoManual/License.lean
+++ b/src/verso-manual/VersoManual/License.lean
@@ -260,10 +260,6 @@ block_extension Block.licenseInfo where
return allLicenses.map (·.toHtml headerLevel)
-@[block_role_expander licenseInfo]
-def licenseInfo : BlockRoleExpander
- | args, contents => do
- if let some first := contents[0]? then
- throwErrorAt first "Unexpected contents"
- ArgParse.done.run args
- return #[← ``(Block.other Block.licenseInfo #[])]
+@[block_command]
+def licenseInfo : BlockCommandOf Unit
+ | () => ``(Block.other Block.licenseInfo #[])
diff --git a/src/verso-manual/VersoManual/Marginalia.lean b/src/verso-manual/VersoManual/Marginalia.lean
index 1aeca27d5..211cc4046 100644
--- a/src/verso-manual/VersoManual/Marginalia.lean
+++ b/src/verso-manual/VersoManual/Marginalia.lean
@@ -105,9 +105,8 @@ inline_extension Inline.margin where
some <| fun goI _ _ content => do
Marginalia.html <$> content.mapM goI
-@[role_expander margin]
-def margin : RoleExpander
- | args, inlines => do
- ArgParse.done.run args
+@[role]
+def margin : RoleExpanderOf Unit
+ | (), inlines => do
let content ← inlines.mapM elabInline
- pure #[← ``(Doc.Inline.other Inline.margin #[$content,*])]
+ ``(Doc.Inline.other Inline.margin #[$content,*])
diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean
index ce262d939..ad2b32786 100644
--- a/src/verso-manual/VersoManual/Table.lean
+++ b/src/verso-manual/VersoManual/Table.lean
@@ -132,12 +132,15 @@ table.tabular td > p:last-child, table.tabular th > p:first-child {
"##
]
+section
+variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m]
-def TableConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] : ArgParse m TableConfig :=
+def TableConfig.parse : ArgParse m TableConfig :=
TableConfig.mk <$> .named `tag .string true <*> ((·.getD false) <$> .named `header .bool true) <*> .named `align alignment true
where
alignment := {
description := "Alignment of the table ('left', 'right', or 'center')"
+ signature := .Ident
get
| .name x =>
match x.getId with
@@ -146,13 +149,15 @@ where
| `center => pure .center
| _ => throwErrorAt x "Expected 'left', 'right', or 'center'"
| .num x | .str x => throwErrorAt x "Expected 'left', 'right', or 'center'"
-
}
-@[directive_expander table]
-def table : DirectiveExpander
- | args, contents => do
- let cfg ← TableConfig.parse.run args
+instance : FromArgs TableConfig m := ⟨TableConfig.parse⟩
+
+end
+
+@[directive]
+def table : DirectiveExpanderOf TableConfig
+ | cfg, contents => do
-- The table should be a list of lists. Extract them!
let #[oneBlock] := contents
| throwError "Expected a single unordered list"
@@ -172,11 +177,12 @@ def table : DirectiveExpander
if columns = 0 then
throwErrorAt oneBlock "Expected at least one column"
if rows.any (·.size != columns) then
+
throwErrorAt oneBlock s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
let flattened := rows.flatten
let blocks : Array (Syntax.TSepArray `term ",") ← flattened.mapM (·.mapM elabBlock)
- pure #[← ``(Block.other (Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])]
+ ``(Block.other (Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
where
getLi
diff --git a/src/verso/Verso/Code/External.lean b/src/verso/Verso/Code/External.lean
index 72479b88e..a776a3edb 100644
--- a/src/verso/Verso/Code/External.lean
+++ b/src/verso/Verso/Code/External.lean
@@ -107,7 +107,7 @@ Parses the project directory as a named argument `project`, falling back to the
def projectOrDefault : ArgParse m StrLit :=
.named `project .strLit false <|>
(Syntax.mkStrLit <$> .lift "default project" defaultProject) <|>
- .fail none (some m!"No `(project := ...)` argument provided and no default project set.")
+ .fail none (some "No `(project := ...)` argument provided and no default project set.")
/--
Parses the current module as a named argument `module`, falling back to the default if specified in the option `verso.exampleModule`.
@@ -115,7 +115,7 @@ Parses the current module as a named argument `module`, falling back to the defa
def moduleOrDefault : ArgParse m Ident :=
.named `module .ident false <|>
(mkIdent <$> .lift "default module" defaultModule) <|>
- .fail none (some m!"No `(module := ...)` argument provided and no default module set.")
+ .fail none (some "No `(module := ...)` argument provided and no default module set.")
/--
A specification of which module to look in to find example code.
diff --git a/src/verso/Verso/Doc/ArgParse.lean b/src/verso/Verso/Doc/ArgParse.lean
index dfb02f920..39e5f820d 100644
--- a/src/verso/Verso/Doc/ArgParse.lean
+++ b/src/verso/Verso/Doc/ArgParse.lean
@@ -21,10 +21,87 @@ section
variable (m) [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m]
+
+inductive SigDoc where
+ | text (str : String)
+ | name (name : Name)
+ | append (d1 d2 : SigDoc)
+
+instance : Append SigDoc := ⟨.append⟩
+
+instance : Coe String SigDoc := ⟨.text⟩
+
+instance : Coe Name SigDoc := ⟨.name⟩
+
+def SigDoc.toMessageData : SigDoc → MessageData
+ | .text s => s
+ | .append x y => x.toMessageData ++ y.toMessageData
+ | .name x => x
+
+instance : ToMessageData SigDoc where
+ toMessageData x := x.toMessageData
+
+def SigDoc.toString {m} [Monad m] [MonadResolveName m] [MonadEnv m] : SigDoc → m String
+ | .text s => pure s
+ | .name x => do
+ let x ← unresolveNameGlobal x
+ pure x.toString
+ | .append d1 d2 => do
+ return (← d1.toString) ++ (← d2.toString)
+
+elab "doc!" s:interpolatedStr(ident) : term => do
+ let mut out ← Meta.mkAppM ``SigDoc.text #[toExpr ""]
+ for part in s.raw.getArgs do
+ if let some str := part.isInterpolatedStrLit? then
+ out ← Meta.mkAppM ``SigDoc.append #[out, ← Meta.mkAppM ``SigDoc.text #[toExpr str]]
+ else if part.getKind == identKind then
+ let x ← realizeGlobalConstNoOverloadWithInfo part
+ out ← Meta.mkAppM ``SigDoc.append #[out, ← Meta.mkAppM ``SigDoc.name #[toExpr x]]
+ else
+ throwErrorAt part "Didn't understand"
+ return out
+
+structure CanMatch where
+ ident : Bool
+ string : Bool
+ num : Bool
+
+def CanMatch.toString (m : CanMatch) : String :=
+ let s :=
+ (if m.ident then ["Ident"] else []) ++
+ (if m.string then ["String"] else []) ++
+ (if m.num then ["Num"] else []) |> String.intercalate " | "
+ if s.isEmpty then "∅" else s
+
+def CanMatch.format (m : CanMatch) : Std.Format :=
+ let sep : Std.Format := .text " |" ++ .line
+ let s :=
+ (if m.ident then ["Ident"] else []) ++
+ (if m.string then ["String"] else []) ++
+ (if m.num then ["Num"] else [])
+ if s.isEmpty then "∅" else .group (sep.joinSep s)
+
+instance : ToString CanMatch := ⟨CanMatch.toString⟩
+
+def CanMatch.Ident : CanMatch := { ident := true, string := false, num := false }
+def CanMatch.String : CanMatch := { ident := false, string := true, num := false }
+def CanMatch.Num : CanMatch := { ident := false, string := false, num := true }
+
+instance : Union CanMatch where
+ union a b := {
+ ident := a.ident || b.ident,
+ string := a.string || b.string,
+ num := a.num || b.num
+ }
+
structure ValDesc (α) where
- description : MessageData
+ description : SigDoc
+ signature : CanMatch
get : ArgVal → m α
+instance [Functor m] : Functor (ValDesc m) where
+ map f d := { d with get := fun v => f <$> d.get v }
+
/--
A canonical way to convert a Verso argument into a given type.
-/
@@ -33,18 +110,52 @@ class FromArgVal (α : Type) (m : Type → Type) where
export FromArgVal (fromArgVal)
+/--
+A parser for arguments in some underlying monad.
+-/
inductive ArgParse (m : Type → Type) : Type → Type 1 where
- | fail (stx? : Option Syntax) (message? : Option MessageData) : ArgParse m α
+ /--
+ Fails with the provided error message.
+ -/
+ | fail (stx? : Option Syntax) (message? : Option SigDoc) : ArgParse m α
+ /--
+ Returns a value without parsing any arguments.
+ -/
| pure (val : α) : ArgParse m α
+ /--
+ Provides an argument value by lifting an action from the underlying monad.
+ -/
| lift (desc : String) (act : m α) : ArgParse m α
- | positional (nameHint : Name) (val : ValDesc m α) (doc? : Option MessageData := none) :
+ /--
+ Matches a positional argument.
+ -/
+ | positional (nameHint : Name) (val : ValDesc m α) (doc? : Option SigDoc := none) :
ArgParse m α
- | named (name : Name) (val : ValDesc m α) (optional : Bool) (doc? : Option MessageData := none) :
+ /--
+ Matches an argument with the provided name.
+ -/
+ | named (name : Name) (val : ValDesc m α) (optional : Bool) (doc? : Option SigDoc := none) :
ArgParse m (if optional then Option α else α)
- | anyNamed (name : Name) (val : ValDesc m α) (doc? : Option MessageData := none) : ArgParse m (Ident × α)
+ /--
+ Matches any named argument.
+ -/
+ | anyNamed (name : Name) (val : ValDesc m α) (doc? : Option SigDoc := none) : ArgParse m (Ident × α)
+ /--
+ No further arguments are allowed.
+ -/
| done : ArgParse m Unit
+ /--
+ Error recovery.
+ -/
| orElse (p1 : ArgParse m α) (p2 : Unit → ArgParse m α) : ArgParse m α
+ /--
+ The sequencing operation of an applicative functor.
+ -/
| seq (p1 : ArgParse m (α → β)) (p2 : Unit → ArgParse m α) : ArgParse m β
+ /--
+ Zero or more repetitions.
+ -/
+ | many : ArgParse m α → ArgParse m (List α)
/-- Returns all remaining arguments. This is useful for consuming some, then forwarding the rest. -/
| remaining : ArgParse m (Array Arg)
@@ -56,16 +167,18 @@ class FromArgs (α : Type) (m : Type → Type) where
export FromArgs (fromArgs)
-def ArgParse.positional' {m} [FromArgVal α m] (nameHint : Name) (doc? : Option MessageData := none) : ArgParse m α :=
+instance : FromArgs Unit m := ⟨.pure ()⟩
+
+def ArgParse.positional' {m} [FromArgVal α m] (nameHint : Name) (doc? : Option SigDoc := none) : ArgParse m α :=
.positional nameHint fromArgVal (doc? := doc?)
def ArgParse.named' {m} [FromArgVal α m]
- (name : Name) (optional : Bool) (doc? : Option MessageData := none) :
+ (name : Name) (optional : Bool) (doc? : Option SigDoc := none) :
ArgParse m (if optional then Option α else α) :=
.named name fromArgVal optional (doc? := doc?)
def ArgParse.anyNamed' {m} [FromArgVal α m]
- (name : Name) (doc? : Option MessageData := none) :
+ (name : Name) (doc? : Option SigDoc := none) :
ArgParse m (Ident × α) :=
.anyNamed name fromArgVal (doc? := doc?)
@@ -87,18 +200,118 @@ def ArgParse.namedD {m} (name : Name) (val : ValDesc m α) (default : α) : ArgP
def ArgParse.namedD' {m} [FromArgVal α m] (name : Name) (default : α) : ArgParse m α :=
namedD name fromArgVal default
-def ArgParse.describe : ArgParse m α → MessageData
+def ArgParse.describe : ArgParse m α → SigDoc
| .fail _ msg? => msg?.getD "Cannot succeed"
| .pure x => "No arguments expected"
| .lift desc act => desc
| .positional _x v _ => v.description
- | .named x v opt _ => if opt then "[" else "" ++ m!"{x} : {v.description}" ++ if opt then "]" else ""
+ | .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
| .done => "no arguments remaining"
| .orElse p1 p2 => p1.describe ++ " or " ++ (p2 ()).describe
| .seq p1 p2 => p1.describe ++ " then " ++ (p2 ()).describe
+ | .many p => "zero or more " ++ p.describe
| .remaining => "any arguments"
+structure SimpleDesc where
+ positional : Array (Name × CanMatch × SigDoc) := {}
+ byName : Array (Name × CanMatch × Bool × SigDoc) := {}
+ keyVals : Option (Name × CanMatch × SigDoc) := none
+
+def toSimpleDesc {m} (p : ArgParse m α) : Option SimpleDesc :=
+ go p |>.run {} |>.map (·.snd)
+where
+ go {α} : ArgParse m α → StateT SimpleDesc Option Unit
+ | .fail _ msg? => failure
+ | .pure x | .done => pure ()
+ | .lift .. | .orElse .. => failure
+ | .positional x v doc? =>
+ modify fun sd => { sd with positional := sd.positional.push (x, v.signature, doc?.getD v.description) }
+ | .named x v opt doc? =>
+ modify fun sd => { sd with byName := sd.byName.push (x, v.signature, opt, doc?.getD v.description)}
+ | .anyNamed x v doc? | .many (.anyNamed x v doc?) => do
+ if (← get).keyVals.isNone then
+ modify fun sd => { sd with keyVals := some (x, v.signature, doc?.getD v.description) }
+ else failure
+ | .seq p1 p2 => do
+ go p1
+ go (p2 ())
+ | .many p => failure
+ | .remaining => failure
+
+
+def SimpleDesc.markdown (d : SimpleDesc) : SigDoc :=
+ let {positional, byName, keyVals} := d
+ if positional.isEmpty && byName.isEmpty && keyVals.isNone then
+ "No parameters"
+ else
+ posList positional ++ nameList byName ++ kv keyVals
+where
+ posList (pos : Array (Name × CanMatch × SigDoc)) : SigDoc :=
+ if pos.isEmpty then ""
+ else if let #[(x, t, doc)] := pos then
+ doc!"Positional: `" ++ x.toString ++ " : " ++ t.toString ++ " — " ++ doc ++ "`\n\n"
+ else
+ let args :=
+ pos.foldl (init := doc!"Positional:\n") fun s (x, t, doc) =>
+ s ++ doc!"* `" ++ .text x.toString ++ " : " ++ t.toString ++ "` — " ++ doc ++ "\n"
+ args ++ "\n"
+ nameList (ns : Array (Name × CanMatch × Bool × SigDoc)) : SigDoc :=
+ if ns.isEmpty then ""
+ else if let #[(x, t, opt, doc)] := ns then
+ doc!"Named: `" ++ .text x.toString ++ " : " ++ t.toString ++ "` (" ++
+ (if opt then "optional" else "required") ++ doc!") — " ++ doc ++ "\n\n"
+ else
+ let args :=
+ ns.foldl (init := doc!"Named:\n") fun s (x, t, opt, doc) =>
+ s ++ doc!"* `" ++ x.toString ++ " : " ++ t.toString ++
+ "` (" ++ (if opt then "optional" else "required") ++ ") — " ++ doc ++ "\n"
+ args ++ "\n"
+ kv : Option (Name × CanMatch × SigDoc) → SigDoc
+ | none => ""
+ | some (x, t, doc) =>
+ doc!"Dictionary: `" ++ x.toString ++ "`, saving names of `" ++ t.toString ++ "` — " ++ doc
+
+def ArgParse.signature' {m} (prec : Nat) (p : ArgParse m α) : Option Std.Format :=
+ match p with
+ | .fail _ msg? => failure
+ | .pure x | .done => do return .nil
+ | .lift desc act => do return desc
+ | .positional x v _ => do return s!"{x} :" ++ .line ++ (← v.signature.format)
+ | .named x v opt _ => do
+ let d := v.signature.format
+ let s := .group <| .nest 2 <| .text s!"{x} :" ++ .line ++ d
+ return withParen 2 <| if opt then "(" ++ s ++ ")?" else s
+ | .anyNamed x v _ => do
+ let d := v.signature.format
+ let s := .group <| .nest 2 <| .text s!"{x} :" ++ .line ++ d ++ .line ++ "(key/value)"
+ return withParen 2 s
+ | .orElse p1 p2 => do
+ let s1 := p1.signature' 2
+ let s2 := (p2 ()).signature' 3
+ match s1, s2 with
+ | some s1, some s2 =>
+ return .group <| s1 ++ " <|>" ++ .line ++ s2
+ | some s, none | none, some s => return s
+ | none, none => failure
+ | .seq p1 p2 => do
+ let s1 ← p1.signature' 2
+ let s2 ← (p2 ()).signature' 2
+ if s1.isEmpty then return s2
+ else if s2.isEmpty then return s1
+ else return s1 ++ .line ++ s2
+ | .many p => do return (← p.signature' 1) ++ "*"
+ | .remaining => return "any"
+where
+ withParen p (x : Std.Format) : Std.Format := if p > prec then "(" ++ x ++ ")" else x
+
+def ArgParse.signature {m} (p : ArgParse m α) : Option SigDoc :=
+ if let some sd := toSimpleDesc p then
+ some sd.markdown
+ else if let some s := p.signature' 0 then
+ some <| doc!"```\n" ++ s.pretty 40 ++ doc!"\n```\n"
+ else none
+
scoped instance [Monad m] [MonadError m] : MonadError (StateT σ m) where
throw e := fun _ => throw e
tryCatch act handler := fun st => tryCatch (act st) (fun e => handler e st)
@@ -120,7 +333,7 @@ instance : ToMessageData Arg where
structure ParseState where
remaining : Array Arg
- info : Array (Syntax × Name × MessageData)
+ info : Array (Syntax × Name × SigDoc)
private def firstOriginal (stxs : Array Syntax) : Syntax := Id.run do
for stx in stxs do
@@ -128,11 +341,11 @@ private def firstOriginal (stxs : Array Syntax) : Syntax := Id.run do
return .missing
-- NB the order of ExceptT and StateT is important here
-def ArgParse.parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (StateT ParseState m) α
+partial def ArgParse.parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (StateT ParseState m) α
| .fail stx? msg? => do
let stx ← stx?.getDM getRef
let msg := msg?.getD "failed"
- throw ((← get).remaining, .error stx msg)
+ throw ((← get).remaining, .error stx msg.toMessageData)
| .pure x => Pure.pure x
| .lift desc act => act
| .positional x vp doc? => do
@@ -221,6 +434,13 @@ def ArgParse.parseArgs : ArgParse m α → ExceptT (Array Arg × Exception) (Sta
| e2@(args2, _) =>
if args2.size < args1.size then throw e1 else throw e2
| .seq p1 p2 => Seq.seq p1.parseArgs (fun () => p2 () |>.parseArgs)
+ | .many p => do
+ let x ←
+ try
+ p.parseArgs
+ catch | _ => return []
+ let xs ← many p |>.parseArgs
+ return (x :: xs)
| .remaining => modifyGet fun s =>
let r := s.remaining
(r, {s with remaining := #[]})
@@ -240,7 +460,8 @@ end
variable {m} [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] [MonadLiftT CoreM m]
def ValDesc.bool : ValDesc m Bool where
- description := m!"{true} or {false}"
+ description := doc!"{true} or {false}"
+ signature := .Ident
get
| .name b => do
let b' ← liftM <| realizeGlobalConstNoOverloadWithInfo b
@@ -253,7 +474,8 @@ instance : FromArgVal Bool m where
fromArgVal := .bool
def ValDesc.string : ValDesc m String where
- description := m!"a string"
+ description := doc!"a string"
+ signature := .String
get
| .str s => pure s.getString
| other => throwError "Expected string, got {toMessageData other}"
@@ -262,7 +484,8 @@ instance : FromArgVal String m where
fromArgVal := .string
def ValDesc.ident : ValDesc m Ident where
- description := m!"an identifier"
+ description := doc!"an identifier"
+ signature := .Ident
get
| .name x => pure x
| other => throwError "Expected identifier, got { toMessageData other}"
@@ -276,7 +499,8 @@ Parses a name as an argument value.
The name is returned without macro scopes.
-/
def ValDesc.name : ValDesc m Name where
- description := m!"a name"
+ description := doc!"a name"
+ signature := .Ident
get
| .name x => pure x.getId.eraseMacroScopes
| other => throwError "Expected identifier, got {other}"
@@ -285,20 +509,22 @@ instance : FromArgVal Name m where
fromArgVal := .name
def ValDesc.resolvedName : ValDesc m Name where
- description := m!"a resolved name"
+ description := doc!"a resolved name"
+ signature := .Ident
get
| .name x => realizeGlobalConstNoOverloadWithInfo x
| other => throwError "Expected identifier, got {other}"
/-- Associates a new description with a parser for better error messages. -/
-def ValDesc.as (what : MessageData) (desc : ValDesc m α) : ValDesc m α :=
+def ValDesc.as (what : SigDoc) (desc : ValDesc m α) : ValDesc m α :=
{desc with description := what}
/--
Parses a natural number.
-/
def ValDesc.nat : ValDesc m Nat where
- description := m!"a name"
+ description := doc!"a name"
+ signature := .Num
get
| .num n => pure n.getNat
| other => throwError "Expected string, got {repr other}"
@@ -312,7 +538,8 @@ Parses a sequence of Verso inline elements from a string literal. Returns a File
they can be related to their original source.
-/
def ValDesc.inlinesString [MonadFileMap m] : ValDesc m (FileMap × TSyntaxArray `inline) where
- description := m!"a string that contains a sequence of inline elements"
+ description := doc!"a string that contains a sequence of inline elements"
+ signature := .String
get
| .str s => open Lean.Parser in do
let text ← getFileMap
@@ -339,7 +566,8 @@ def ValDesc.inlinesString [MonadFileMap m] : ValDesc m (FileMap × TSyntaxArray
def ValDesc.messageSeverity : ValDesc m MessageSeverity where
description :=
open MessageSeverity in
- m!"The expected severity: '{``error}', '{``warning}', or '{``information}'"
+ doc!"The expected severity: `{error}`, `{warning}`, or `{information}`"
+ signature := .Ident
get := open MessageSeverity in fun
| .name b => do
let b' ← realizeGlobalConstNoOverloadWithInfo b
@@ -356,7 +584,8 @@ open Lean.Elab.Tactic.GuardMsgs in
def ValDesc.whitespaceMode : ValDesc m WhitespaceMode where
description :=
open WhitespaceMode in
- m!"The expected whitespace mode: '{``exact}', '{``normalized}', or '{``lax}'"
+ doc!"The expected whitespace mode: `{exact}`, `{normalized}`, or `{lax}`"
+ signature := .Ident
get := open WhitespaceMode in fun
| .name b => do
let b' ← realizeGlobalConstNoOverloadWithInfo b
@@ -381,6 +610,7 @@ other feedback at the right location.
-/
def ValDesc.withSyntax (desc : ValDesc m α) : ValDesc m (WithSyntax α) where
description := desc.description
+ signature := desc.signature
get v := (WithSyntax.mk · v.syntax) <$> desc.get v
instance [FromArgVal α m] : FromArgVal (WithSyntax α) m where
@@ -390,7 +620,8 @@ instance [FromArgVal α m] : FromArgVal (WithSyntax α) m where
Parses a string literal.
-/
def ValDesc.strLit [Monad m] [MonadError m] : ValDesc m StrLit where
- description := m!"a string"
+ description := doc!"a string"
+ signature := .String
get
| .str s => pure s
| other => throwError "Expected string, got {toMessageData other}"
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index b715fe969..1bfdead38 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -13,6 +13,7 @@ open Lean Elab
open PartElabM
open DocElabM
open Verso.Syntax
+open Verso.ArgParse (SigDoc)
def throwUnexpected [Monad m] [MonadError m] (stx : Syntax) : m α :=
throwErrorAt stx "unexpected syntax{indentD stx}"
@@ -119,6 +120,16 @@ def appFallback
f (.node .none nullKind <| arrArg ++ argStx)
return ⟨appStx⟩
+private def expanderDocHover (stx : Syntax) (what : String) (name : Name) (doc? : Option String) (sig? : Option SigDoc) : DocElabM Unit := do
+ let mut out := s!"{what} `{name}`"
+ if let some sig := sig? then
+
+ out := out ++ "\n\n" ++ (← sig.toString)
+ if let some d := doc? then
+ out := out ++ "\n\n" ++ d
+ Hover.addCustomHover stx out
+
+
open Lean.Parser.Term in
@[inline_expander Verso.Syntax.role]
def _root_.Verso.Syntax.role.expand : InlineExpander
@@ -132,11 +143,13 @@ def _root_.Verso.Syntax.role.expand : InlineExpander
-- If no expanders are registered, then try elaborating just as a
-- function application node
return ← appFallback inline name resolvedName argVals subjects
- for e in exp do
+ for (e, doc?, sig?) in exp do
try
let termStxs ← withFreshMacroScope <| e argVals subjects
+ expanderDocHover name "Role" resolvedName doc? sig?
let termStxs ← termStxs.mapM fun t => (``(($t : Inline $(⟨genre⟩))))
- return (← ``(Inline.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+ if h : termStxs.size = 1 then return termStxs[0]
+ else return (← ``(Inline.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
catch
| ex@(.internal id) =>
if id == unsupportedSyntaxExceptionId then pure ()
@@ -341,46 +354,48 @@ def _root_.Verso.Syntax.metadata_block.command : PartCommand
modifyThe PartElabM.State fun st => {st with partContext.metadata := some stx}
| _ => throwUnsupportedSyntax
-@[part_command Verso.Syntax.block_role]
+@[part_command Verso.Syntax.command]
def includeSection : PartCommand
- | `(block|block_role{include $_args* }[ $content ]) => throwErrorAt content "Unexpected block argument"
- | `(block|block_role{include}) => throwError "Expected an argument"
- | `(block|block_role{include $arg1 $arg2 $arg3 $args*}) => throwErrorAt arg2 "Expected one or two arguments"
- | stx@`(block|block_role{include $args* }) => do
- Hover.addCustomHover stx
- r#"Includes another document at this point in the document.
-
-* `{include NAME}`: Includes the document as a child part.
-* `{include N NAME}`: Includes the document at header level `N`, as if its header had `N` header indicators (`#`) before it.
-"#
- match (← parseArgs args) with
- | #[.anon (.name x)] =>
- let name ← resolved x
- addPart <| .included name
- | #[.anon (.num lvl), .anon (.name x)] =>
- let name ← resolved x
- closePartsUntil lvl.getNat stx.getHeadInfo.getPos!
- addPart <| .included name
- | _ => throwErrorAt stx "Expected exactly one positional argument that is a name"
- | _ => Lean.Elab.throwUnsupportedSyntax
+ | `(block|command{include $args* }) => do
+ if h : args.size = 0 then throwError "Expected an argument"
+ else if h : args.size > 2 then throwErrorAt args[2] "Expected one or two arguments"
+ else
+ let ref ← getRef
+ Hover.addCustomHover ref
+ r#"Includes another document at this point in the document.
+
+ * `{include NAME}`: Includes the document as a child part.
+ * `{include N NAME}`: Includes the document at header level `N`, as if its header had `N` header indicators (`#`) before it.
+ "#
+ match (← parseArgs args) with
+ | #[.anon (.name x)] =>
+ let name ← resolved x
+ addPart <| .included name
+ | #[.anon (.num lvl), .anon (.name x)] =>
+ let name ← resolved x
+ closePartsUntil lvl.getNat ref.getHeadInfo.getPos!
+ addPart <| .included name
+ | _ => throwErrorAt ref "Expected exactly one positional argument that is a name"
+ | _ => (Lean.Elab.throwUnsupportedSyntax : PartElabM Unit)
where
resolved id := mkIdentFrom id <$> realizeGlobalConstNoOverloadWithInfo (mkIdentFrom id (docName id.getId))
-@[block_expander Verso.Syntax.block_role]
-def _root_.Verso.Syntax.block_role.expand : BlockExpander := fun block =>
+@[block_expander Verso.Syntax.command]
+def _root_.Verso.Syntax.command.expand : BlockExpander := fun block =>
match block with
- | `(block|block_role{$name $args*}) => do
+ | `(block|command{$name $args*}) => do
withTraceNode `Elab.Verso.block (fun _ => pure m!"Block role {name}") <|
withRef block <| withFreshMacroScope <| withIncRecDepth <| do
let ⟨genre, _⟩ ← readThe DocElabContext
let resolvedName ← realizeGlobalConstNoOverloadWithInfo name
- let exp ← blockRoleExpandersFor resolvedName
+ let exp ← blockCommandExpandersFor resolvedName
let argVals ← parseArgs args
if exp.isEmpty then
return ← appFallback block name resolvedName argVals none
- for e in exp do
+ for (e, doc?, sig?) in exp do
try
- let termStxs ← withFreshMacroScope <| e argVals #[]
+ let termStxs ← withFreshMacroScope <| e argVals
+ expanderDocHover name "Command" resolvedName doc? sig?
return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
catch
| ex@(.internal id) =>
@@ -481,21 +496,22 @@ def _root_.Verso.Syntax.blockquote.expand : BlockExpander
@[block_expander Verso.Syntax.codeblock]
def _root_.Verso.Syntax.codeblock.expand : BlockExpander
| `(block|``` $nameStx:ident $argsStx* | $contents:str ```) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
- let name ← realizeGlobalConstNoOverloadWithInfo nameStx
- let exp ← codeBlockExpandersFor name
- -- TODO typed syntax here
- let args ← parseArgs <| argsStx.map (⟨·⟩)
- for e in exp do
- try
- let termStxs ← withFreshMacroScope <| e args contents
- return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
- catch
- | ex@(.internal id) =>
- if id == unsupportedSyntaxExceptionId then pure ()
- else throw ex
- | ex => throw ex
- throwUnsupportedSyntax
+ let ⟨genre, _⟩ ← readThe DocElabContext
+ let name ← realizeGlobalConstNoOverloadWithInfo nameStx
+ let exp ← codeBlockExpandersFor name
+ -- TODO typed syntax here
+ let args ← parseArgs <| argsStx.map (⟨·⟩)
+ for (e, doc?, sig?) in exp do
+ try
+ let termStxs ← withFreshMacroScope <| e args contents
+ expanderDocHover nameStx "Code block" name doc? sig?
+ return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+ throwUnsupportedSyntax
| `(block|``` | $contents:str ```) => do
``(Block.code $(quote contents.getString))
| _ =>
@@ -508,9 +524,10 @@ def _root_.Verso.Syntax.directive.expand : BlockExpander
let name ← realizeGlobalConstNoOverloadWithInfo nameStx
let exp ← directiveExpandersFor name
let args ← parseArgs argsStx
- for e in exp do
+ for (e, doc?, sig?) in exp do
try
let termStxs ← withFreshMacroScope <| e args contents
+ expanderDocHover nameStx "Directive" name doc? sig?
return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
catch
| ex@(.internal id) =>
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index a53137468..b61075934 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -8,8 +8,10 @@ import Std.Data.HashMap
import Std.Data.HashSet
import Lean.Elab.DeclUtil
+import Lean.Meta.Reduce
import Verso.Doc
+import Verso.Doc.ArgParse
import Verso.Doc.Elab.ExpanderAttribute
import Verso.Doc.Elab.InlineString
import Verso.Hover
@@ -22,6 +24,7 @@ open Lean
open Lean.Elab
open Std (HashMap HashSet)
open Verso.SyntaxUtils
+open Verso.ArgParse (FromArgs SigDoc)
initialize registerTraceClass `Elab.Verso
initialize registerTraceClass `Elab.Verso.part
@@ -583,7 +586,22 @@ unsafe def blockExpandersForUnsafe (x : Name) : DocElabM (Array BlockExpander) :
@[implemented_by blockExpandersForUnsafe]
opaque blockExpandersFor (x : Name) : DocElabM (Array BlockExpander)
+initialize expanderSignatureExt : PersistentEnvExtension (Name × SigDoc) (Name × SigDoc) (NameMap SigDoc) ←
+ registerPersistentEnvExtension {
+ mkInitial := pure {},
+ addImportedFn xss :=
+ pure <| xss.foldl (init := {}) fun ns xs =>
+ xs.foldl (init := ns) fun ns (x, s) =>
+ ns.insert x s
+ addEntryFn
+ | xs, (x, y) =>
+ xs.insert x y
+ exportEntriesFn xs :=
+ xs.toArray
+ }
+private def sig (α) [inst : FromArgs α DocElabM] : Option ArgParse.SigDoc :=
+ ArgParse.ArgParse.signature inst.fromArgs
abbrev PartCommand := Syntax → PartElabM Unit
@@ -600,53 +618,377 @@ opaque partCommandsFor (x : Name) : PartElabM (Array PartCommand)
abbrev RoleExpander := Array Arg → TSyntaxArray `inline → DocElabM (Array (TSyntax `term))
+abbrev RoleExpanderOf α := α → TSyntaxArray `inline → DocElabM Term
+
initialize roleExpanderAttr : KeyedDeclsAttribute RoleExpander ←
mkDocExpanderAttribute `role_expander ``RoleExpander "Indicates that this function is used to implement a given role" `roleExpanderAttr
-unsafe def roleExpandersForUnsafe (x : Name) : DocElabM (Array RoleExpander) := do
+private def toRole {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `inline → DocElabM Term) : RoleExpander :=
+ fun args inlines => do
+ let v ← ArgParse.parse args
+ return #[← expander v inlines]
+
+syntax (name := role) "role " (ident)? : attr
+
+
+initialize roleExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+ registerPersistentEnvExtension {
+ mkInitial := pure {},
+ addImportedFn xss :=
+ pure <| xss.foldl (init := {}) fun ns xs =>
+ xs.foldl (init := ns) fun ns (x, ys) =>
+ ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+ addEntryFn
+ | xs, (x, y) =>
+ xs.insert x (xs.find? x |>.getD #[] |>.push y)
+ exportEntriesFn xs :=
+ xs.toArray
+ }
+
+private unsafe def roleExpandersForUnsafe' (x : Name) : DocElabM (Array (RoleExpander × Option String × Option SigDoc)) := do
+ let expanders := roleExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+ expanders.mapM fun n => do
+ let e ← evalConst RoleExpander n
+ let doc? ← findDocString? (← getEnv) n
+ let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+ return (e, doc?, sig)
+
+private unsafe def roleExpandersForUnsafe'' (x : Name) : DocElabM (Array RoleExpander) := do
let expanders := roleExpanderAttr.getEntries (← getEnv) x
return expanders.map (·.value) |>.toArray
+private unsafe def roleExpandersForUnsafe (x : Name) : DocElabM (Array (RoleExpander × Option String × Option SigDoc)) := do
+ return (← roleExpandersForUnsafe' x) ++ (← roleExpandersForUnsafe'' x).map (·, none, none)
+
@[implemented_by roleExpandersForUnsafe]
-opaque roleExpandersFor (x : Name) : DocElabM (Array RoleExpander)
+opaque roleExpandersFor (x : Name) : DocElabM (Array (RoleExpander × Option String × Option SigDoc))
+
+private unsafe def evalIOOptStringUnsafe (x : Name) : MetaM (Option SigDoc) := do
+ evalConst (Option SigDoc) x
+
+@[implemented_by evalIOOptStringUnsafe]
+private opaque evalOptMsg (x : Name) : MetaM (Option SigDoc)
+
+private def saveSignature (expanderName : Name) (argTy : Expr) : MetaM Unit := do
+ let s ← Meta.mkAppM ``sig #[argTy]
+ let inst ← Meta.synthInstance (mkApp2 (.const ``FromArgs []) argTy (.const ``DocElabM []))
+ let s := .app s inst
+ let s ← instantiateExprMVars s
+ let s ← Meta.whnf s
+ let name ← mkFreshUserName <| expanderName ++ `signature
+ addAndCompile <| .defnDecl {
+ name,
+ levelParams := [],
+ type := .app (.const ``Option [0]) (.const ``SigDoc []),
+ value := s,
+ hints := .opaque,
+ safety := .safe
+ }
+ let str? ← evalOptMsg name
+ if let some str := str? then
+ modifyEnv (expanderSignatureExt.addEntry · (expanderName, str))
+
+unsafe initialize registerBuiltinAttribute {
+ name := `role,
+ descr := "Define a new role",
+ applicationTime := .afterCompilation,
+ add declName stx k := do
+ unless k == .global do throwError m!"Must be `global`"
+ let roleName ←
+ match stx with
+ | `(attr|role) => pure declName
+ | `(attr|role $x) => realizeGlobalConstNoOverloadWithInfo x
+ | _ => throwError "Invalid `role` attribute"
+
+ let n ← mkFreshUserName <| declName ++ `role
+
+ let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do
+ let e ← Meta.mkAppM ``toRole #[.const declName []]
+ let e ← instantiateMVars e
+ let t ← Meta.inferType e
+
+
+ match_expr e with
+ | toRole ty _ _ => saveSignature n ty
+ | _ => pure ()
+
+ pure (e, t)
+
+ addAndCompile <| .defnDecl {
+ name := n,
+ levelParams := [],
+ type := t,
+ value := e,
+ hints := .opaque,
+ safety := .safe
+ }
+
+ addDocStringCore' n (← findSimpleDocString? (← getEnv) declName)
+
+ modifyEnv fun env =>
+ roleExpanderExt.addEntry env (roleName, n)
+}
abbrev CodeBlockExpander := Array Arg → TSyntax `str → DocElabM (Array (TSyntax `term))
+abbrev CodeBlockExpanderOf α := α → StrLit → DocElabM Term
+
+
initialize codeBlockExpanderAttr : KeyedDeclsAttribute CodeBlockExpander ←
mkDocExpanderAttribute `code_block_expander ``CodeBlockExpander "Indicates that this function is used to implement a given code block" `codeBlockExpanderAttr
-unsafe def codeBlockExpandersForUnsafe (x : Name) : DocElabM (Array CodeBlockExpander) := do
+private def toCodeBlock {α : Type} [FromArgs α DocElabM] (expander : α → StrLit → DocElabM Term) : CodeBlockExpander :=
+ fun args str => do
+ let v ← ArgParse.parse args
+ return #[← expander v str]
+
+syntax (name := code_block) "code_block " (ident)? : attr
+
+initialize codeBlockExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+ registerPersistentEnvExtension {
+ mkInitial := pure {},
+ addImportedFn xss :=
+ pure <| xss.foldl (init := {}) fun ns xs =>
+ xs.foldl (init := ns) fun ns (x, ys) =>
+ ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+ addEntryFn
+ | xs, (x, y) =>
+ xs.insert x (xs.find? x |>.getD #[] |>.push y)
+ exportEntriesFn xs :=
+ xs.toArray
+ }
+
+unsafe initialize registerBuiltinAttribute {
+ name := `code_block,
+ descr := "Define a new code_block",
+ applicationTime := .afterCompilation,
+ add declName stx k := do
+ unless k == .global do throwError m!"Must be `global`"
+ let blockName ←
+ match stx with
+ | `(attr|code_block) => pure declName
+ | `(attr|code_block $x) => realizeGlobalConstNoOverloadWithInfo x
+ | _ => throwError "Invalid `code_block` attribute"
+
+ let n ← mkFreshUserName <| declName ++ `code_block
+
+ let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do
+ let e ← Meta.mkAppM ``toCodeBlock #[.const declName []]
+ let e ← instantiateMVars e
+ let t ← Meta.inferType e
+
+
+ match_expr e with
+ | toCodeBlock ty _ _ => saveSignature n ty
+ | _ => pure ()
+
+ pure (e, t)
+
+ addAndCompile <| .defnDecl {
+ name := n,
+ levelParams := [],
+ type := t,
+ value := e,
+ hints := .opaque,
+ safety := .safe
+ }
+
+ addDocStringCore' n (← findSimpleDocString? (← getEnv) declName)
+
+ modifyEnv fun env =>
+ codeBlockExpanderExt.addEntry env (blockName, n)
+}
+
+private unsafe def codeBlockExpandersForUnsafe' (x : Name) : DocElabM (Array (CodeBlockExpander × Option String × Option SigDoc)) := do
+ let expanders := codeBlockExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+ expanders.mapM fun n => do
+ let e ← evalConst CodeBlockExpander n
+ let doc? ← findDocString? (← getEnv) n
+ let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+ return (e, doc?, sig)
+
+private unsafe def codeBlockExpandersForUnsafe'' (x : Name) : DocElabM (Array CodeBlockExpander) := do
let expanders := codeBlockExpanderAttr.getEntries (← getEnv) x
return expanders.map (·.value) |>.toArray
+private unsafe def codeBlockExpandersForUnsafe (x : Name) : DocElabM (Array (CodeBlockExpander × Option String × Option SigDoc)) := do
+ return (← codeBlockExpandersForUnsafe' x) ++ (← codeBlockExpandersForUnsafe'' x).map (·, none, none)
+
@[implemented_by codeBlockExpandersForUnsafe]
-opaque codeBlockExpandersFor (x : Name) : DocElabM (Array CodeBlockExpander)
+opaque codeBlockExpandersFor (x : Name) : DocElabM (Array (CodeBlockExpander × Option String × Option SigDoc))
+abbrev DirectiveExpander := Array Arg → TSyntaxArray `block → DocElabM (Array (TSyntax `term))
+abbrev DirectiveExpanderOf α := α → TSyntaxArray `block → DocElabM Term
-abbrev DirectiveExpander := Array Arg → TSyntaxArray `block → DocElabM (Array (TSyntax `term))
initialize directiveExpanderAttr : KeyedDeclsAttribute DirectiveExpander ←
mkDocExpanderAttribute `directive_expander ``DirectiveExpander "Indicates that this function is used to implement a given directive" `directiveExpanderAttr
-unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array DirectiveExpander) := do
+private def toDirective {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Term) : DirectiveExpander :=
+ fun args blocks => do
+ let v ← ArgParse.parse args
+ return #[← expander v blocks]
+
+syntax (name := directive) "directive " (ident)? : attr
+
+initialize directiveExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+ registerPersistentEnvExtension {
+ mkInitial := pure {},
+ addImportedFn xss :=
+ pure <| xss.foldl (init := {}) fun ns xs =>
+ xs.foldl (init := ns) fun ns (x, ys) =>
+ ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+ addEntryFn
+ | xs, (x, y) =>
+ xs.insert x (xs.find? x |>.getD #[] |>.push y)
+ exportEntriesFn xs :=
+ xs.toArray
+ }
+
+unsafe initialize registerBuiltinAttribute {
+ name := `directive,
+ descr := "Define a new directive",
+ applicationTime := .afterCompilation,
+ add declName stx k := do
+ unless k == .global do throwError m!"Must be `global`"
+ let directiveName ←
+ match stx with
+ | `(attr|directive) => pure declName
+ | `(attr|directive $x) => realizeGlobalConstNoOverloadWithInfo x
+ | _ => throwError "Invalid `directive` attribute"
+
+ let n ← mkFreshUserName <| declName ++ `directive
+
+ let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do
+ let e ← Meta.mkAppM ``toDirective #[.const declName []]
+ let e ← instantiateMVars e
+ let t ← Meta.inferType e
+
+
+ match_expr e with
+ | toDirective ty _ _ => saveSignature n ty
+ | _ => pure ()
+
+ pure (e, t)
+
+ addAndCompile <| .defnDecl {
+ name := n,
+ levelParams := [],
+ type := t,
+ value := e,
+ hints := .opaque,
+ safety := .safe
+ }
+
+ addDocStringCore' n (← findSimpleDocString? (← getEnv) declName)
+
+ modifyEnv fun env =>
+ directiveExpanderExt.addEntry env (directiveName, n)
+}
+
+private unsafe def directiveExpandersForUnsafe' (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do
+ let expanders := directiveExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+ expanders.mapM fun n => do
+ let e ← evalConst DirectiveExpander n
+ let doc? ← findDocString? (← getEnv) n
+ let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+ return (e, doc?, sig)
+
+private unsafe def directiveExpandersForUnsafe'' (x : Name) : DocElabM (Array DirectiveExpander) := do
let expanders := directiveExpanderAttr.getEntries (← getEnv) x
return expanders.map (·.value) |>.toArray
+private unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do
+ return (← directiveExpandersForUnsafe' x) ++ (← directiveExpandersForUnsafe'' x).map (·, none, none)
+
@[implemented_by directiveExpandersForUnsafe]
-opaque directiveExpandersFor (x : Name) : DocElabM (Array DirectiveExpander)
+opaque directiveExpandersFor (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc))
+
+
+abbrev BlockCommandExpander := Array Arg → DocElabM (Array (TSyntax `term))
+abbrev BlockCommandOf α := α → DocElabM Term
+initialize blockCommandExpanderAttr : KeyedDeclsAttribute BlockCommandExpander ←
+ mkDocExpanderAttribute `block_command_expander ``BlockCommandExpander "Indicates that this function is used to implement a given block-level command" `blockCommandExpanderAttr
-abbrev BlockRoleExpander := Array Arg → Array Syntax → DocElabM (Array (TSyntax `term))
+private def toBlockCommand {α : Type} [FromArgs α DocElabM] (expander : α → DocElabM Term) : BlockCommandExpander :=
+ fun args => do
+ let v ← ArgParse.parse args
+ return #[← expander v]
+
+syntax (name := block_command) "block_command " (ident)? : attr
+
+initialize blockCommandExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+ registerPersistentEnvExtension {
+ mkInitial := pure {},
+ addImportedFn xss :=
+ pure <| xss.foldl (init := {}) fun ns xs =>
+ xs.foldl (init := ns) fun ns (x, ys) =>
+ ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+ addEntryFn
+ | xs, (x, y) =>
+ xs.insert x (xs.find? x |>.getD #[] |>.push y)
+ exportEntriesFn xs :=
+ xs.toArray
+ }
-initialize blockRoleExpanderAttr : KeyedDeclsAttribute BlockRoleExpander ←
- mkDocExpanderAttribute `block_role_expander ``BlockRoleExpander "Indicates that this function is used to implement a given blockRole" `blockRoleExpanderAttr
+unsafe initialize registerBuiltinAttribute {
+ name := `block_command,
+ descr := "Define a new block command",
+ applicationTime := .afterCompilation,
+ add declName stx k := do
+ unless k == .global do throwError m!"Must be `global`"
+ let cmdName ←
+ match stx with
+ | `(attr|block_command) => pure declName
+ | `(attr|block_command $x) => realizeGlobalConstNoOverloadWithInfo x
+ | _ => throwError "Invalid `block_command` attribute"
-unsafe def blockRoleExpandersForUnsafe (x : Name) : DocElabM (Array BlockRoleExpander) := do
- let expanders := blockRoleExpanderAttr.getEntries (← getEnv) x
+ let n ← mkFreshUserName <| declName ++ `block_command
+
+ let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do
+ let e ← Meta.mkAppM ``toBlockCommand #[.const declName []]
+ let e ← instantiateMVars e
+ let t ← Meta.inferType e
+
+ match_expr e with
+ | toBlockCommand ty _ _ => saveSignature n ty
+ | _ => pure ()
+
+ pure (e, t)
+
+ addAndCompile <| .defnDecl {
+ name := n,
+ levelParams := [],
+ type := t,
+ value := e,
+ hints := .opaque,
+ safety := .safe
+ }
+
+ addDocStringCore' n (← findSimpleDocString? (← getEnv) declName)
+
+ modifyEnv fun env =>
+ blockCommandExpanderExt.addEntry env (cmdName, n)
+}
+
+private unsafe def blockCommandExpandersForUnsafe' (x : Name) : DocElabM (Array (BlockCommandExpander × Option String × Option SigDoc)) := do
+ let expanders := blockCommandExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+ expanders.mapM fun n => do
+ let e ← evalConst BlockCommandExpander n
+ let doc? ← findDocString? (← getEnv) n
+ let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+ return (e, doc?, sig)
+
+private unsafe def blockCommandExpandersForUnsafe'' (x : Name) : DocElabM (Array BlockCommandExpander) := do
+ let expanders := blockCommandExpanderAttr.getEntries (← getEnv) x
return expanders.map (·.value) |>.toArray
-@[implemented_by blockRoleExpandersForUnsafe]
-opaque blockRoleExpandersFor (x : Name) : DocElabM (Array BlockRoleExpander)
+private unsafe def blockCommandExpandersForUnsafe (x : Name) : DocElabM (Array (BlockCommandExpander × Option String × Option SigDoc)) := do
+ return (← blockCommandExpandersForUnsafe' x) ++ (← blockCommandExpandersForUnsafe'' x).map (·, none, none)
+
+@[implemented_by blockCommandExpandersForUnsafe]
+opaque blockCommandExpandersFor (x : Name) : DocElabM (Array (BlockCommandExpander × Option String × Option SigDoc))
diff --git a/src/verso/Verso/Doc/Lsp.lean b/src/verso/Verso/Doc/Lsp.lean
index ff245163e..3d5b6631f 100644
--- a/src/verso/Verso/Doc/Lsp.lean
+++ b/src/verso/Verso/Doc/Lsp.lean
@@ -535,19 +535,11 @@ partial def versoTokens (text : FileMap) (stx : Syntax) : Array SemanticTokenEnt
mkTok text .keyword s ++
-- No tokens for defs, because Lean should supply them
mkTok text .keyword e
- | `(block| block_role{%$s $f $args* }%$e) =>
+ | `(block| command{%$s $f $args* }%$e) =>
mkTok text .keyword s ++
mkTok text .function f ++
versoTokens text (mkNullNode args) ++
mkTok text .keyword e
- | `(block| block_role{%$s $f $args* }%$e [%$s' $block ]%$e') =>
- mkTok text .keyword s ++
- mkTok text .function f ++
- versoTokens text (mkNullNode args) ++
- mkTok text .keyword e ++
- mkTok text .keyword s' ++
- versoTokens text block ++
- mkTok text .keyword e'
| `(argument| $x:ident :=%$eq $v:arg_val) =>
mkTok text .parameter x ++
mkTok text .keyword eq ++
diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean
index 6cfd83d59..3798c3d0b 100644
--- a/src/verso/Verso/Parser.lean
+++ b/src/verso/Verso/Parser.lean
@@ -2396,7 +2396,7 @@ mutual
-- This low-level definition is to get exactly the right amount of lookahead
-- together with column tracking
- partial def block_role (ctxt : BlockCtxt) : ParserFn := fun c s =>
+ partial def block_command (ctxt : BlockCtxt) : ParserFn := fun c s =>
let iniPos := s.pos
let iniSz := s.stxStack.size
let restorePosOnErr : ParserState → ParserState
@@ -2405,15 +2405,13 @@ mutual
let s := eatSpaces c s
if s.hasError then restorePosOnErr s
else
- let col := c.currentColumn s
let s := (intro >> eatSpaces >> ignoreFn (satisfyFn (· == '\n') "newline" <|> eoiFn)) c s
if s.hasError then restorePosOnErr s
else
- let s := (nodeFn nullKind <| atomicFn (ignoreFn (eatSpaces >> (satisfyFn (· == '\n') "newline" <|> eoiFn))) <|> block {ctxt with minIndent := col}) c s
- s.mkNode ``block_role iniSz
+ s.mkNode ``Verso.Syntax.command iniSz
where
eatSpaces := takeWhileFn (· == ' ')
- intro := guardMinColumn (ctxt.minIndent) >> withCurrentColumn fun c => atomicFn (chFn '{') >> withCurrentColumn fun c' => nameAndArgs (some c') >> nameArgWhitespace (some c) >> chFn '}'
+ intro := guardMinColumn (ctxt.minIndent) >> atomicFn (chFn '{') >> nameAndArgs >> nameArgWhitespace none >> chFn '}'
partial def linkRef (c : BlockCtxt) : ParserFn :=
nodeFn ``link_ref <|
@@ -2430,7 +2428,7 @@ mutual
notFollowedByFn blockOpener "block opener" >> guardMinColumn c.minIndent >> textLine
partial def block (c : BlockCtxt) : ParserFn :=
- block_role c <|> unorderedList c <|> orderedList c <|> definitionList c <|> header c <|> codeBlock c <|> directive c <|> blockquote c <|> linkRef c <|> footnoteRef c <|> para c <|> metadataBlock
+ block_command c <|> unorderedList c <|> orderedList c <|> definitionList c <|> header c <|> codeBlock c <|> directive c <|> blockquote c <|> linkRef c <|> footnoteRef c <|> para c <|> metadataBlock
partial def blocks (c : BlockCtxt) : ParserFn := sepByFn true (block c) (ignoreFn (manyFn blankLine))
@@ -4149,93 +4147,84 @@ r##"* `structure` and `inductive` commands
/--
info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- []
- "}"
- [(Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str "\"Here's a modified paragraph.\""))]
- "}")])
-All input consumed.
+ (Verso.Syntax.command "{" `test [] "}")
+Remaining:
+"Here's a paragraph."
-/
#guard_msgs in
-#eval block {} |>.test! "{test}\nHere's a modified paragraph."
+#eval block {} |>.test! "{test}\nHere's a paragraph."
+
/--
info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- []
- "}"
- [(Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str "\"Here's a modified paragraph.\""))]
- "}")])
+ [(Verso.Syntax.command "{" `test [] "}")
+ (Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.text
+ (str "\"Here's a paragraph.\""))]
+ "}")]
All input consumed.
-/
#guard_msgs in
-#eval block {} |>.test! "{test}\n Here's a modified paragraph."
+#eval blocks {} |>.test! "{test}\nHere's a paragraph."
+
/--
info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- []
- "}"
- [(Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str "\"Here's a modified paragraph.\""))]
- "}")])
-All input consumed.
+ (Verso.Syntax.command "{" `test [] "}")
+Remaining:
+" Here's a paragraph."
-/
#guard_msgs in
-#eval block {} |>.test! " {test}\n Here's a modified paragraph."
+#eval block {} |>.test! "{test}\n Here's a paragraph."
+
/--
-info: Failure @8 (⟨2, 0⟩): ':'; expected %%% (at line beginning), expected column at least 1 or expected end of file
-Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- []
- "}"
- [(Verso.Syntax.metadata_block
-
- )])
-Remaining: "Here's a modified paragraph."
+info: Success! Final stack:
+ (Verso.Syntax.command "{" `test [] "}")
+Remaining:
+" Here's a paragraph."
-/
#guard_msgs in
-#eval block {} |>.test! " {test}\nHere's a modified paragraph."
+#eval block {} |>.test! " {test}\n Here's a paragraph."
+/--
+info: Success! Final stack:
+ (Verso.Syntax.command "{" `test [] "}")
+Remaining:
+"Here's a paragraph."
+-/
+#guard_msgs in
+#eval block {} |>.test! " {test}\nHere's a paragraph."
/--
info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- []
- "}"
- [(Verso.Syntax.blockquote
- ">"
- [(Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str
- "\"Here's a modified blockquote\""))]
- "}")
- (Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str "\"with multiple paras\""))]
- "}")])])
+ (Verso.Syntax.command "{" `test [] "}")
Remaining:
-"that ends"
+"> Here's a blockquote\n\n with multiple paras\n\nthat ends"
-/
#guard_msgs in
-#eval block {} |>.test! "{test}\n> Here's a modified blockquote\n\n with multiple paras\n\nthat ends"
+#eval block {} |>.test! "{test}\n> Here's a blockquote\n\n with multiple paras\n\nthat ends"
+
+/--
+info: Success! Final stack:
+ [(Verso.Syntax.command "{" `test [] "}")
+ (Verso.Syntax.blockquote
+ ">"
+ [(Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.text
+ (str "\"Here's a blockquote\""))]
+ "}")
+ (Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.text
+ (str "\"with multiple paras\""))]
+ "}")])
+ (Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.text (str "\"that ends\""))]
+ "}")]
+All input consumed.
+-/
+#guard_msgs in
+#eval blocks {} |>.test! "{test}\n> Here's a blockquote\n\n with multiple paras\n\nthat ends"
/--
info: 2 failures:
@@ -4258,18 +4247,21 @@ Final stack:
#eval block {} |>.test! "{\ntest}\nHere's a modified paragraph."
/--
-info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- []
- "}"
- [(Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str "\"Here's a modified paragraph.\""))]
- "}")])
-All input consumed.
+info: 2 failures:
+ @37 (⟨3, 28⟩): expected identifier
+ ""
+ @37 (⟨3, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+ ""
+
+Final stack:
+ (Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.role
+ "{"
+
+ "["
+ [(Verso.Syntax.footnote )]
+ "]")])
-/
#guard_msgs in
#eval block {} |>.test! "{\n test}\nHere's a modified paragraph."
@@ -4295,36 +4287,52 @@ Final stack:
#eval block {} |>.test! "{\n test\narg}\nHere's a modified paragraph."
/--
-info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- [(Verso.Syntax.anon
- (Verso.Syntax.arg_ident `arg))]
- "}"
- [(Verso.Syntax.para
- "para{"
- [(Verso.Syntax.text
- (str "\"Here's a modified paragraph.\""))]
- "}")])
-All input consumed.
+info: 2 failures:
+ @45 (⟨4, 28⟩): expected identifier
+ ""
+ @45 (⟨4, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+ ""
+
+Final stack:
+ (Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.role
+ "{"
+
+ "["
+ [(Verso.Syntax.footnote )]
+ "]")])
-/
#guard_msgs in
#eval block {} |>.test! "{\n test\n arg}\nHere's a modified paragraph."
+/--
+info: 2 failures:
+ @19 (⟨6, 0⟩): '{'; expected '![', '$$', '$', '[' or '[^'
+ "Here's a paragraph."
+ @19 (⟨6, 0⟩): expected identifier
+ "Here's a paragraph."
+
+Final stack:
+ (Verso.Syntax.para
+ "para{"
+ [(Verso.Syntax.role
+ "{"
+
+ "["
+ [(Verso.Syntax.footnote )]
+ "]")])
+-/
+#guard_msgs in
+#eval block {} |>.test! "{\n test\n arg}\n\n\nHere's a paragraph."
+
/--
info: Success! Final stack:
- (Verso.Syntax.block_role
- "{"
- `test
- [(Verso.Syntax.anon
- (Verso.Syntax.arg_ident `arg))]
- "}"
- [])
-Remaining:
-"\nHere's a non-modified paragraph."
+ [(Verso.Syntax.command "{" `abc [] "}")
+ (Verso.Syntax.command "{" `def [] "}")]
+All input consumed.
-/
#guard_msgs in
-#eval block {} |>.test! "{\n test\n arg}\n\n\nHere's a non-modified paragraph."
+#eval blocks {} |>.test! "{abc}\n{def}\n"
/--
info: Success! Final stack:
diff --git a/src/verso/Verso/Syntax.lean b/src/verso/Verso/Syntax.lean
index a0ab367e4..3f3792e8a 100644
--- a/src/verso/Verso/Syntax.lean
+++ b/src/verso/Verso/Syntax.lean
@@ -152,4 +152,4 @@ def metadataContents := structInstFields (sepByIndent structInstField ", " (allo
/-- Metadata for this section, defined by the current genre -/
syntax (name:=metadata_block) "%%%" metadataContents "%%%" : block
-syntax (name:=block_role) "block_role{" rawIdent argument* "}" ("[" block "]")? : block
+syntax (name:=command) "command{" rawIdent argument* "}" : block