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)` -/

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) := [