added @{undefined} with somewhat undefined symbol;
authorwenzelm
Sat Nov 07 12:53:22 2015 +0100 (2015-11-07)
changeset 6159753e32a9b66b8
parent 61596 8323b8e21fe9
child 61598 ed4dad8823a4
added @{undefined} with somewhat undefined symbol;
Admin/components/components.sha1
Admin/components/main
NEWS
etc/symbols
lib/fonts/IsabelleText.sfd
lib/fonts/IsabelleTextBold.sfd
src/Pure/ML/ml_antiquotations.ML
     1.1 --- a/Admin/components/components.sha1	Sat Nov 07 00:28:42 2015 +0100
     1.2 +++ b/Admin/components/components.sha1	Sat Nov 07 12:53:22 2015 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4  20b53cfc3ffc5b15c1eabc91846915b49b4c0367  isabelle_fonts-20151021.tar.gz
     1.5  736844204b2ef83974cd9f0a215738b767958c41  isabelle_fonts-20151104.tar.gz
     1.6  9502c1aea938021f154adadff254c5c55da344bd  isabelle_fonts-20151106.tar.gz
     1.7 +f5c63689a394b974ac0d365debda577c6fa31c07  isabelle_fonts-20151107.tar.gz
     1.8  8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
     1.9  38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
    1.10  d765bc4ad2f34d494429b2a8c1563c49db224944  jdk-7u13.tar.gz
     2.1 --- a/Admin/components/main	Sat Nov 07 00:28:42 2015 +0100
     2.2 +++ b/Admin/components/main	Sat Nov 07 12:53:22 2015 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  e-1.8
     2.5  exec_process-1.0.3
     2.6  Haskabelle-2015
     2.7 -isabelle_fonts-20151106
     2.8 +isabelle_fonts-20151107
     2.9  jdk-8u66
    2.10  jedit_build-20151023
    2.11  jfreechart-1.0.14-1
     3.1 --- a/NEWS	Sat Nov 07 00:28:42 2015 +0100
     3.2 +++ b/NEWS	Sat Nov 07 12:53:22 2015 +0100
     3.3 @@ -502,6 +502,8 @@
     3.4  
     3.5  *** ML ***
     3.6  
     3.7 +* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
     3.8 +
     3.9  * The auxiliary module Pure/display.ML has been eliminated. Its
    3.10  elementary thm print operations are now in Pure/more_thm.ML and thus
    3.11  called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
     4.1 --- a/etc/symbols	Sat Nov 07 00:28:42 2015 +0100
     4.2 +++ b/etc/symbols	Sat Nov 07 12:53:22 2015 +0100
     4.3 @@ -353,6 +353,7 @@
     4.4  \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
     4.5  \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
     4.6  \<here>                 code: 0x002302  font: IsabelleText
     4.7 +\<^undefined>           code: 0x002756  group: control  font: IsabelleText
     4.8  \<^noindent>            code: 0x0021e4  group: control  font: IsabelleText
     4.9  \<^smallskip>           code: 0x002508  group: control  font: IsabelleText
    4.10  \<^medskip>             code: 0x002509  group: control  font: IsabelleText
     5.1 --- a/lib/fonts/IsabelleText.sfd	Sat Nov 07 00:28:42 2015 +0100
     5.2 +++ b/lib/fonts/IsabelleText.sfd	Sat Nov 07 12:53:22 2015 +0100
     5.3 @@ -19,7 +19,7 @@
     5.4  OS2_WeightWidthSlopeOnly: 0
     5.5  OS2_UseTypoMetrics: 1
     5.6  CreationTime: 1050361371
     5.7 -ModificationTime: 1446829878
     5.8 +ModificationTime: 1446896286
     5.9  PfmFamily: 17
    5.10  TTFWeight: 400
    5.11  TTFWidth: 5
    5.12 @@ -2241,11 +2241,11 @@
    5.13  DisplaySize: -96
    5.14  AntiAlias: 1
    5.15  FitToEm: 1
    5.16 -WinInfo: 10998 18 16
    5.17 +WinInfo: 9864 18 16
    5.18  BeginPrivate: 0
    5.19  EndPrivate
    5.20  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
    5.21 -BeginChars: 1114189 1396
    5.22 +BeginChars: 1114189 1398
    5.23  
    5.24  StartChar: u10000
    5.25  Encoding: 65536 65536 0
    5.26 @@ -62015,5 +62015,35 @@
    5.27   206 1142 l 1,50,-1
    5.28  EndSplineSet
    5.29  EndChar
    5.30 +
    5.31 +StartChar: uni2756
    5.32 +Encoding: 10070 10070 1397
    5.33 +Width: 1233
    5.34 +Flags: W
    5.35 +LayerCount: 2
    5.36 +Fore
    5.37 +SplineSet
    5.38 +44 569 m 1,0,-1
    5.39 + 303 828 l 1,1,-1
    5.40 + 563 569 l 1,2,-1
    5.41 + 303 309 l 1,3,-1
    5.42 + 44 569 l 1,0,-1
    5.43 +670 569 m 1,4,-1
    5.44 + 930 827 l 1,5,-1
    5.45 + 1189 569 l 1,6,-1
    5.46 + 930 308 l 1,7,-1
    5.47 + 670 569 l 1,4,-1
    5.48 +358 879 m 1,8,-1
    5.49 + 618 1140 l 1,9,-1
    5.50 + 878 879 l 1,10,-1
    5.51 + 618 620 l 1,11,-1
    5.52 + 358 879 l 1,8,-1
    5.53 +358 254 m 1,12,-1
    5.54 + 618 514 l 1,13,-1
    5.55 + 878 254 l 1,14,-1
    5.56 + 618 -6 l 1,15,-1
    5.57 + 358 254 l 1,12,-1
    5.58 +EndSplineSet
    5.59 +EndChar
    5.60  EndChars
    5.61  EndSplineFont
     6.1 --- a/lib/fonts/IsabelleTextBold.sfd	Sat Nov 07 00:28:42 2015 +0100
     6.2 +++ b/lib/fonts/IsabelleTextBold.sfd	Sat Nov 07 12:53:22 2015 +0100
     6.3 @@ -20,7 +20,7 @@
     6.4  OS2_WeightWidthSlopeOnly: 0
     6.5  OS2_UseTypoMetrics: 1
     6.6  CreationTime: 1050374980
     6.7 -ModificationTime: 1446830034
     6.8 +ModificationTime: 1446896348
     6.9  PfmFamily: 17
    6.10  TTFWeight: 700
    6.11  TTFWidth: 5
    6.12 @@ -1678,10 +1678,10 @@
    6.13  DisplaySize: -96
    6.14  AntiAlias: 1
    6.15  FitToEm: 1
    6.16 -WinInfo: 10983 21 15
    6.17 +WinInfo: 9996 21 15
    6.18  BeginPrivate: 0
    6.19  EndPrivate
    6.20 -BeginChars: 1114115 1388
    6.21 +BeginChars: 1114115 1389
    6.22  
    6.23  StartChar: .notdef
    6.24  Encoding: 1114112 -1 0
    6.25 @@ -68257,5 +68257,35 @@
    6.26   206 1142 l 1,50,-1
    6.27  EndSplineSet
    6.28  EndChar
    6.29 +
    6.30 +StartChar: uni2756
    6.31 +Encoding: 10070 10070 1388
    6.32 +Width: 1233
    6.33 +Flags: W
    6.34 +LayerCount: 2
    6.35 +Fore
    6.36 +SplineSet
    6.37 +44 569 m 1,0,-1
    6.38 + 303 828 l 1,1,-1
    6.39 + 563 569 l 1,2,-1
    6.40 + 303 309 l 1,3,-1
    6.41 + 44 569 l 1,0,-1
    6.42 +670 569 m 1,4,-1
    6.43 + 930 827 l 1,5,-1
    6.44 + 1189 569 l 1,6,-1
    6.45 + 930 308 l 1,7,-1
    6.46 + 670 569 l 1,4,-1
    6.47 +358 879 m 1,8,-1
    6.48 + 618 1140 l 1,9,-1
    6.49 + 878 879 l 1,10,-1
    6.50 + 618 620 l 1,11,-1
    6.51 + 358 879 l 1,8,-1
    6.52 +358 254 m 1,12,-1
    6.53 + 618 514 l 1,13,-1
    6.54 + 878 254 l 1,14,-1
    6.55 + 618 -6 l 1,15,-1
    6.56 + 358 254 l 1,12,-1
    6.57 +EndSplineSet
    6.58 +EndChar
    6.59  EndChars
    6.60  EndSplineFont
     7.1 --- a/src/Pure/ML/ml_antiquotations.ML	Sat Nov 07 00:28:42 2015 +0100
     7.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Sat Nov 07 12:53:22 2015 +0100
     7.3 @@ -16,6 +16,9 @@
     7.4          "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
     7.5            ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))) #>
     7.6  
     7.7 +  ML_Antiquotation.inline @{binding undefined}
     7.8 +    (Scan.succeed "(raise General.Match)") #>
     7.9 +
    7.10    ML_Antiquotation.inline @{binding assert}
    7.11      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    7.12