# HG changeset patch
# User wenzelm
# Date 1459517279 -7200
# Node ID f90a9fe3329fa2eb4e2bbb7ab4d6f84b5f1930ef
# Parent  2461a58b3587e00cb484ccf0b5d3148003e464c6
tuned markup;

diff -r 2461a58b3587 -r f90a9fe3329f src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 14:49:02 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 15:27:59 2016 +0200
@@ -109,12 +109,13 @@
   |> map Symbol.explode;
 
 fun reports_of (xsym, pos: Position.T) =
-  (case xsym of
-    Delim _ => [(pos, Markup.literal)]
-  | Bg _ => [(pos, Markup.keyword3)]
-  | Brk _ => [(pos, Markup.keyword3)]
-  | En => [(pos, Markup.keyword3)]
-  | _ => []);
+  (pos, Markup.expression) ::
+    (case xsym of
+      Delim _ => [(pos, Markup.literal)]
+    | Bg _ => [(pos, Markup.keyword3)]
+    | Brk _ => [(pos, Markup.keyword3)]
+    | En => [(pos, Markup.keyword3)]
+    | _ => []);
 
 
 
@@ -220,7 +221,9 @@
 
     val consistent = get_bool Markup.consistentN props;
     val indent = get_nat Markup.indentN props;
-  in Bg {markup = markup, consistent = consistent, indent = indent} end;
+  in Bg {markup = markup, consistent = consistent, indent = indent} end
+  handle ERROR msg => error (msg ^
+    Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 ""));
 
 val read_block_indent =
   map Symbol_Pos.symbol #> (fn ss =>