56 } |
56 } |
57 |
57 |
58 |
58 |
59 /* reported positions */ |
59 /* reported positions */ |
60 |
60 |
|
61 private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) |
|
62 private val exclude_pos = Set(Markup.LOCATION) |
|
63 |
61 def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] = |
64 def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] = |
62 { |
65 { |
63 def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = |
66 def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = |
64 tree match { |
67 tree match { |
65 case XML.Elem(Markup(name, Position.Id_Range(id, range)), body) |
68 case XML.Elem(Markup(name, Position.Id_Range(id, range)), body) |
66 if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) && |
69 if include_pos(name) && id == command_id => |
67 id == command_id => body.foldLeft(set + range)(reported) |
70 body.foldLeft(set + range)(reported) |
68 case XML.Elem(_, body) => body.foldLeft(set)(reported) |
71 case XML.Elem(Markup(name, _), body) if !exclude_pos(name) => |
69 case XML.Text(_) => set |
72 body.foldLeft(set)(reported) |
|
73 case _ => set |
70 } |
74 } |
71 reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties) |
75 val set = reported(Set.empty, message) |
|
76 if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties) |
|
77 else set |
72 } |
78 } |
73 } |
79 } |
74 |
80 |
75 |
81 |
76 trait Isar_Document extends Isabelle_Process |
82 trait Isar_Document extends Isabelle_Process |