src/Pure/PIDE/rendering.scala
changeset 65129 06a7c2d316cf
parent 65126 45ccb8ee3d08
child 65133 41f80c6978bc
     1.1 --- a/src/Pure/PIDE/rendering.scala	Mon Mar 06 11:48:06 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Mar 06 16:47:52 2017 +0100
     1.3 @@ -126,12 +126,16 @@
     1.4        Markup.TFREE -> "free type variable",
     1.5        Markup.TVAR -> "schematic type variable")
     1.6  
     1.7 -  private val tooltip_elements =
     1.8 +  val tooltip_elements =
     1.9      Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    1.10        Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    1.11        Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    1.12        Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    1.13  
    1.14 +  val tooltip_message_elements =
    1.15 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    1.16 +      Markup.BAD)
    1.17 +
    1.18    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.19      Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    1.20  
    1.21 @@ -168,93 +172,108 @@
    1.22  
    1.23    def timing_threshold: Double
    1.24  
    1.25 -  def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
    1.26 +  private sealed case class Tooltip_Info(
    1.27 +    range: Text.Range,
    1.28 +    timing: Timing = Timing.zero,
    1.29 +    messages: List[Command.Results.Entry] = Nil,
    1.30 +    rev_infos: List[(Boolean, XML.Tree)] = Nil)
    1.31    {
    1.32 -    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    1.33 -      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    1.34 +    def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
    1.35 +    def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
    1.36 +    {
    1.37 +      val r = snapshot.convert(r0)
    1.38 +      if (range == r) copy(messages = (serial -> tree) :: messages)
    1.39 +      else copy(range = r, messages = List(serial -> tree))
    1.40 +    }
    1.41 +    def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
    1.42      {
    1.43        val r = snapshot.convert(r0)
    1.44 -      val (t, info) = prev.info
    1.45 -      if (prev.range == r)
    1.46 -        Text.Info(r, (t, info :+ p))
    1.47 -      else Text.Info(r, (t, Vector(p)))
    1.48 +      if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
    1.49 +      else copy (range = r, rev_infos = List(important -> tree))
    1.50      }
    1.51 +    def infos(important: Boolean): List[XML.Tree] =
    1.52 +      rev_infos.filter(p => p._1 == important).reverse.map(_._2)
    1.53 +  }
    1.54  
    1.55 +  def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
    1.56 +  {
    1.57      val results =
    1.58 -      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    1.59 -        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
    1.60 +      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ =>
    1.61          {
    1.62 -          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    1.63 -            Some(Text.Info(r, (t1 + t2, info)))
    1.64 +          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
    1.65  
    1.66 -          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
    1.67 +          case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
    1.68 +          if Rendering.tooltip_message_elements(name) && body.nonEmpty =>
    1.69 +            Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body)))
    1.70 +
    1.71 +          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
    1.72            if kind != "" && kind != Markup.ML_DEF =>
    1.73              val kind1 = Word.implode(Word.explode('_', kind))
    1.74              val txt1 =
    1.75                if (name == "") kind1
    1.76                else if (kind1 == "") quote(name)
    1.77                else kind1 + " " + quote(name)
    1.78 -            val t = prev.info._1
    1.79              val txt2 =
    1.80 -              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
    1.81 -                "\n" + t.message
    1.82 +              if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold)
    1.83 +                "\n" + info.timing.message
    1.84                else ""
    1.85 -            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    1.86 +            Some(info + (r0, true, XML.Text(txt1 + txt2)))
    1.87  
    1.88 -          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
    1.89 +          case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
    1.90              val file = resources.append_file(snapshot.node_name.master_dir, name)
    1.91              val text =
    1.92                if (name == file) "file " + quote(file)
    1.93                else "path " + quote(name) + "\nfile " + quote(file)
    1.94 -            Some(add(prev, r, (true, XML.Text(text))))
    1.95 +            Some(info + (r0, true, XML.Text(text)))
    1.96  
    1.97 -          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
    1.98 +          case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
    1.99              val text = "doc " + quote(name)
   1.100 -            Some(add(prev, r, (true, XML.Text(text))))
   1.101 +            Some(info + (r0, true, XML.Text(text)))
   1.102  
   1.103 -          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   1.104 -            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   1.105 +          case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
   1.106 +            Some(info + (r0, true, XML.Text("URL " + quote(name))))
   1.107  
   1.108 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   1.109 +          case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
   1.110            if name == Markup.SORTING || name == Markup.TYPING =>
   1.111 -            Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
   1.112 +            Some(info + (r0, true, Rendering.pretty_typing("::", body)))
   1.113  
   1.114 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   1.115 -            Some(add(prev, r, (true, Pretty.block(0, body))))
   1.116 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   1.117 +            Some(info + (r0, true, Pretty.block(0, body)))
   1.118  
   1.119 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   1.120 -            Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
   1.121 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   1.122 +            Some(info + (r0, false, Rendering.pretty_typing("ML:", body)))
   1.123  
   1.124 -          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   1.125 +          case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
   1.126              val text =
   1.127                if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   1.128                else "breakpoint (disabled)"
   1.129 -            Some(add(prev, r, (true, XML.Text(text))))
   1.130 +            Some(info + (r0, true, XML.Text(text)))
   1.131  
   1.132 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   1.133 +          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   1.134              val lang = Word.implode(Word.explode('_', language))
   1.135 -            Some(add(prev, r, (true, XML.Text("language: " + lang))))
   1.136 +            Some(info + (r0, true, XML.Text("language: " + lang)))
   1.137  
   1.138 -          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   1.139 +          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
   1.140              val descr = if (kind == "") "expression" else "expression: " + kind
   1.141 -            Some(add(prev, r, (true, XML.Text(descr))))
   1.142 +            Some(info + (r0, true, XML.Text(descr)))
   1.143  
   1.144 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   1.145 -            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   1.146 -          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   1.147 -            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   1.148 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   1.149 +            Some(info + (r0, true, XML.Text("Markdown: paragraph")))
   1.150 +          case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
   1.151 +            Some(info + (r0, true, XML.Text("Markdown: " + kind)))
   1.152  
   1.153 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   1.154 -            Rendering.tooltip_descriptions.get(name).
   1.155 -              map(descr => add(prev, r, (true, XML.Text(descr))))
   1.156 +          case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
   1.157 +            Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
   1.158          }).map(_.info)
   1.159  
   1.160 -    results.map(_.info).flatMap(res => res._2.toList) match {
   1.161 -      case Nil => None
   1.162 -      case tips =>
   1.163 -        val r = Text.Range(results.head.range.start, results.last.range.stop)
   1.164 -        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   1.165 -        Some(Text.Info(r, all_tips))
   1.166 +    if (results.isEmpty) None
   1.167 +    else {
   1.168 +      val r = Text.Range(results.head.range.start, results.last.range.stop)
   1.169 +      val all_tips =
   1.170 +        Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
   1.171 +        results.flatMap(res => res.infos(true)) :::
   1.172 +        results.flatMap(res => res.infos(false)).lastOption.toList
   1.173 +      if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
   1.174      }
   1.175    }
   1.176  
   1.177 @@ -380,8 +399,8 @@
   1.178  
   1.179    /* message underline color */
   1.180  
   1.181 -  def message_underline_color(
   1.182 -    elements: Markup.Elements, range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   1.183 +  def message_underline_color(elements: Markup.Elements, range: Text.Range)
   1.184 +    : List[Text.Info[Rendering.Color.Value]] =
   1.185    {
   1.186      val results =
   1.187        snapshot.cumulate[Int](range, 0, elements, _ =>