From 079710d40ae17ed3f0f2bc7fc1fc49b8be88318d Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Mon, 5 Jun 2023 18:42:43 -0600
Subject: [PATCH] Sync doc-gen4 with upstream.

---
 DocGen4/Output/Module.lean |  2 +-
 lake-manifest.json         | 12 ++++++------
 lean-toolchain             |  2 +-
 static/search.js           |  3 ++-
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index dd673e5..03c0fdc 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -98,7 +98,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   -- extra information like equations and instances
   let extraInfoHtml ← match doc with
   | DocInfo.classInfo i => pure #[← classInstancesToHtml i.name]
-  | DocInfo.definitionInfo i => equationsToHtml i
+  | DocInfo.definitionInfo i => pure ((← equationsToHtml i) ++ #[← instancesForToHtml i.name])
   | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
   | DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name]
   | DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]
diff --git a/lake-manifest.json b/lake-manifest.json
index 5f9f502..2701e8e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,7 +10,7 @@
   {"git":
    {"url": "https://github.com/leanprover/lake",
     "subDir?": null,
-    "rev": "257fc59a6464f5732a4f49e7dda0fc37475819fb",
+    "rev": "0d4da61cbfe65f19ac7070c2c9f62f36db529c4c",
     "name": "lake",
     "inputRev?": "master"}},
   {"git":
@@ -22,7 +22,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "62e469416e55278c1a4bca000426539b578b7749",
+    "rev": "47535ddd6cff5cf523b8914a5269639641b9bb54",
     "name": "mathlib",
     "inputRev?": "master"}},
   {"git":
@@ -34,7 +34,7 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "409f3b050034337664d21e41fe1cc1bf7f5daec0",
+    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
@@ -46,18 +46,18 @@
   {"git":
    {"url": "https://github.com/fgdorais/lean4-unicode-basic",
     "subDir?": null,
-    "rev": "ce508dcd1fd49ba15675861aafd864572a0b8252",
+    "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
     "name": "UnicodeBasic",
     "inputRev?": "main"}},
   {"git":
    {"url": "https://github.com/leanprover/std4.git",
     "subDir?": null,
-    "rev": "acb5ba1b6643269a37da88fa3ce5d30e27e66bad",
+    "rev": "176b4657e21ea6f5a1517c625ee97e89acad0126",
     "name": "std4",
     "inputRev?": "main"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "3156cd5b375d1a932d590c918b7ad50e3be11947",
+    "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lean-toolchain b/lean-toolchain
index e7e8b2d..02773ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-16
+leanprover/lean4:nightly-2023-05-31
diff --git a/static/search.js b/static/search.js
index 1409e00..7971a82 100644
--- a/static/search.js
+++ b/static/search.js
@@ -147,7 +147,8 @@ DeclarationDataCenter.init()
         checkbox.addEventListener("input", ev => SEARCH_PAGE_INPUT.dispatchEvent(new Event("input")))
       );
       SEARCH_PAGE_INPUT.dispatchEvent(new Event("input"))
-    }
+    };
+    SEARCH_INPUT.dispatchEvent(new Event("input"))
   })
   .catch(e => {
     SEARCH_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS,true ));