src/Tools/jEdit/src/rendering.scala
changeset 50507 9605b0d93d1e
parent 50502 51408dde956f
child 50542 58bd88159f8f
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 19:53:55 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Dec 14 12:09:08 2012 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4      snapshot.select_markup(range, Some(active_include), command_state =>
     1.5          {
     1.6            case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
     1.7 -          if !command_state.results.isDefinedAt(serial) =>
     1.8 +          if !command_state.results.defined(serial) =>
     1.9              Text.Info(snapshot.convert(info_range), elem)
    1.10            case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
    1.11            if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
    1.12 @@ -269,24 +269,25 @@
    1.13      val results =
    1.14        snapshot.select_markup[Command.Results](range, None, command_state =>
    1.15          { case _ => command_state.results }).map(_.info)
    1.16 -    (Command.empty_results /: results)(_ ++ _)
    1.17 +    (Command.Results.empty /: results)(_ ++ _)
    1.18    }
    1.19  
    1.20    def tooltip_message(range: Text.Range): XML.Body =
    1.21    {
    1.22      val msgs =
    1.23 -      snapshot.cumulate_markup[Command.Results](range, Command.empty_results,
    1.24 -        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    1.25 -        {
    1.26 -          case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    1.27 -          if name == Markup.WRITELN ||
    1.28 -              name == Markup.WARNING ||
    1.29 -              name == Markup.ERROR =>
    1.30 -            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    1.31 -          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    1.32 -          if !body.isEmpty => msgs + (Document.new_id() -> msg)
    1.33 -        }).toList.flatMap(_.info)
    1.34 -    Pretty.separate(msgs.iterator.map(_._2).toList)
    1.35 +      Command.Results.merge(
    1.36 +        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
    1.37 +          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    1.38 +          {
    1.39 +            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    1.40 +            if name == Markup.WRITELN ||
    1.41 +                name == Markup.WARNING ||
    1.42 +                name == Markup.ERROR =>
    1.43 +              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    1.44 +            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    1.45 +            if !body.isEmpty => msgs + (Document.new_id() -> msg)
    1.46 +          }).map(_.info))
    1.47 +    Pretty.separate(msgs.entries.map(_._2).toList)
    1.48    }
    1.49  
    1.50  
    1.51 @@ -420,7 +421,7 @@
    1.52  
    1.53    def output_messages(st: Command.State): List[XML.Tree] =
    1.54    {
    1.55 -    st.results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
    1.56 +    st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
    1.57    }
    1.58  
    1.59