Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Made test_term escape special characters in strings that caused the
authorberghofe
Wed, 24 Nov 2004 10:37:38 +0100
changeset 15326 ff21cddee442
parent 15325 50ac7d2c34c9
child 15327 0230a10582d3
Made test_term escape special characters in strings that caused the ML compiler to fail.
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/codegen.ML	Wed Nov 24 10:32:33 2004 +0100
+++ b/src/Pure/codegen.ML	Wed Nov 24 10:37:38 2004 +0100
@@ -642,7 +642,7 @@
               Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
                 flat (separate [Pretty.str ",", Pretty.brk 1]
                   (map (fn (s, T) => [Pretty.block
-                    [Pretty.str ("(" ^ Library.quote s ^ ","), Pretty.brk 1,
+                    [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
                      mk_app false (mk_term_of sg false T)
                        [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
                   [Pretty.str "]"])]],
isabelle