From 8dd994d1ca91238ff845bb6abe4a93292e54ad89 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 30 Oct 2023 14:45:43 -0700
Subject: [PATCH] bug: Fix quote escape problem

---
 Pantograph/Serial.lean | 2 +-
 Test/Serial.lean       | 7 ++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index a46c2c7..c89fc7f 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -52,7 +52,7 @@ def name_to_ast (name: Name) (sanitize: Bool := true): String :=
   else toString name |> enclose_if_escaped
   where
   enclose_if_escaped (n: String) :=
-    let quote := "̈̈\""
+    let quote := "\""
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
diff --git a/Test/Serial.lean b/Test/Serial.lean
index f1b0a9d..dfa3890 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -13,11 +13,12 @@ def test_str_to_name: LSpec.TestSeq :=
   LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
 
 def test_name_to_ast: LSpec.TestSeq :=
-  let quote := "̈̈\""
+  let quote := "\""
+  let escape := "\\"
   LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
-  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}")
+  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
   -- Pathological test case
-  --LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«̈{escape}{quote}»{quote}")
+  LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × Protocol.BoundExpression) := [