adapt changes to Option String

leanprover · Jun 11, 2024 · f50d2c1 · f50d2c1
1 parent 175fbfd
commit f50d2c1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
@@ -228,7 +228,9 @@ end
 
 /-- Convert docstring to Html. -/
 def docStringToHtml (s : String) : HtmlM (Array Html) := do
-  let rendered := MD4Lean.renderHtml s
+  let rendered := match MD4Lean.renderHtml s with
+    | .some res => res
+    | _ => "" -- TODO: should print some error message
   match manyDocument rendered.mkIterator with
   | Parsec.ParseResult.success _ res =>
     -- TODO: use `toString` instead of `eToStringEscaped`

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "45c9ddea211f51a9f6564d920f8aedc4ad252cfe",
+   "rev": "d812b96744f9b60879cbfa9c436de2b95003db2a",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",