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.
specials: include single quote;
authorwenzelm
Mon, 11 Dec 2006 21:41:05 +0100
changeset 21775 8be8da44ee56
parent 21774 3f9324ff06e3
child 21776 e65109e168f3
specials: include single quote;
src/HOL/Tools/string_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/string_syntax.ML	Mon Dec 11 21:41:03 2006 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Mon Dec 11 21:41:05 2006 +0100
@@ -32,7 +32,7 @@
     Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
   else error ("Non-ASCII symbol: " ^ quote s);
 
-val specials = explode "\\\"`";
+val specials = explode "\\\"`'";
 
 fun dest_chr c1 c2 =
   let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
isabelle