feat: shim code for lean4web

src/verso-manual/VersoManual.lean

@@ -1045,3 +1045,96 @@ where
       emit cfg text traverseState
       for step in extraSteps do
         step .single cfg.toConfig traverseState text
+
+
+
+
+section HtmlRPC
+/-!
+What we *are* doing: doc finalizer elaborates and stores HTML string in
+environment extension, RPC retrieves string from environment extension.
+
+What we *should be* doing:
+ - Verso is proactively storing a representation of the document in an
+   environment extension
+ - The RPC is looking up that representation of the document, incurring the
+   cost of elaboration and translation to an HTML string, and returning that
+-/
+
+open Lean
+
+/-! The environment extension in question -/
+
+inductive VersoDocumentData where
+  | success : String → VersoDocumentData
+  | errors : Array String → VersoDocumentData
+  | noDoc : VersoDocumentData
+deriving ToJson, FromJson
+
+initialize versoDocumentExt : EnvExtension (Option VersoDocumentData) ←
+  registerEnvExtension (pure .none)
+
+/-! Alternative route to HTML output -/
+
+def shortcutToHtml (extensionImpls : ExtensionImpls) (part : Lean.Doc.Part Genre.Manual.Inline Genre.Manual.Block Genre.Manual.PartMetadata) : IO VersoDocumentData := do
+  let (logs, result) ← runWithLogs do
+    let (part, traverseState) ← traverse part { htmlDepth := 0 }
+    let contentGenerator : StateT (State Html) (ReaderT AllRemotes (ReaderT ExtensionImpls (BuildLogT IO))) Html := do
+      Manual.toHtml {} {} traverseState (traverseState.definitionIds {}) {} {} part
+    let (html, htmlState) ← contentGenerator |>.run .empty |>.run {}
+
+    let featureJsFiles :=
+      traverseState.features.toArray.flatMap fun f =>
+        f.jsFilePaths.map fun (name, defer) => ("/verso/view/-verso-data/" ++ name, defer)
+    let extraJsFiles :=
+      sortJs <|
+        traverseState.extraJsFiles.toArray.map (false, ·.toStaticJsFile)
+    let extraJsFiles := featureJsFiles ++ extraJsFiles.map fun
+      | (true, f) => (f.filename, f.defer)
+      | (false, f) => ("/verso/view/-verso-data/" ++ f.filename, f.defer)
+    let cssFiles :=
+      traverseState.extraCssFiles.toArray.map (·.filename) ++
+      traverseState.features.toArray.flatMap (fun f => f.cssFilePaths)
+
+    let page := Html.standalonePage html htmlState.dedup.docJson
+      (extraJsFiles := extraJsFiles)
+      (extraStylesheets := cssFiles.toList.map ("/verso/view/-verso-data/" ++ ·))
+    return Html.doctype ++ page.asString
+  if logs.size > 0 then
+    return .errors (logs.map (·.format))
+  return .success result
+where
+  runWithLogs {a} (act : ReaderT ExtensionImpls (BuildLogT IO) a) : IO (Array LogMessage × a) := do
+    let logger ← Logger.new
+    let result ← ReaderT.run act extensionImpls |> (ReaderT.run · logger)
+    return (← logger.errors, result)
+
+/-! When the document is finished parsing, generate HTML and put it in the extension -/
+
+open Elab.Command in
+def putDocInContext (doc : VersoDocumentData) : CommandElabM Unit := do
+  modifyEnv (versoDocumentExt.setState · (.some doc))
+
+section RPC
+open Elab.Command Server
+
+@[doc_finalize]
+unsafe def liveDocFinalizer : CommandElabM Unit := do
+  let name := docName (← getEnv).mainModule
+  let versoDoc ← liftTermElabM <| evalConst (VersoDoc Manual) name
+  let htmlDoc ← shortcutToHtml (by exact extension_impls%) (versoDoc.toPart)
+  putDocInContext htmlDoc
+
+@[server_rpc_method]
+def _root_.Verso.getLiveDocument (_ : Unit) : RequestM (RequestTask VersoDocumentData) := do
+  let doc ← RequestM.readDoc
+  let endPos := doc.meta.text.source.rawEndPos
+  RequestM.withWaitFindSnap doc (·.endPos >= endPos) (notFoundX := pure (.errors #["Internal invariant violated: notFoundX"]))
+    fun snap =>
+      match versoDocumentExt.getState snap.env with
+      | .none => return .noDoc
+      | .some s =>
+        return s
+
+end RPC
+end HtmlRPC

src/verso-manual/VersoManual/Html.lean

@@ -516,6 +516,35 @@ public def page
   }}
 
 
