tuned markup;
authorwenzelm
Fri, 01 Apr 2016 15:27:59 +0200
changeset 62787 f90a9fe3329f
parent 62786 2461a58b3587
child 62788 374820748c70
tuned markup;
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 =>