src/Pure/PIDE/rendering.scala
changeset 65149 9dccbebf4511
parent 65145 576d52aa0a78
child 65150 fa299b4e50c3
     1.1 --- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 20:31:30 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Mar 08 10:25:47 2017 +0100
     1.3 @@ -160,28 +160,9 @@
     1.4      Markup.SML_COMMENT -> Color.inner_comment)
     1.5  
     1.6  
     1.7 -  /* markup elements */
     1.8 -
     1.9 -  val active_elements =
    1.10 -    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.11 -      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
    1.12 +  /* tooltips */
    1.13  
    1.14 -  private val background_elements =
    1.15 -    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    1.16 -      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    1.17 -      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    1.18 -      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    1.19 -      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    1.20 -      Markup.Markdown_Item.name ++ active_elements
    1.21 -
    1.22 -  private val foreground_elements =
    1.23 -    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    1.24 -      Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.25 -
    1.26 -  private val semantic_completion_elements =
    1.27 -    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    1.28 -
    1.29 -  private val tooltip_descriptions =
    1.30 +  val tooltip_descriptions =
    1.31      Map(
    1.32        Markup.CITATION -> "citation",
    1.33        Markup.TOKEN_RANGE -> "inner syntax token",
    1.34 @@ -192,6 +173,28 @@
    1.35        Markup.TFREE -> "free type variable",
    1.36        Markup.TVAR -> "schematic type variable")
    1.37  
    1.38 +
    1.39 +  /* markup elements */
    1.40 +
    1.41 +  val active_elements =
    1.42 +    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.43 +      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
    1.44 +
    1.45 +  val background_elements =
    1.46 +    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    1.47 +      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    1.48 +      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    1.49 +      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    1.50 +      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    1.51 +      Markup.Markdown_Item.name ++ active_elements
    1.52 +
    1.53 +  val foreground_elements =
    1.54 +    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    1.55 +      Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.56 +
    1.57 +  val semantic_completion_elements =
    1.58 +    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    1.59 +
    1.60    val tooltip_elements =
    1.61      Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    1.62        Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    1.63 @@ -202,9 +205,6 @@
    1.64      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    1.65        Markup.BAD)
    1.66  
    1.67 -  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.68 -    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    1.69 -
    1.70    val caret_focus_elements = Markup.Elements(Markup.ENTITY)
    1.71  
    1.72    val text_color_elements = Markup.Elements(text_color.keySet)
    1.73 @@ -251,116 +251,6 @@
    1.74        }).headOption.map(_.info)
    1.75  
    1.76  
    1.77 -  /* tooltips */
    1.78 -
    1.79 -  def timing_threshold: Double
    1.80 -
    1.81 -  private sealed case class Tooltip_Info(
    1.82 -    range: Text.Range,
    1.83 -    timing: Timing = Timing.zero,
    1.84 -    messages: List[Command.Results.Entry] = Nil,
    1.85 -    rev_infos: List[(Boolean, XML.Tree)] = Nil)
    1.86 -  {
    1.87 -    def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
    1.88 -    def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
    1.89 -    {
    1.90 -      val r = snapshot.convert(r0)
    1.91 -      if (range == r) copy(messages = (serial -> tree) :: messages)
    1.92 -      else copy(range = r, messages = List(serial -> tree))
    1.93 -    }
    1.94 -    def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
    1.95 -    {
    1.96 -      val r = snapshot.convert(r0)
    1.97 -      if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
    1.98 -      else copy (range = r, rev_infos = List(important -> tree))
    1.99 -    }
   1.100 -    def infos(important: Boolean): List[XML.Tree] =
   1.101 -      rev_infos.filter(p => p._1 == important).reverse.map(_._2)
   1.102 -  }
   1.103 -
   1.104 -  def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   1.105 -  {
   1.106 -    val results =
   1.107 -      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ =>
   1.108 -        {
   1.109 -          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
   1.110 -
   1.111 -          case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   1.112 -          if Rendering.tooltip_message_elements(name) && body.nonEmpty =>
   1.113 -            Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body)))
   1.114 -
   1.115 -          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
   1.116 -          if kind != "" && kind != Markup.ML_DEF =>
   1.117 -            val kind1 = Word.implode(Word.explode('_', kind))
   1.118 -            val txt1 =
   1.119 -              if (name == "") kind1
   1.120 -              else if (kind1 == "") quote(name)
   1.121 -              else kind1 + " " + quote(name)
   1.122 -            val txt2 =
   1.123 -              if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold)
   1.124 -                "\n" + info.timing.message
   1.125 -              else ""
   1.126 -            Some(info + (r0, true, XML.Text(txt1 + txt2)))
   1.127 -
   1.128 -          case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
   1.129 -            val file = resources.append_file(snapshot.node_name.master_dir, name)
   1.130 -            val text =
   1.131 -              if (name == file) "file " + quote(file)
   1.132 -              else "path " + quote(name) + "\nfile " + quote(file)
   1.133 -            Some(info + (r0, true, XML.Text(text)))
   1.134 -
   1.135 -          case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
   1.136 -            val text = "doc " + quote(name)
   1.137 -            Some(info + (r0, true, XML.Text(text)))
   1.138 -
   1.139 -          case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
   1.140 -            Some(info + (r0, true, XML.Text("URL " + quote(name))))
   1.141 -
   1.142 -          case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
   1.143 -          if name == Markup.SORTING || name == Markup.TYPING =>
   1.144 -            Some(info + (r0, true, Rendering.pretty_typing("::", body)))
   1.145 -
   1.146 -          case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   1.147 -            Some(info + (r0, true, Pretty.block(0, body)))
   1.148 -
   1.149 -          case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   1.150 -            Some(info + (r0, false, Rendering.pretty_typing("ML:", body)))
   1.151 -
   1.152 -          case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
   1.153 -            val text =
   1.154 -              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   1.155 -              else "breakpoint (disabled)"
   1.156 -            Some(info + (r0, true, XML.Text(text)))
   1.157 -
   1.158 -          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   1.159 -            val lang = Word.implode(Word.explode('_', language))
   1.160 -            Some(info + (r0, true, XML.Text("language: " + lang)))
   1.161 -
   1.162 -          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
   1.163 -            val descr = if (kind == "") "expression" else "expression: " + kind
   1.164 -            Some(info + (r0, true, XML.Text(descr)))
   1.165 -
   1.166 -          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   1.167 -            Some(info + (r0, true, XML.Text("Markdown: paragraph")))
   1.168 -          case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
   1.169 -            Some(info + (r0, true, XML.Text("Markdown: " + kind)))
   1.170 -
   1.171 -          case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
   1.172 -            Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
   1.173 -        }).map(_.info)
   1.174 -
   1.175 -    if (results.isEmpty) None
   1.176 -    else {
   1.177 -      val r = Text.Range(results.head.range.start, results.last.range.stop)
   1.178 -      val all_tips =
   1.179 -        Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
   1.180 -        results.flatMap(res => res.infos(true)) :::
   1.181 -        results.flatMap(res => res.infos(false)).lastOption.toList
   1.182 -      if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
   1.183 -    }
   1.184 -  }
   1.185 -
   1.186 -
   1.187    /* text background */
   1.188  
   1.189    def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
   1.190 @@ -495,4 +385,114 @@
   1.191        color <- Rendering.message_underline_color.get(pri)
   1.192      } yield Text.Info(r, color)
   1.193    }
   1.194 +
   1.195 +
   1.196 +  /* tooltips */
   1.197 +
   1.198 +  def timing_threshold: Double
   1.199 +
   1.200 +  private sealed case class Tooltip_Info(
   1.201 +    range: Text.Range,
   1.202 +    timing: Timing = Timing.zero,
   1.203 +    messages: List[Command.Results.Entry] = Nil,
   1.204 +    rev_infos: List[(Boolean, XML.Tree)] = Nil)
   1.205 +  {
   1.206 +    def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
   1.207 +    def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
   1.208 +    {
   1.209 +      val r = snapshot.convert(r0)
   1.210 +      if (range == r) copy(messages = (serial -> tree) :: messages)
   1.211 +      else copy(range = r, messages = List(serial -> tree))
   1.212 +    }
   1.213 +    def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
   1.214 +    {
   1.215 +      val r = snapshot.convert(r0)
   1.216 +      if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
   1.217 +      else copy (range = r, rev_infos = List(important -> tree))
   1.218 +    }
   1.219 +    def infos(important: Boolean): List[XML.Tree] =
   1.220 +      rev_infos.filter(p => p._1 == important).reverse.map(_._2)
   1.221 +  }
   1.222 +
   1.223 +  def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   1.224 +  {
   1.225 +    val results =
   1.226 +      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ =>
   1.227 +        {
   1.228 +          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
   1.229 +
   1.230 +          case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   1.231 +          if Rendering.tooltip_message_elements(name) && body.nonEmpty =>
   1.232 +            Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body)))
   1.233 +
   1.234 +          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
   1.235 +          if kind != "" && kind != Markup.ML_DEF =>
   1.236 +            val kind1 = Word.implode(Word.explode('_', kind))
   1.237 +            val txt1 =
   1.238 +              if (name == "") kind1
   1.239 +              else if (kind1 == "") quote(name)
   1.240 +              else kind1 + " " + quote(name)
   1.241 +            val txt2 =
   1.242 +              if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold)
   1.243 +                "\n" + info.timing.message
   1.244 +              else ""
   1.245 +            Some(info + (r0, true, XML.Text(txt1 + txt2)))
   1.246 +
   1.247 +          case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
   1.248 +            val file = resources.append_file(snapshot.node_name.master_dir, name)
   1.249 +            val text =
   1.250 +              if (name == file) "file " + quote(file)
   1.251 +              else "path " + quote(name) + "\nfile " + quote(file)
   1.252 +            Some(info + (r0, true, XML.Text(text)))
   1.253 +
   1.254 +          case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
   1.255 +            val text = "doc " + quote(name)
   1.256 +            Some(info + (r0, true, XML.Text(text)))
   1.257 +
   1.258 +          case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
   1.259 +            Some(info + (r0, true, XML.Text("URL " + quote(name))))
   1.260 +
   1.261 +          case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
   1.262 +          if name == Markup.SORTING || name == Markup.TYPING =>
   1.263 +            Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body)))
   1.264 +
   1.265 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   1.266 +            Some(info + (r0, true, Pretty.block(0, body)))
   1.267 +
   1.268 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   1.269 +            Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
   1.270 +
   1.271 +          case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
   1.272 +            val text =
   1.273 +              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   1.274 +              else "breakpoint (disabled)"
   1.275 +            Some(info + (r0, true, XML.Text(text)))
   1.276 +
   1.277 +          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   1.278 +            val lang = Word.implode(Word.explode('_', language))
   1.279 +            Some(info + (r0, true, XML.Text("language: " + lang)))
   1.280 +
   1.281 +          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
   1.282 +            val descr = if (kind == "") "expression" else "expression: " + kind
   1.283 +            Some(info + (r0, true, XML.Text(descr)))
   1.284 +
   1.285 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   1.286 +            Some(info + (r0, true, XML.Text("Markdown: paragraph")))
   1.287 +          case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
   1.288 +            Some(info + (r0, true, XML.Text("Markdown: " + kind)))
   1.289 +
   1.290 +          case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
   1.291 +            Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
   1.292 +        }).map(_.info)
   1.293 +
   1.294 +    if (results.isEmpty) None
   1.295 +    else {
   1.296 +      val r = Text.Range(results.head.range.start, results.last.range.stop)
   1.297 +      val all_tips =
   1.298 +        Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
   1.299 +        results.flatMap(res => res.infos(true)) :::
   1.300 +        results.flatMap(res => res.infos(false)).lastOption.toList
   1.301 +      if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
   1.302 +    }
   1.303 +  }
   1.304  }