# HG changeset patch # User wenzelm # Date 1446897202 -3600 # Node ID 53e32a9b66b8834dfb19186c85fdb8fd812c15e1 # Parent 8323b8e21fe9a1a6d09ccacac23da64d6b26eb39 added @{undefined} with somewhat undefined symbol; diff -r 8323b8e21fe9 -r 53e32a9b66b8 Admin/components/components.sha1 --- 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 diff -r 8323b8e21fe9 -r 53e32a9b66b8 Admin/components/main --- 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 diff -r 8323b8e21fe9 -r 53e32a9b66b8 NEWS --- 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. diff -r 8323b8e21fe9 -r 53e32a9b66b8 etc/symbols --- 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 @@ \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \ 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 diff -r 8323b8e21fe9 -r 53e32a9b66b8 lib/fonts/IsabelleText.sfd --- 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 diff -r 8323b8e21fe9 -r 53e32a9b66b8 lib/fonts/IsabelleTextBold.sfd --- 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 diff -r 8323b8e21fe9 -r 53e32a9b66b8 src/Pure/ML/ml_antiquotations.ML --- 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\")") #>