--- a/Admin/isabelle_fonts/IsabelleSymbols.sfd Wed Jul 17 09:40:43 2019 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbols.sfd Wed Jul 17 11:09:43 2019 +0200
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1563348871
+ModificationTime: 1563353029
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2242,11 +2242,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 64 32 8
+WinInfo: 10944 32 8
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 1411
+BeginChars: 1114189 1412
StartChar: u10000
Encoding: 65536 65536 0
@@ -61628,5 +61628,25 @@
578 410 l 1,19,-1
EndSplineSet
EndChar
+
+StartChar: uni2AFF
+Encoding: 11007 11007 1411
+Width: 1151
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+350 1576 m 1,0,-1
+ 350 -466 l 1,1,-1
+ 788 -466 l 1,2,-1
+ 788 1576 l 1,3,-1
+ 350 1576 l 1,0,-1
+264 1670 m 1,4,-1
+ 880 1670 l 1,5,-1
+ 880 -558 l 1,6,-1
+ 264 -558 l 1,7,-1
+ 264 1670 l 1,4,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Wed Jul 17 09:40:43 2019 +0200
+++ b/Admin/isabelle_fonts/IsabelleSymbolsBold.sfd Wed Jul 17 11:09:43 2019 +0200
@@ -21,7 +21,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1563348893
+ModificationTime: 1563354308
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1679,10 +1679,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 64 32 8
+WinInfo: 10944 32 8
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1403
+BeginChars: 1114115 1404
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -13030,23 +13030,23 @@
Encoding: 183 183 125
Width: 614
VWidth: 2326
-Flags: WO
-LayerCount: 2
-Fore
-SplineSet
-115.193359375 841.811523438 m 1
- 498.806640625 841.811523438 l 1
- 549.806640625 841.811523438 l 1
- 549.806640625 790.811523438 l 1
- 549.806640625 415.188476562 l 1
- 549.806640625 364.188476562 l 1
- 498.806640625 364.188476562 l 1
- 115.193359375 364.188476562 l 1
- 64.193359375 364.188476562 l 1
- 64.193359375 415.188476562 l 1
- 64.193359375 790.811523438 l 1
- 64.193359375 841.811523438 l 1
- 115.193359375 841.811523438 l 1
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+115.193359375 841.811523438 m 1,0,-1
+ 498.806640625 841.811523438 l 1,1,-1
+ 549.806640625 841.811523438 l 1,2,-1
+ 549.806640625 790.811523438 l 1,3,-1
+ 549.806640625 415.188476562 l 1,4,-1
+ 549.806640625 364.188476562 l 1,5,-1
+ 498.806640625 364.188476562 l 1,6,-1
+ 115.193359375 364.188476562 l 1,7,-1
+ 64.193359375 364.188476562 l 1,8,-1
+ 64.193359375 415.188476562 l 1,9,-1
+ 64.193359375 790.811523438 l 1,10,-1
+ 64.193359375 841.811523438 l 1,11,-1
+ 115.193359375 841.811523438 l 1,0,-1
EndSplineSet
EndChar
@@ -69155,5 +69155,33 @@
547 440 l 1,19,-1
EndSplineSet
EndChar
+
+StartChar: uni2AFF
+Encoding: 11007 11007 1403
+Width: 1151
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+401 1525 m 1
+ 401 -415 l 1
+ 737 -415 l 1
+ 737 1525 l 1
+ 401 1525 l 1
+264 1721 m 1
+ 880 1721 l 1
+ 931 1721 l 1
+ 931 1670 l 1
+ 931 -558 l 1
+ 931 -609 l 1
+ 880 -609 l 1
+ 264 -609 l 1
+ 213 -609 l 1
+ 213 -558 l 1
+ 213 1670 l 1
+ 213 1721 l 1
+ 264 1721 l 1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/etc/symbols Wed Jul 17 09:40:43 2019 +0200
+++ b/etc/symbols Wed Jul 17 11:09:43 2019 +0200
@@ -278,6 +278,7 @@
\<succeq> code: 0x00227d group: relation
\<parallel> code: 0x002225 group: punctuation abbrev: ||
\<bar> code: 0x0000a6 group: punctuation abbrev: ||
+\<bbar> code: 0x002aff group: punctuation abbrev: ||
\<plusminus> code: 0x0000b1 group: operator
\<minusplus> code: 0x002213 group: operator
\<times> code: 0x0000d7 group: operator abbrev: <*>
--- a/lib/texinputs/isabellesym.sty Wed Jul 17 09:40:43 2019 +0200
+++ b/lib/texinputs/isabellesym.sty Wed Jul 17 11:09:43 2019 +0200
@@ -280,6 +280,7 @@
\newcommand{\isasymsucceq}{\isamath{\succeq}}
\newcommand{\isasymparallel}{\isamath{\parallel}}
\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymbbar}{\isamath{[\!]}}
\newcommand{\isasymplusminus}{\isamath{\pm}}
\newcommand{\isasymminusplus}{\isamath{\mp}}
\newcommand{\isasymtimes}{\isamath{\times}}
--- a/src/Pure/Admin/build_fonts.scala Wed Jul 17 09:40:43 2019 +0200
+++ b/src/Pure/Admin/build_fonts.scala Wed Jul 17 11:09:43 2019 +0200
@@ -31,6 +31,7 @@
0x204b, // FOOTNOTE
0x20ac, // Euro
0x2710, // pencil
+ 0x2aff, // n-ary Dijkstra choice
0xfb01, // ligature fi
0xfb02, // ligature fl
0xfffd, // replacement character