diff -r 42934bdf90ba -r de9bf8171626 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 19:01:34 2016 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 21:34:17 2016 +0200 @@ -110,15 +110,6 @@ fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods [] |> map Symbol.explode; -fun reports_of (xsym, pos: Position.T) = - (pos, Markup.expression) :: - (case xsym of - Delim _ => [(pos, Markup.literal)] - | Bg _ => [(pos, Markup.keyword3)] - | Brk _ => [(pos, Markup.keyword3)] - | En => [(pos, Markup.keyword3)] - | _ => []); - (** datatype mfix **) @@ -210,6 +201,18 @@ fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol); fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); +fun reports_of_block pos = + [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)]; + +fun reports_of (xsym, pos: Position.T) = + (case xsym of + Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)] + | Argument _ => [(pos, Markup.expression "mixfix argument")] + | Space _ => [(pos, Markup.expression "mixfix space")] + | Bg _ => reports_of_block pos + | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)] + | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]); + fun read_block_properties ss = let val props = read_properties ss; @@ -227,8 +230,12 @@ val unbreakable = get_bool Markup.unbreakableN props; val indent = get_nat Markup.indentN props; in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end - handle ERROR msg => error (msg ^ - Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 "")); + handle ERROR msg => + let + val reported_texts = + reports_of_block (#1 (Symbol_Pos.range ss)) + |> map (fn (p, m) => Markup.markup_report (Position.reported_text p m "")) + in error (msg ^ implode reported_texts) end; val read_block_indent = Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;