# HG changeset patch # User wenzelm # Date 1488965147 -3600 # Node ID 9dccbebf4511b23bbac5c3e6d6aeb43ba3cac61e # Parent d232832b943ce73ab7ce0e70d2304b9bd73d4425 tuned; diff -r d232832b943c -r 9dccbebf4511 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Tue Mar 07 20:31:30 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Wed Mar 08 10:25:47 2017 +0100 @@ -160,28 +160,9 @@ Markup.SML_COMMENT -> Color.inner_comment) - /* markup elements */ - - val active_elements = - Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, - Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) + /* tooltips */ - private val background_elements = - Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + - Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + - Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + - Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + - Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + - Markup.Markdown_Item.name ++ active_elements - - private val foreground_elements = - Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, - Markup.CARTOUCHE, Markup.ANTIQUOTED) - - private val semantic_completion_elements = - Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) - - private val tooltip_descriptions = + val tooltip_descriptions = Map( Markup.CITATION -> "citation", Markup.TOKEN_RANGE -> "inner syntax token", @@ -192,6 +173,28 @@ Markup.TFREE -> "free type variable", Markup.TVAR -> "schematic type variable") + + /* markup elements */ + + val active_elements = + Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, + Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) + + val background_elements = + Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + + Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + + Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + + Markup.Markdown_Item.name ++ active_elements + + val foreground_elements = + Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, + Markup.CARTOUCHE, Markup.ANTIQUOTED) + + val semantic_completion_elements = + Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) + val tooltip_elements = Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, @@ -202,9 +205,6 @@ Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, Markup.BAD) - private def pretty_typing(kind: String, body: XML.Body): XML.Tree = - Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body) - val caret_focus_elements = Markup.Elements(Markup.ENTITY) val text_color_elements = Markup.Elements(text_color.keySet) @@ -251,116 +251,6 @@ }).headOption.map(_.info) - /* tooltips */ - - def timing_threshold: Double - - private sealed case class Tooltip_Info( - range: Text.Range, - timing: Timing = Timing.zero, - messages: List[Command.Results.Entry] = Nil, - rev_infos: List[(Boolean, XML.Tree)] = Nil) - { - def + (t: Timing): Tooltip_Info = copy(timing = timing + t) - def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = - { - val r = snapshot.convert(r0) - if (range == r) copy(messages = (serial -> tree) :: messages) - else copy(range = r, messages = List(serial -> tree)) - } - def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info = - { - val r = snapshot.convert(r0) - if (range == r) copy(rev_infos = (important -> tree) :: rev_infos) - else copy (range = r, rev_infos = List(important -> tree)) - } - def infos(important: Boolean): List[XML.Tree] = - rev_infos.filter(p => p._1 == important).reverse.map(_._2) - } - - def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = - { - val results = - snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ => - { - case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t) - - case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) - if Rendering.tooltip_message_elements(name) && body.nonEmpty => - Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body))) - - case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) - if kind != "" && kind != Markup.ML_DEF => - val kind1 = Word.implode(Word.explode('_', kind)) - val txt1 = - if (name == "") kind1 - else if (kind1 == "") quote(name) - else kind1 + " " + quote(name) - val txt2 = - if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold) - "\n" + info.timing.message - else "" - Some(info + (r0, true, XML.Text(txt1 + txt2))) - - case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => - val file = resources.append_file(snapshot.node_name.master_dir, name) - val text = - if (name == file) "file " + quote(file) - else "path " + quote(name) + "\nfile " + quote(file) - Some(info + (r0, true, XML.Text(text))) - - case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => - val text = "doc " + quote(name) - Some(info + (r0, true, XML.Text(text))) - - case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => - Some(info + (r0, true, XML.Text("URL " + quote(name)))) - - case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) - if name == Markup.SORTING || name == Markup.TYPING => - Some(info + (r0, true, Rendering.pretty_typing("::", body))) - - case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => - Some(info + (r0, true, Pretty.block(0, body))) - - case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => - Some(info + (r0, false, Rendering.pretty_typing("ML:", body))) - - case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => - val text = - if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" - else "breakpoint (disabled)" - Some(info + (r0, true, XML.Text(text))) - - case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) => - val lang = Word.implode(Word.explode('_', language)) - Some(info + (r0, true, XML.Text("language: " + lang))) - - case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => - val descr = if (kind == "") "expression" else "expression: " + kind - Some(info + (r0, true, XML.Text(descr))) - - case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => - Some(info + (r0, true, XML.Text("Markdown: paragraph"))) - case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => - Some(info + (r0, true, XML.Text("Markdown: " + kind))) - - case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => - Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc))) - }).map(_.info) - - if (results.isEmpty) None - else { - val r = Text.Range(results.head.range.start, results.last.range.stop) - val all_tips = - Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList ::: - results.flatMap(res => res.infos(true)) ::: - results.flatMap(res => res.infos(false)).lastOption.toList - if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) - } - } - - /* text background */ def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] = @@ -495,4 +385,114 @@ color <- Rendering.message_underline_color.get(pri) } yield Text.Info(r, color) } + + + /* tooltips */ + + def timing_threshold: Double + + private sealed case class Tooltip_Info( + range: Text.Range, + timing: Timing = Timing.zero, + messages: List[Command.Results.Entry] = Nil, + rev_infos: List[(Boolean, XML.Tree)] = Nil) + { + def + (t: Timing): Tooltip_Info = copy(timing = timing + t) + def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = + { + val r = snapshot.convert(r0) + if (range == r) copy(messages = (serial -> tree) :: messages) + else copy(range = r, messages = List(serial -> tree)) + } + def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info = + { + val r = snapshot.convert(r0) + if (range == r) copy(rev_infos = (important -> tree) :: rev_infos) + else copy (range = r, rev_infos = List(important -> tree)) + } + def infos(important: Boolean): List[XML.Tree] = + rev_infos.filter(p => p._1 == important).reverse.map(_._2) + } + + def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = + { + val results = + snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ => + { + case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t) + + case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) + if Rendering.tooltip_message_elements(name) && body.nonEmpty => + Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body))) + + case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) + if kind != "" && kind != Markup.ML_DEF => + val kind1 = Word.implode(Word.explode('_', kind)) + val txt1 = + if (name == "") kind1 + else if (kind1 == "") quote(name) + else kind1 + " " + quote(name) + val txt2 = + if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold) + "\n" + info.timing.message + else "" + Some(info + (r0, true, XML.Text(txt1 + txt2))) + + case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => + val file = resources.append_file(snapshot.node_name.master_dir, name) + val text = + if (name == file) "file " + quote(file) + else "path " + quote(name) + "\nfile " + quote(file) + Some(info + (r0, true, XML.Text(text))) + + case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => + val text = "doc " + quote(name) + Some(info + (r0, true, XML.Text(text))) + + case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => + Some(info + (r0, true, XML.Text("URL " + quote(name)))) + + case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) + if name == Markup.SORTING || name == Markup.TYPING => + Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body))) + + case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => + Some(info + (r0, true, Pretty.block(0, body))) + + case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => + Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body))) + + case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => + val text = + if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" + else "breakpoint (disabled)" + Some(info + (r0, true, XML.Text(text))) + + case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) => + val lang = Word.implode(Word.explode('_', language)) + Some(info + (r0, true, XML.Text("language: " + lang))) + + case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => + val descr = if (kind == "") "expression" else "expression: " + kind + Some(info + (r0, true, XML.Text(descr))) + + case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => + Some(info + (r0, true, XML.Text("Markdown: paragraph"))) + case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => + Some(info + (r0, true, XML.Text("Markdown: " + kind))) + + case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => + Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc))) + }).map(_.info) + + if (results.isEmpty) None + else { + val r = Text.Range(results.head.range.start, results.last.range.stop) + val all_tips = + Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList ::: + results.flatMap(res => res.infos(true)) ::: + results.flatMap(res => res.infos(false)).lastOption.toList + if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) + } + } }