98 |
98 |
99 /* text messages */ |
99 /* text messages */ |
100 |
100 |
101 def text_messages( |
101 def text_messages( |
102 snapshot: Document.Snapshot, |
102 snapshot: Document.Snapshot, |
103 range: Text.Range = Text.Range.full |
103 range: Text.Range = Text.Range.full, |
|
104 filter: XML.Elem => Boolean = _ => true |
104 ): List[Text.Info[XML.Elem]] = { |
105 ): List[Text.Info[XML.Elem]] = { |
105 val results = |
106 val results = |
106 snapshot.cumulate[Vector[Command.Results.Entry]]( |
107 snapshot.cumulate[Vector[Command.Results.Entry]]( |
107 range, Vector.empty, message_elements, command_states => |
108 range, Vector.empty, message_elements, command_states => |
108 { |
109 { |
109 case (res, Text.Info(_, elem)) => |
110 case (res, Text.Info(_, elem)) => |
110 Command.State.get_result_proper(command_states, elem.markup.properties) |
111 if (filter(elem)) { |
111 .map(res :+ _) |
112 Command.State.get_result_proper(command_states, elem.markup.properties) |
|
113 .map(res :+ _) |
|
114 } |
|
115 else None |
112 }) |
116 }) |
113 |
117 |
114 var seen_serials = Set.empty[Long] |
118 var seen_serials = Set.empty[Long] |
115 def seen(i: Long): Boolean = { |
119 def seen(i: Long): Boolean = { |
116 val b = seen_serials(i) |
120 val b = seen_serials(i) |