500 { |
500 { |
501 val results = |
501 val results = |
502 snapshot.cumulate[List[Text.Info[Command.Results.Entry]]]( |
502 snapshot.cumulate[List[Text.Info[Command.Results.Entry]]]( |
503 range, Nil, JEdit_Rendering.tooltip_message_elements, _ => |
503 range, Nil, JEdit_Rendering.tooltip_message_elements, _ => |
504 { |
504 { |
505 case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body))) |
505 case (msgs, Text.Info(info_range, |
|
506 XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) |
506 if body.nonEmpty => |
507 if body.nonEmpty => |
507 val entry: Command.Results.Entry = (Document_ID.make(), msg) |
|
508 Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) |
|
509 |
|
510 case (msgs, Text.Info(info_range, |
|
511 XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) => |
|
512 val entry: Command.Results.Entry = |
508 val entry: Command.Results.Entry = |
513 serial -> XML.Elem(Markup(Markup.message(name), props), body) |
509 serial -> XML.Elem(Markup(Markup.message(name), props), body) |
514 Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) |
510 Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) |
515 |
511 |
516 case _ => None |
512 case _ => None |