chore: bump toolchain to v4.29.0-rc1

BibtexQuery.lean

@@ -5,3 +5,4 @@ import BibtexQuery.Query
 import BibtexQuery.String
 import BibtexQuery.Name
 import BibtexQuery.Format
+import BibtexQuery.Xml

BibtexQuery/Format.lean

@@ -6,7 +6,7 @@ Author: Jz Pan
 
 import BibtexQuery.Name
 import BibtexQuery.Entry
-import Lean.Data.Xml.Basic
+import BibtexQuery.Xml
 import Std.Data.HashMap
 import Std.Internal.Parsec
 import Std.Internal.Parsec.String
@@ -20,7 +20,7 @@ tag generating and sorting.
 
 -/
 
-open Lean Xml Std.Internal.Parsec Unicode BibtexQuery.TexDiacritics BibtexQuery.Name
+open BibtexQuery.Xml Std.Internal.Parsec Unicode BibtexQuery.TexDiacritics BibtexQuery.Name
 
 namespace BibtexQuery
 

BibtexQuery/Main.lean

@@ -20,7 +20,7 @@ spaces and special characters before the queries are performed. In addition, the
 firstnamelastname. Hence, for example, "Dupuis, Frédéric" will match the query `a.ericdup`.
 -/
 
-open Lean BibtexQuery
+open BibtexQuery BibtexQuery.Xml
 
 def listDoublons (parseRes : List BibtexQuery.Entry) : List String :=
   let keysOnly := parseRes.filterMap (fun entry => match entry with

BibtexQuery/Name.lean

@@ -21,7 +21,7 @@ return an array of `BibtexName`.
 
 -/
 
-open Lean Unicode BibtexQuery.TexDiacritics
+open BibtexQuery.Xml Unicode BibtexQuery.TexDiacritics
 
 namespace BibtexQuery.Name
 

BibtexQuery/TexDiacritics.lean

@@ -6,7 +6,7 @@ Author: Jz Pan
 
 import Std.Internal.Parsec
 import Std.Internal.Parsec.String
-import Lean.Data.Xml.Basic
+import BibtexQuery.Xml
 import UnicodeBasic
 
 /-!
@@ -20,7 +20,7 @@ and preserve other TeX commands.
 
 -/
 
-open Lean Xml Std.Internal.Parsec Std.Internal.Parsec.String Unicode
+open BibtexQuery.Xml Std.Internal.Parsec Std.Internal.Parsec.String Unicode
 
 namespace BibtexQuery.TexDiacritics
 
@@ -131,7 +131,7 @@ mutual
 
 open Std.TreeMap
 
-/-- Convert a TeX content to HTML, represented by an array of `Lean.Xml.Content`.
+/-- Convert a TeX content to HTML, represented by an array of `Xml.Content`.
 A few TeX commands can be converted to corresponding HTML. -/
 partial def toHtml (x : TexContent) : Array Content :=
   match x with

BibtexQuery/Xml.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Dany Fabian
+
+These types were previously part of Lean.Data.Xml.Basic in the Lean 4 core,
+removed in https://github.com/leanprover/lean4/pull/12302.
+Inlined here for BibtexQuery's use.
+-/
+
+import Std.Data.TreeMap.Basic
+
+namespace BibtexQuery.Xml
+
+def Attributes := Std.TreeMap String String compare
+
+mutual
+
+inductive Element where
+  | Element
+    (name : String)
+    (attributes : Attributes)
+    (content : Array Content)
+
+inductive Content where
+  | Element (element : Element)
+  | Comment (comment : String)
+  | Character (content : String)
+  deriving Inhabited
+
+end
+
+mutual
+
+partial def Element.toString : Element → String
+  | .Element n a c =>
+    let inner := c.map Content.toString |>.toList |> String.join
+    let attrs := a.foldl (init := "") fun acc k v => acc ++ s!" {k}=\"{v}\""
+    s!"<{n}{attrs}>{inner}</{n}>"
+
+partial def Content.toString : Content → String
+  | .Element e => e.toString
+  | .Comment c => s!"<!--{c}-->"
+  | .Character s => s
+
+end
+
+instance : ToString Element := ⟨Element.toString⟩
+instance : ToString Content := ⟨Content.toString⟩
+
+end BibtexQuery.Xml

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ff04f5c424e50e23476d3539c7c0cc4956e971ad",
+   "rev": "9484dd63d30bce157c7f98007a9f26ca4dfb7fb6",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.29.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "BibtexQuery",

lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["BibtexQuery", "«bibtex-query»"]
 [[require]]
 name = "UnicodeBasic"
 git = "https://github.com/fgdorais/lean4-unicode-basic"
-rev = "main"
+rev = "v4.29.0-rc1"
 
 [[lean_lib]]
 name = "BibtexQuery"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.28.0
+leanprover/lean4:v4.29.0-rc1