--- 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 "\<newline>" 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
--- 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 @@
\<cedilla> code: 0x0000b8
\<hungarumlaut> code: 0x0002dd
\<some> code: 0x0003f5
+\<newline> code: 0x0023ce
\<^sub> code: 0x0021e9 group: control font: IsabelleText
\<^sup> code: 0x0021e7 group: control font: IsabelleText
\<^bold> code: 0x002759 group: control font: IsabelleText
--- 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
Binary file lib/fonts/IsabelleText.ttf has changed
--- 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
Binary file lib/fonts/IsabelleTextBold.ttf has changed
--- 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 ''\<newline>'', 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,
--- 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 = "\<newline>" 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 "\<newline>"
+ else raise Match
end;
fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2