src/Tools/jEdit/src/rendering.scala
changeset 51496 cb677987b7e3
parent 50895 3a1edaa0dc6d
child 51574 2b58d7b139d6
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 23 16:46:09 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 23 19:39:31 2013 +0100
     1.3 @@ -275,22 +275,30 @@
     1.4      (Command.Results.empty /: results)(_ ++ _)
     1.5    }
     1.6  
     1.7 -  def tooltip_message(range: Text.Range): XML.Body =
     1.8 +  def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
     1.9    {
    1.10 -    val msgs =
    1.11 -      Command.Results.merge(
    1.12 -        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
    1.13 -          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    1.14 -          {
    1.15 -            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    1.16 -            if name == Markup.WRITELN ||
    1.17 -                name == Markup.WARNING ||
    1.18 -                name == Markup.ERROR =>
    1.19 -              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    1.20 -            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    1.21 -            if !body.isEmpty => msgs + (Document.new_id() -> msg)
    1.22 -          }).map(_.info))
    1.23 -    Pretty.separate(msgs.entries.map(_._2).toList)
    1.24 +    val results =
    1.25 +      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
    1.26 +        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
    1.27 +        {
    1.28 +          case (msgs, Text.Info(info_range,
    1.29 +            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    1.30 +          if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
    1.31 +            val entry: Command.Results.Entry =
    1.32 +              (serial -> XML.Elem(Markup(Markup.message(name), props), body))
    1.33 +            Text.Info(snapshot.convert(info_range), entry) :: msgs
    1.34 +
    1.35 +          case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    1.36 +          if !body.isEmpty =>
    1.37 +            val entry: Command.Results.Entry = (Document.new_id(), msg)
    1.38 +            Text.Info(snapshot.convert(info_range), entry) :: msgs
    1.39 +        }).toList.flatMap(_.info)
    1.40 +    if (results.isEmpty) None
    1.41 +    else {
    1.42 +      val r = Text.Range(results.head.range.start, results.last.range.stop)
    1.43 +      val msgs = Command.Results.make(results.map(_.info))
    1.44 +      Some(Text.Info(r, Pretty.separate(msgs.entries.map(_._2).toList)))
    1.45 +    }
    1.46    }
    1.47  
    1.48  
    1.49 @@ -317,12 +325,15 @@
    1.50    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.51      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    1.52  
    1.53 -  def tooltip(range: Text.Range): XML.Body =
    1.54 +  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    1.55    {
    1.56 -    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
    1.57 +    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r0: Text.Range, p: (Boolean, XML.Tree)) =
    1.58 +    {
    1.59 +      val r = snapshot.convert(r0)
    1.60        if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
    1.61 +    }
    1.62  
    1.63 -    val tips =
    1.64 +    val results =
    1.65        snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
    1.66          range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
    1.67          {
    1.68 @@ -340,11 +351,15 @@
    1.69              add(prev, r, (false, pretty_typing("ML:", body)))
    1.70            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
    1.71            if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
    1.72 -        }).toList.flatMap(_.info.info)
    1.73 +        }).toList.map(_.info)
    1.74  
    1.75 -    val all_tips =
    1.76 -      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
    1.77 -    Library.separate(Pretty.FBreak, all_tips.toList)
    1.78 +    results.flatMap(_.info) match {
    1.79 +      case Nil => None
    1.80 +      case tips =>
    1.81 +        val r = Text.Range(results.head.range.start, results.last.range.stop)
    1.82 +        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
    1.83 +        Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
    1.84 +    }
    1.85    }
    1.86  
    1.87    val tooltip_margin: Int = options.int("jedit_tooltip_margin")