--- a/Admin/components/components.sha1 Sat Nov 07 00:28:42 2015 +0100
+++ b/Admin/components/components.sha1 Sat Nov 07 12:53:22 2015 +0100
@@ -33,6 +33,7 @@
20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz
9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz
+f5c63689a394b974ac0d365debda577c6fa31c07 isabelle_fonts-20151107.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
--- a/Admin/components/main Sat Nov 07 00:28:42 2015 +0100
+++ b/Admin/components/main Sat Nov 07 12:53:22 2015 +0100
@@ -4,7 +4,7 @@
e-1.8
exec_process-1.0.3
Haskabelle-2015
-isabelle_fonts-20151106
+isabelle_fonts-20151107
jdk-8u66
jedit_build-20151023
jfreechart-1.0.14-1
--- a/NEWS Sat Nov 07 00:28:42 2015 +0100
+++ b/NEWS Sat Nov 07 12:53:22 2015 +0100
@@ -502,6 +502,8 @@
*** ML ***
+* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
+
* The auxiliary module Pure/display.ML has been eliminated. Its
elementary thm print operations are now in Pure/more_thm.ML and thus
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
--- a/etc/symbols Sat Nov 07 00:28:42 2015 +0100
+++ b/etc/symbols Sat Nov 07 12:53:22 2015 +0100
@@ -353,6 +353,7 @@
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
\<here> code: 0x002302 font: IsabelleText
+\<^undefined> code: 0x002756 group: control font: IsabelleText
\<^noindent> code: 0x0021e4 group: control font: IsabelleText
\<^smallskip> code: 0x002508 group: control font: IsabelleText
\<^medskip> code: 0x002509 group: control font: IsabelleText
--- a/lib/fonts/IsabelleText.sfd Sat Nov 07 00:28:42 2015 +0100
+++ b/lib/fonts/IsabelleText.sfd Sat Nov 07 12:53:22 2015 +0100
@@ -19,7 +19,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1446829878
+ModificationTime: 1446896286
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2241,11 +2241,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 10998 18 16
+WinInfo: 9864 18 16
BeginPrivate: 0
EndPrivate
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 1396
+BeginChars: 1114189 1398
StartChar: u10000
Encoding: 65536 65536 0
@@ -62015,5 +62015,35 @@
206 1142 l 1,50,-1
EndSplineSet
EndChar
+
+StartChar: uni2756
+Encoding: 10070 10070 1397
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+44 569 m 1,0,-1
+ 303 828 l 1,1,-1
+ 563 569 l 1,2,-1
+ 303 309 l 1,3,-1
+ 44 569 l 1,0,-1
+670 569 m 1,4,-1
+ 930 827 l 1,5,-1
+ 1189 569 l 1,6,-1
+ 930 308 l 1,7,-1
+ 670 569 l 1,4,-1
+358 879 m 1,8,-1
+ 618 1140 l 1,9,-1
+ 878 879 l 1,10,-1
+ 618 620 l 1,11,-1
+ 358 879 l 1,8,-1
+358 254 m 1,12,-1
+ 618 514 l 1,13,-1
+ 878 254 l 1,14,-1
+ 618 -6 l 1,15,-1
+ 358 254 l 1,12,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/lib/fonts/IsabelleTextBold.sfd Sat Nov 07 00:28:42 2015 +0100
+++ b/lib/fonts/IsabelleTextBold.sfd Sat Nov 07 12:53:22 2015 +0100
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1446830034
+ModificationTime: 1446896348
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1678,10 +1678,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 10983 21 15
+WinInfo: 9996 21 15
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1388
+BeginChars: 1114115 1389
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -68257,5 +68257,35 @@
206 1142 l 1,50,-1
EndSplineSet
EndChar
+
+StartChar: uni2756
+Encoding: 10070 10070 1388
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+44 569 m 1,0,-1
+ 303 828 l 1,1,-1
+ 563 569 l 1,2,-1
+ 303 309 l 1,3,-1
+ 44 569 l 1,0,-1
+670 569 m 1,4,-1
+ 930 827 l 1,5,-1
+ 1189 569 l 1,6,-1
+ 930 308 l 1,7,-1
+ 670 569 l 1,4,-1
+358 879 m 1,8,-1
+ 618 1140 l 1,9,-1
+ 878 879 l 1,10,-1
+ 618 620 l 1,11,-1
+ 358 879 l 1,8,-1
+358 254 m 1,12,-1
+ 618 514 l 1,13,-1
+ 878 254 l 1,14,-1
+ 618 -6 l 1,15,-1
+ 358 254 l 1,12,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/src/Pure/ML/ml_antiquotations.ML Sat Nov 07 00:28:42 2015 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sat Nov 07 12:53:22 2015 +0100
@@ -16,6 +16,9 @@
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))) #>
+ ML_Antiquotation.inline @{binding undefined}
+ (Scan.succeed "(raise General.Match)") #>
+
ML_Antiquotation.inline @{binding assert}
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>