# HG changeset patch # User wenzelm # Date 1483353735 -3600 # Node ID 155bf86321041d2006ad8fbb1f93ee624276ba79 # Parent 54afac94f52b0013b17ab21c08d90d7929d67871 clarified multiple tooltips; diff -r 54afac94f52b -r 155bf8632104 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Jan 02 11:26:26 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Jan 02 11:42:15 2017 +0100 @@ -73,7 +73,7 @@ def tooltip_margin: Int def timing_threshold: Double - def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] = + def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] = { def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])], r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] = @@ -159,7 +159,7 @@ case tips => val r = Text.Range(results.head.range.start, results.last.range.stop) val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2) - Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips))) + Some(Text.Info(r, all_tips)) } } } diff -r 54afac94f52b -r 155bf8632104 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Mon Jan 02 11:26:26 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Mon Jan 02 11:42:15 2017 +0100 @@ -280,12 +280,13 @@ val result = for { (rendering, offset) <- rendering_offset(node_pos) - info <- rendering.tooltip(Text.Range(offset, offset + 1)) + info <- rendering.tooltips(Text.Range(offset, offset + 1)) } yield { val doc = rendering.model.doc val range = doc.range(info.range) - val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin) - (range, List(s)) + val contents = + info.info.map(tree => Pretty.string_of(List(tree), margin = rendering.tooltip_margin)) + (range, contents) } channel.write(Protocol.Hover.reply(id, result)) } diff -r 54afac94f52b -r 155bf8632104 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Jan 02 11:26:26 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Jan 02 11:42:15 2017 +0100 @@ -525,6 +525,10 @@ def tooltip_margin: Int = options.int("jedit_tooltip_margin") def timing_threshold: Double = options.real("jedit_timing_threshold") + def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] = + tooltips(range).map({ case Text.Info(r, all_tips) => + Text.Info(r, Library.separate(Pretty.fbrk, all_tips)) }) + lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))