chore: reorg

ProofWidgets/Data/Html.lean

@@ -1,7 +1,7 @@
 /-
  Copyright (c) 2021-2023 Wojciech Nawrocki. All rights reserved.
  Released under Apache 2.0 license as described in the file LICENSE.
- Authors: Wojciech Nawrocki, Sebastian Ullrich
+ Authors: Wojciech Nawrocki, Sebastian Ullrich, Eric Wieser
  -/
 import Lean.Data.Json.FromToJson
 import Lean.Parser
@@ -140,35 +140,6 @@ section delaborator
 
 open Lean Delaborator SubExpr
 
-/-- Delaborate the elements of a list literal separately, calling `elem` on each. -/
-partial def delabListLiteral {α} (elem : DelabM α) : DelabM (Array α) :=
-  go #[]
-where
-  go (acc : Array α) : DelabM (Array α) := do
-    match_expr ← getExpr with
-    | List.nil _ => return acc
-    | List.cons _ _ _ =>
-      let hd ← withNaryArg 1 elem
-      withNaryArg 2 $ go (acc.push hd)
-    | _ => failure
-
-/-- Delaborate the elements of an array literal separately, calling `elem` on each. -/
-partial def delabArrayLiteral {α} (elem : DelabM α) : DelabM (Array α) := do
-  match_expr ← getExpr with
-  | List.toArray _ _ => withNaryArg 1 <| delabListLiteral elem
-  | _ => failure
-
-/-- A copy of `Delaborator.annotateTermInfo` for other syntactic categories. -/
-def annotateTermLikeInfo (stx : TSyntax n) : DelabM (TSyntax n) := do
-  let stx ← annotateCurPos ⟨stx⟩
-  addTermInfo (← getPos) stx (← getExpr)
-  pure ⟨stx⟩
-
-/-- A copy of `Delaborator.withAnnotateTermInfo` for other syntactic categories. -/
-def withAnnotateTermLikeInfo (d : DelabM (TSyntax n)) : DelabM (TSyntax n) := do
-  let stx ← d
-  annotateTermLikeInfo stx
-
 /-! First delaborate into our non-term `TSyntax`. Note this means we can't call `delab`,
 so we have to add the term annotations ourselves. -/
 

ProofWidgets/Util.lean

@@ -1,6 +1,12 @@
-open Lean
+/-
+ Copyright (c) 2024 Eric Wieser. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Authors: Eric Wieser
+ -/
+import Lean.PrettyPrinter.Delaborator.Basic
 
 namespace ProofWidgets.Util
+open Lean
 
 /-- Sends `#[a, b, c]` to `` `(term| $a ++ $b ++ $c)``-/
 def joinArrays {m} [Monad m] [MonadRef m] [MonadQuotation m] (arr : Array Term) : m Term := do
@@ -28,3 +34,37 @@ def foldInlsM {m} [Monad m] (arr : Array (α ⊕ β)) (f : Array α → m β) :
   return ret
 
 end ProofWidgets.Util
+
+namespace Lean.PrettyPrinter.Delaborator
+open SubExpr
+
+/-- Delaborate the elements of a list literal separately, calling `elem` on each. -/
+partial def delabListLiteral {α} (elem : DelabM α) : DelabM (Array α) :=
+  go #[]
+where
+  go (acc : Array α) : DelabM (Array α) := do
+    match_expr ← getExpr with
+    | List.nil _ => return acc
+    | List.cons _ _ _ =>
+      let hd ← withNaryArg 1 elem
+      withNaryArg 2 $ go (acc.push hd)
+    | _ => failure
+
+/-- Delaborate the elements of an array literal separately, calling `elem` on each. -/
+partial def delabArrayLiteral {α} (elem : DelabM α) : DelabM (Array α) := do
+  match_expr ← getExpr with
+  | List.toArray _ _ => withNaryArg 1 <| delabListLiteral elem
+  | _ => failure
+
+/-- A copy of `Delaborator.annotateTermInfo` for other syntactic categories. -/
+def annotateTermLikeInfo (stx : TSyntax n) : DelabM (TSyntax n) := do
+  let stx ← annotateCurPos ⟨stx⟩
+  addTermInfo (← getPos) stx (← getExpr)
+  pure ⟨stx⟩
+
+/-- A copy of `Delaborator.withAnnotateTermInfo` for other syntactic categories. -/
+def withAnnotateTermLikeInfo (d : DelabM (TSyntax n)) : DelabM (TSyntax n) := do
+  let stx ← d
+  annotateTermLikeInfo stx
+
+end Lean.PrettyPrinter.Delaborator