# HG changeset patch # User wenzelm # Date 1389824728 -3600 # Node ID e33c5bd729ff492371d3326292d0cda54b7dcd9e # Parent a93f496f6c301c4753c5aeee9f9fbd9ae9725dea added \ symbol, which is used for char/string literals in HOL; diff -r a93f496f6c30 -r e33c5bd729ff NEWS --- a/NEWS Wed Jan 15 22:24:57 2014 +0100 +++ b/NEWS Wed Jan 15 23:25:28 2014 +0100 @@ -42,6 +42,9 @@ *** HOL *** +* The symbol "\" may be used within char or string literals +to represent (Char Nibble0 NibbleA), i.e. ASCII newline. + * Activation of Z3 now works via "z3_non_commercial" system option (without requiring restart), instead of former settings variable "Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu diff -r a93f496f6c30 -r e33c5bd729ff etc/symbols --- a/etc/symbols Wed Jan 15 22:24:57 2014 +0100 +++ b/etc/symbols Wed Jan 15 23:25:28 2014 +0100 @@ -347,6 +347,7 @@ \ code: 0x0000b8 \ code: 0x0002dd \ code: 0x0003f5 +\ code: 0x0023ce \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText diff -r a93f496f6c30 -r e33c5bd729ff lib/fonts/IsabelleText.sfd --- a/lib/fonts/IsabelleText.sfd Wed Jan 15 22:24:57 2014 +0100 +++ b/lib/fonts/IsabelleText.sfd Wed Jan 15 23:25:28 2014 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050361371 -ModificationTime: 1377295392 +ModificationTime: 1389823475 PfmFamily: 17 TTFWeight: 400 TTFWidth: 5 @@ -2240,9 +2240,9 @@ DisplaySize: -48 AntiAlias: 1 FitToEm: 1 -WinInfo: 10544 16 10 +WinInfo: 9104 16 10 TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144 -BeginChars: 1114189 1094 +BeginChars: 1114189 1095 StartChar: u10000 Encoding: 65536 65536 0 @@ -55542,5 +55542,35 @@ 219 -248 l 1,4,-1 EndSplineSet EndChar + +StartChar: uni23CE +Encoding: 9166 9166 1094 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +398 188 m 1,0,-1 + 25 561 l 1,1,-1 + 398 934 l 1,2,-1 + 398 733 l 1,3,-1 + 823 733 l 1,4,-1 + 823 1142 l 1,5,-1 + 1167 1142 l 1,6,-1 + 1167 389 l 1,7,-1 + 398 389 l 1,8,-1 + 398 188 l 1,0,-1 +893 663 m 1,9,-1 + 319 663 l 1,10,-1 + 319 756 l 1,11,-1 + 125 561 l 1,12,-1 + 319 366 l 1,13,-1 + 319 459 l 1,14,-1 + 1097 459 l 1,15,-1 + 1097 1072 l 1,16,-1 + 893 1072 l 1,17,-1 + 893 663 l 1,9,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r a93f496f6c30 -r e33c5bd729ff lib/fonts/IsabelleText.ttf Binary file lib/fonts/IsabelleText.ttf has changed diff -r a93f496f6c30 -r e33c5bd729ff lib/fonts/IsabelleTextBold.sfd --- a/lib/fonts/IsabelleTextBold.sfd Wed Jan 15 22:24:57 2014 +0100 +++ b/lib/fonts/IsabelleTextBold.sfd Wed Jan 15 23:25:28 2014 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050374980 -ModificationTime: 1377295361 +ModificationTime: 1389823579 PfmFamily: 17 TTFWeight: 700 TTFWidth: 5 @@ -1674,8 +1674,8 @@ DisplaySize: -48 AntiAlias: 1 FitToEm: 1 -WinInfo: 10592 16 10 -BeginChars: 1114112 1083 +WinInfo: 9072 16 10 +BeginChars: 1114112 1084 StartChar: u10000 Encoding: 65536 65536 0 @@ -58472,5 +58472,35 @@ 219 -248 l 1,4,-1 EndSplineSet EndChar + +StartChar: uni23CE +Encoding: 9166 9166 1083 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +408 138 m 1,0,-1 + 5 561 l 1,1,-1 + 408 984 l 1,2,-1 + 408 753 l 1,3,-1 + 783 753 l 1,4,-1 + 783 1162 l 1,5,-1 + 1167 1162 l 1,6,-1 + 1167 369 l 1,7,-1 + 408 369 l 1,8,-1 + 408 138 l 1,0,-1 +1067 1072 m 1,9,-1 + 883 1072 l 1,10,-1 + 883 653 l 1,11,-1 + 309 653 l 1,12,-1 + 309 746 l 1,13,-1 + 145 561 l 1,14,-1 + 309 376 l 1,15,-1 + 309 469 l 1,16,-1 + 1067 469 l 1,17,-1 + 1067 1072 l 1,9,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r a93f496f6c30 -r e33c5bd729ff lib/fonts/IsabelleTextBold.ttf Binary file lib/fonts/IsabelleTextBold.ttf has changed diff -r a93f496f6c30 -r e33c5bd729ff src/HOL/String.thy --- a/src/HOL/String.thy Wed Jan 15 22:24:57 2014 +0100 +++ b/src/HOL/String.thy Wed Jan 15 23:25:28 2014 +0100 @@ -148,7 +148,7 @@ "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5, Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8, - Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB, + Char Nibble0 Nibble9, CHR ''\'', Char Nibble0 NibbleB, Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE, Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1, Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4, diff -r a93f496f6c30 -r e33c5bd729ff src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Wed Jan 15 22:24:57 2014 +0100 +++ b/src/HOL/Tools/string_syntax.ML Wed Jan 15 23:25:28 2014 +0100 @@ -28,16 +28,21 @@ (* char *) fun mk_char s = - if Symbol.is_ascii s then - Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)] - else error ("Non-ASCII symbol: " ^ quote s); + let + val c = + if Symbol.is_ascii s then ord s + else if s = "\" then 10 + else error ("Bad character: " ^ quote s); + in Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (c div 16), mk_nib (c mod 16)] end; val specials = raw_explode "\\\"`'"; fun dest_chr c1 c2 = let val c = chr (dest_nib c1 * 16 + dest_nib c2) in if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c - then c else raise Match + then c + else if c = "\n" then "\" + else raise Match end; fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2