feat: inline element for Lean commands (#698)

* Refactors a useful helper to make it more broadly accessible.
 * Adds a `leanCommand` role to the inline Lean code infrastructure.

Author: david-christiansen

src/verso-manual/VersoManual/InlineLean.lean

@@ -213,13 +213,12 @@ private def toHighlightedLeanInline (shouldShow : Bool) (hls : Highlighted) (str
   ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(← quoteHighlightViaSerialization hls)) #[Inline.code $(quote str.getString)])
 
 
-/--
-Elaborates the provided Lean command in the context of the current Verso module.
--/
-@[code_block]
-def lean : CodeBlockExpanderOf LeanBlockConfig
-  | config, str => withoutAsync <| do
-
+def elabCommands (config : LeanBlockConfig) (str : StrLit)
+    (toHighlightedLeanContent : (shouldShow : Bool) → (hls : Highlighted) → (str: StrLit) → DocElabM Term)
+    (minCommands : Option Nat := none)
+    (maxCommands : Option Nat := none) :
+    DocElabM Term :=
+  withoutAsync <| do
     PointOfInterest.save (← getRef) ((config.name.map (·.toString)).getD (abbrevFirstLine 20 str.getString))
       (kind := Lsp.SymbolKind.file)
       (detail? := some ("Lean code" ++ config.outlineMeta))
@@ -247,14 +246,24 @@ def lean : CodeBlockExpanderOf LeanBlockConfig
       let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages
       cmds := cmds.push cmd
       pstate := ps'
-      cmdState := {cmdState with messages := messages}
+      cmdState := { cmdState with messages := messages }
 
 
       cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) <|
         runCommand (Command.elabCommand cmd) cmd cctx cmdState
 
       if Parser.isTerminalCommand cmd then break
 
+    let nonTerm := cmds.filter (! Parser.isTerminalCommand ·)
+    if let some maxCmds := maxCommands then
+      if h : nonTerm.size > maxCmds then
+        logErrorAt nonTerm.back m!"Expected at most {maxCmds} commands, but got {nonTerm.size} commands."
+
+    if let some minCmds := minCommands then
+      if h : nonTerm.size < minCmds then
+        let blame := nonTerm[0]? |>.getD (← getRef)
+        logErrorAt blame m!"Expected at least {minCmds} commands, but got {nonTerm.size} commands."
+
     let origEnv ← getEnv
     try
       setEnv cmdState.env
@@ -271,7 +280,7 @@ def lean : CodeBlockExpanderOf LeanBlockConfig
         hls := hls ++ (← highlightIncludingUnparsed cmd nonSilentMsgs cmdState.infoState.trees (startPos? := lastPos))
         lastPos := (cmd.getTrailingTailPos?).getD lastPos
 
-      toHighlightedLeanBlock config.show hls str
+      toHighlightedLeanContent config.show hls str
     finally
       if !config.keep then
         setEnv origEnv
@@ -308,6 +317,22 @@ where
     | .error _ => pure cmdState
     | .ok ((), cmdState) => pure cmdState
 
+/--
+Elaborates the provided Lean command in the context of the current Verso module.
+-/
+@[code_block]
+def lean : CodeBlockExpanderOf LeanBlockConfig
+  | config, str => elabCommands config str toHighlightedLeanBlock
+
+@[role]
+def leanCommand : RoleExpanderOf LeanBlockConfig
+  | config, inls => do
+    if let some str ← oneCodeStr? inls then
+      elabCommands config str toHighlightedLeanInline (minCommands := some 1) (maxCommands := some 1)
+    else
+      `(sorry)
+
+
 /--
 Elaborates the provided Lean term in the context of the current Verso module.
 -/

src/verso/Verso/Code/External.lean

@@ -8,6 +8,7 @@ public import Verso.Doc
 import Verso.Doc.ArgParse
 import Verso.Doc.Elab
 public import Verso.Doc.Elab.Monad
+public meta import Verso.Doc.Helpers
 public meta import Verso.Code.External.Code
 import Verso.Code.External.Code
 public import Verso.Code.External.Config
@@ -62,32 +63,7 @@ public class ExternalCode (genre : Genre) where
 
 open ExternalCode
 
-private meta def oneCodeStr [Monad m] [MonadError m] (inlines : Array (TSyntax `inline)) : m StrLit := do
-  let #[code] := inlines
-    | (if inlines.size == 0 then (throwError ·) else (throwErrorAt (mkNullNode inlines) ·)) "Expected one code element"
-  let `(inline|code($code)) := code
-    | throwErrorAt code "Expected a code element"
-  return code
-
-private meta def oneCodeStr? [Monad m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
-    (inlines : Array (TSyntax `inline)) : m (Option StrLit) := do
-  let #[code] := inlines
-    | if inlines.size == 0 then
-        Lean.logError "Expected a code element"
-      else
-        logErrorAt (mkNullNode inlines) "Expected one code element"
-      return none
-  let `(inline|code($code)) := code
-    | logErrorAt code "Expected a code element"
-      return none
-  return some code
-
-
-private meta def oneCodeName [Monad m] [MonadError m] (inlines : Array (TSyntax `inline)) : m Ident := do
-  let code ← oneCodeStr inlines
-  let str := code.getString
-  let name := if str.contains '.' then str.toName else Name.str .anonymous str
-  return mkIdentFrom code name
+
 
 section
 

src/verso/Verso/Doc/Helpers.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+import Lean.DocString.Syntax
+public import Lean.Exception
+public import Lean.Log
+
+set_option doc.verso true
+
+open Lean Doc.Syntax
+
+namespace Verso.Doc
+
+/--
+If {name}`inlines` contains exactly one code inline, its contents are returned. Throws an error
+otherwise.
+-/
+public def oneCodeStr [Monad m] [MonadError m] (inlines : Array (TSyntax `inline)) : m StrLit := do
+  let #[code] := inlines
+    | (if inlines.size == 0 then (throwError ·) else (throwErrorAt (mkNullNode inlines) ·)) "Expected one code element"
+  let `(inline|code($code:str)) := code
+    | throwErrorAt code "Expected a code element"
+  return code
+
+/--
+If {name}`inlines` contains exactly one code inline, its contents are returned. Otherwise, an error
+is logged and {name}`none` is returned.
+-/
+public def oneCodeStr? [Monad m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
+    (inlines : Array (TSyntax `inline)) : m (Option StrLit) := do
+  let #[code] := inlines
+    | if inlines.size == 0 then
+        Lean.logError "Expected a code element"
+      else
+        logErrorAt (mkNullNode inlines) "Expected one code element"
+      return none
+  let `(inline|code($code)) := code
+    | logErrorAt code "Expected a code element"
+      return none
+  return some code
+
+/--
+If {name}`inlines` contains exactly one Lean name, it is returned with its source location as an
+identifier. Otherwise, an error is thrown.
+-/
+public def oneCodeName [Monad m] [MonadError m] (inlines : Array (TSyntax `inline)) : m Ident := do
+  let code ← oneCodeStr inlines
+  let str := code.getString
+  let name := if str.contains '.' then str.toName else Name.str .anonymous str
+  return mkIdentFrom code name