# HG changeset patch
# User wenzelm
# Date 1563354583 -7200
# Node ID 6c65447b8a64aee0e370e3abc372d0e33cb2b8bf
# Parent  b67737bc5bd19e49802154c04f358b65aef35a2a
added \<bbar>;

diff -r b67737bc5bd1 -r 6c65447b8a64 Admin/isabelle_fonts/IsabelleSymbols.sfd
--- 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
diff -r b67737bc5bd1 -r 6c65447b8a64 Admin/isabelle_fonts/IsabelleSymbolsBold.sfd
--- 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
diff -r b67737bc5bd1 -r 6c65447b8a64 etc/symbols
--- 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: <*>
diff -r b67737bc5bd1 -r 6c65447b8a64 lib/texinputs/isabellesym.sty
--- 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}}
diff -r b67737bc5bd1 -r 6c65447b8a64 src/Pure/Admin/build_fonts.scala
--- 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