Revert "chore: complete ProofWidgets bump (#7056)"

This reverts commit ae7a2e4.
leanprover-community · Sep 10, 2023 · c2c2f83 · c2c2f83
1 parent ff7397e
commit c2c2f83
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/Mathlib/Tactic/Widget/CommDiag.lean b/Mathlib/Tactic/Widget/CommDiag.lean
@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Category.Basic
 
 import ProofWidgets.Component.PenroseDiagram
 import ProofWidgets.Presentation.Expr
-import ProofWidgets.Component.Panel.SelectionPanel
+import ProofWidgets.Component.SelectionPanel
 
 /-! This module defines tactic/meta infrastructure for displaying commutative diagrams in the
 infoview. -/
@@ -58,13 +58,13 @@ open scoped Jsx in
 display as labels in the diagram. -/
 def mkCommDiag (sub : String) (embeds : ExprEmbeds) : MetaM Html := do
   let embeds ← embeds.mapM fun (s, h) =>
-      return (s, <InteractiveCode fmt={← Widget.ppExprTagged h} />)
-  return (
+      return (s, Html.ofTHtml <InteractiveCode fmt={← Widget.ppExprTagged h} />)
+  return Html.ofTHtml
     <PenroseDiagram
       embeds={embeds}
       dsl={include_str ".."/".."/".."/"widget"/"src"/"penrose"/"commutative.dsl"}
       sty={include_str ".."/".."/".."/"widget"/"src"/"penrose"/"commutative.sty"}
-      sub={sub} />)
+      sub={sub} />
 
 /-! ## Commutative triangles -/
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "44e6673a20fc0449d003983d1e1f472df40f7107",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.15",
+    "inputRev?": "v0.0.13",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",

diff --git a/test/CommDiag.lean b/test/CommDiag.lean
@@ -1,5 +1,5 @@
 import Mathlib.Tactic.Widget.CommDiag
-import ProofWidgets.Component.Panel.GoalTypePanel
+import ProofWidgets.Component.GoalTypePanel
 
 /-! ## Example use of commutative diagram widgets -/