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