# HG changeset patch
# User wenzelm
# Date 1392669461 -3600
# Node ID 76979adf0b96c8fdf21f493f21eac9dcea825efc
# Parent  4a9f76263ece341abc636f364881d323fa562472
always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);

diff -r 4a9f76263ece -r 76979adf0b96 etc/symbols
--- a/etc/symbols	Mon Feb 17 20:54:03 2014 +0100
+++ b/etc/symbols	Mon Feb 17 21:37:41 2014 +0100
@@ -350,6 +350,7 @@
 \<newline>              code: 0x0023ce
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
+\<here>                 code: 0x002302  font: IsabelleText
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
 \<^bold>                code: 0x002759  group: control  font: IsabelleText
diff -r 4a9f76263ece -r 76979adf0b96 lib/fonts/IsabelleText.sfd
--- a/lib/fonts/IsabelleText.sfd	Mon Feb 17 20:54:03 2014 +0100
+++ b/lib/fonts/IsabelleText.sfd	Mon Feb 17 21:37:41 2014 +0100
@@ -19,7 +19,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050361371
-ModificationTime: 1389823475
+ModificationTime: 1392668982
 PfmFamily: 17
 TTFWeight: 400
 TTFWidth: 5
@@ -2240,9 +2240,9 @@
 DisplaySize: -48
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 9104 16 10
+WinInfo: 8912 16 10
 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 1095
+BeginChars: 1114189 1096
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -55572,5 +55572,27 @@
  893 663 l 1,9,-1
 EndSplineSet
 EndChar
+
+StartChar: house
+Encoding: 8962 8962 1095
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+146.5 0 m 9,0,-1
+ 146.5 647 l 25,1,-1
+ 616 1220 l 25,2,-1
+ 1086.5 647 l 25,3,-1
+ 1086.5 0 l 17,4,-1
+ 146.5 0 l 9,0,-1
+268.5 122 m 17,5,-1
+ 964.5 122 l 9,6,-1
+ 964.5 591 l 25,7,-1
+ 616 1018 l 25,8,-1
+ 268.5 591 l 25,9,-1
+ 268.5 122 l 17,5,-1
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont
diff -r 4a9f76263ece -r 76979adf0b96 lib/fonts/IsabelleText.ttf
Binary file lib/fonts/IsabelleText.ttf has changed
diff -r 4a9f76263ece -r 76979adf0b96 lib/fonts/IsabelleTextBold.sfd
--- a/lib/fonts/IsabelleTextBold.sfd	Mon Feb 17 20:54:03 2014 +0100
+++ b/lib/fonts/IsabelleTextBold.sfd	Mon Feb 17 21:37:41 2014 +0100
@@ -19,7 +19,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050374980
-ModificationTime: 1389823579
+ModificationTime: 1392669044
 PfmFamily: 17
 TTFWeight: 700
 TTFWidth: 5
@@ -1674,8 +1674,8 @@
 DisplaySize: -48
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 9072 16 10
-BeginChars: 1114112 1084
+WinInfo: 8928 16 10
+BeginChars: 1114112 1085
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -58502,5 +58502,27 @@
  1067 1072 l 1,9,-1
 EndSplineSet
 EndChar
+
+StartChar: house
+Encoding: 8962 8962 1084
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+110 0 m 9,0,-1
+ 110 682 l 25,1,-1
+ 616 1220 l 25,2,-1
+ 1123 682 l 25,3,-1
+ 1123 0 l 17,4,-1
+ 110 0 l 9,0,-1
+298 187 m 17,5,-1
+ 935 187 l 9,6,-1
+ 935 625 l 25,7,-1
+ 616 959 l 25,8,-1
+ 298 625 l 25,9,-1
+ 298 187 l 17,5,-1
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont
diff -r 4a9f76263ece -r 76979adf0b96 lib/fonts/IsabelleTextBold.ttf
Binary file lib/fonts/IsabelleTextBold.ttf has changed
diff -r 4a9f76263ece -r 76979adf0b96 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Feb 17 20:54:03 2014 +0100
+++ b/src/Pure/General/position.ML	Mon Feb 17 21:37:41 2014 +0100
@@ -192,7 +192,7 @@
         (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
       | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
       | (NONE, SOME name) => "(file " ^ quote name ^ ")"
-      | _ => "");
+      | _ => if is_reported pos then "\\<here>" else "");
   in
     if null props then ""
     else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s