# HG changeset patch
# User wenzelm
# Date 1552134949 -3600
# Node ID 6dc5506ad44971ab6046b4a179d1d7f47bffa605
# Parent  dec7cc38a5dc754c91cbf9e61a8f7e00249f306d
added glyph for \<marker>;

diff -r dec7cc38a5dc -r 6dc5506ad449 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sat Mar 09 13:24:59 2019 +0100
+++ b/Admin/components/components.sha1	Sat Mar 09 13:35:49 2019 +0100
@@ -78,6 +78,7 @@
 bee32019e5d7cf096ef2ea1d836c732e9a7628cc  isabelle_fonts-20181124.tar.gz
 f249bc2c85bd2af9eee509de17187a766b74ab86  isabelle_fonts-20181129.tar.gz
 928b5320073d04d93bcc5bc4347b6d01632b9d45  isabelle_fonts-20190210.tar.gz
+dfcdf9a757b9dc36cee87f82533b43c58ba84abe  isabelle_fonts-20190309.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39  jdk-11.0.2+9.tar.gz
 71d19df63816e9be1c4c5eb44aea7a44cfadb319  jdk-11.tar.gz
diff -r dec7cc38a5dc -r 6dc5506ad449 Admin/components/main
--- a/Admin/components/main	Sat Mar 09 13:24:59 2019 +0100
+++ b/Admin/components/main	Sat Mar 09 13:35:49 2019 +0100
@@ -4,7 +4,7 @@
 csdp-6.x
 cvc4-1.5-4
 e-2.0-2
-isabelle_fonts-20190210
+isabelle_fonts-20190309
 jdk-11.0.2+9
 jedit_build-20190224
 jfreechart-1.5.0
diff -r dec7cc38a5dc -r 6dc5506ad449 etc/symbols
--- a/etc/symbols	Sat Mar 09 13:24:59 2019 +0100
+++ b/etc/symbols	Sat Mar 09 13:35:49 2019 +0100
@@ -359,6 +359,7 @@
 \<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
 \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
+\<marker>               code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<^latex>                               group: document  argument: cartouche
 \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
diff -r dec7cc38a5dc -r 6dc5506ad449 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Sat Mar 09 13:24:59 2019 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Sat Mar 09 13:35:49 2019 +0100
@@ -30,6 +30,7 @@
         0x203a,  // single guillemet
         0x204b,  // FOOTNOTE
         0x20ac,  // Euro
+        0x2710,  // pencil
         0xfb01,  // ligature fi
         0xfb02,  // ligature fl
         0xfffd,  // replacement character