+public def standalonePage (contents : Html) (highlightingJson : Lean.Json)
+  (extraJsFiles : Array (String × Bool) := #[])
+  (extraStylesheets : List String := []) :=
+  let defer := #[("defer", "defer")]
+  {{
+    <html>
+      <head>
+        <link rel="icon" href="data:," />
+        <meta charset="utf-8"/>
+        <meta name="viewport" content="height=device-height, width=device-width, initial-scale=1, minimum-scale=1, maximum-scale=1"/>
+        <title>{{"Verso Document"}}</title>
+        <link rel="stylesheet" href="/verso/view/book.css" />
+        <link rel="stylesheet" href="/verso/view/verso-vars.css" />
+        <script src="https://cdn.jsdelivr.net/npm/marked@11.1.1/marked.min.js" integrity="sha384-zbcZAIxlvJtNE3Dp5nxLXdXtXyxwOdnILY1TDPVmKFhl4r4nSUG1r8bcFXGVa4Te" crossorigin="anonymous"></script>
+        {{extraJsFiles.map fun f => ({{<script src=s!"{f.1}" {{if f.2 then defer else #[]}}></script>}})}}
+        {{extraStylesheets.map (fun url => {{<link rel="stylesheet" href={{url}}/> }})}}
+        <script>{{Html.text false <| Code.highlightingJs (highlightJsonPromise := "Promise.resolve(" ++ highlightingJson.compress ++ ")")}}</script>
+        <style>{{Html.text false Code.highlightingStyle}}</style>
+      </head>
+      <body>
+        <main>
+          <div class="content-wrapper titlepage">
+            {{contents}}
+          </div>
+        </main>
+      </body>
+    </html>
+  }}
+
 
 public def relativize (path : Path) (html : Html) : Html :=
   html.visitM (m := ReaderT Path Id) (tag := rwTag) |>.run path

src/verso/Verso/Doc/Concrete.lean

@@ -13,6 +13,7 @@ public import Verso.Doc.Elab
 public meta import Verso.Doc.Elab.Monad
 import Verso.Doc.Concrete.InlineString
 import Verso.Doc.Lsp
+public meta import Verso.Doc.Elab.Finalize
 
 namespace Verso.Doc.Concrete
 
@@ -396,6 +397,7 @@ elab_rules : command
     -- so we detect that case and call finishDoc.
     if stopPos.extract txt.source txt.source.rawEndPos |>.all Char.isWhitespace then
       finishDoc
+      Finalize.runFinalizers
 
 open Command in
 /--
@@ -423,4 +425,5 @@ public meta def elabVersoLastBlock : Command.CommandElab
     runVersoBlock b
     -- Finish up the document
     finishDoc
+    Finalize.runFinalizers
   | _ => throwUnsupportedSyntax

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

@@ -0,0 +1,25 @@
+module
+public import Lean
+import Verso.Doc
+
+open Lean
+namespace Verso.Doc.Elab.Finalize
+
+public meta initialize docFinalizeAttr : TagAttribute ←
+  registerTagAttribute `doc_finalize "Indicate to Verso that this function should be run on documents post-parsing" fun declName => do
+    let decl ← getConstInfo declName
+    match decl.type with
+      | (.app (.const ``Elab.Command.CommandElabM []) (.const ``Unit [])) => return
+      | _ => throwError "Decl does not have type `CommandElabM Unit` expected for a document finalizer"
+
+meta def runFinalizer (finalizerName : Name) : Elab.Command.CommandElabM Unit := do
+  let finalizer := mkIdent finalizerName
+  Elab.Command.elabCommand (← `(#eval $finalizer))
+
+public meta def runFinalizers : Elab.Command.CommandElabM Unit := do
+  let state := docFinalizeAttr.ext.toEnvExtension.getState (← getEnv)
+  for list in state.importedEntries do
+    for finalizerName in list do
+      runFinalizer finalizerName
+  for finalizerName in state.state do
+    runFinalizer finalizerName