perf: batch-highlighting of code

lake-manifest.json

@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "847084e80500726e4331dded5f17007ddaf89c31",
+   "rev": "10caddf4d067ad0f916cbf231f2870a08977124e",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "sfl-local",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "verso",

lakefile.lean

@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-require subverso from git "https://github.com/leanprover/subverso"@"main"
+require subverso from git "https://github.com/leanprover/subverso"@"sfl-local"
 require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 require plausible from git "https://github.com/leanprover-community/plausible"@"main"
 require illuminate from git "https://github.com/leanprover/illuminate"@"main"

src/multi-verso/MultiVerso/NameMap.lean

@@ -233,8 +233,7 @@ public instance : GetElem? (NameMap α) Name α fun xs n => n ∈ xs where
   getElem xs x ok :=
     if h : isPublic x then
       show α from GetElem.getElem (coll := TreeMap PublicName α PublicName.quickCmp) (idx := PublicName) (elem := α) (valid := fun xs x => x ∈ xs) xs ⟨x, h⟩ <| by
-        simp only [Membership.mem, h, dite_eq_left_of_eq_true] at ok
-        exact ok
+        simpa [Membership.mem, h] using ok
     else
      False.elim <| by
        simp only [Membership.mem, h] at ok

src/verso-manual/VersoManual/InlineLean.lean

@@ -275,6 +275,7 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit)
     let mut cmdState : Command.State := { env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := origScopes }
     let mut pstate := { pos := startPos, recovering := false, hasLeading := false }
     let mut cmds := #[]
+    let mut cmdTrees : Array (Option Lean.Elab.InfoTree) := #[]
 
     repeat
       let scope := cmdState.scopes.head!
@@ -291,6 +292,13 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit)
       let savedTrees := cmdState.infoState.trees
       cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) <|
         runCommand (Command.elabCommandTopLevel cmd) cmd cctx cmdState
+      -- `elabCommandTopLevel` reset the info state, so the trees present now are exactly this
+      -- command's; record them for the batched highlighting pass below.
+      cmdTrees := cmdTrees.push <|
+        match cmdState.infoState.trees.toArray with
+        | #[t] => some t
+        | #[] => none
+        | ts => some (.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd}) ts.toPArray')
       cmdState := { cmdState with
         messages := savedMsgs ++ cmdState.messages,
         infoState := { cmdState.infoState with trees := savedTrees ++ cmdState.infoState.trees }
@@ -319,12 +327,11 @@ meta def elabCommands (config : LeanBlockConfig) (str : StrLit)
         pushInfoTree (disableUnusedVarLinterInInfoTree t)
 
 
-      let mut hls := Highlighted.empty
       let nonSilentMsgs := cmdState.messages.toArray.filter (!·.isSilent)
-      let mut lastPos : String.Pos.Raw := startPos
-      for cmd in cmds do
-        hls := hls ++ (← highlightIncludingUnparsed cmd nonSilentMsgs cmdState.infoState.trees (startPos? := lastPos))
-        lastPos := (cmd.getTrailingTailPos?).getD lastPos
+      -- One batched highlighting pass shares caches between the whole block's commands.
+      let hlArr ← highlightMany cmds nonSilentMsgs cmdTrees
+        (includeUnparsed := true) (startPos? := some startPos)
+      let hls := hlArr.foldl (· ++ ·) Highlighted.empty
 
       toHighlightedLeanContent config.show hls str
     finally