--- a/NEWS Sat Feb 29 16:38:59 2020 +0100
+++ b/NEWS Sat Feb 29 17:16:17 2020 +0100
@@ -55,6 +55,10 @@
*** Isabelle/jEdit Prover IDE ***
+* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
+tooltip message popups, corresponding to mouse hovering with/without the
+CONTROL/COMMAND key pressed.
+
* Prover IDE startup is now much faster, because theory dependencies are
no longer explored in advance. The overall session structure with its
declarations of 'directories' is sufficient to locate theory files. Thus
--- a/src/Tools/jEdit/src/actions.xml Sat Feb 29 16:38:59 2020 +0100
+++ b/src/Tools/jEdit/src/actions.xml Sat Feb 29 17:16:17 2020 +0100
@@ -77,6 +77,16 @@
isabelle.jedit.Isabelle.complete(view, false);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.tooltip">
+ <CODE>
+ isabelle.jedit.Isabelle.show_tooltip(view, true);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.message">
+ <CODE>
+ isabelle.jedit.Isabelle.show_tooltip(view, false);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.complete-word">
<CODE>
isabelle.jedit.Isabelle.complete(view, true);
--- a/src/Tools/jEdit/src/isabelle.scala Sat Feb 29 16:38:59 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Feb 29 17:16:17 2020 +0100
@@ -9,7 +9,7 @@
import isabelle._
-import java.awt.Frame
+import java.awt.{Frame, Point}
import scala.swing.CheckBox
import scala.swing.event.ButtonClicked
@@ -515,4 +515,26 @@
dismissed
}
+
+
+ /* tooltips */
+
+ def show_tooltip(view: View, control: Boolean)
+ {
+ GUI_Thread.require {}
+
+ val text_area = view.getTextArea
+ val painter = text_area.getPainter
+ val caret_range = JEdit_Lib.caret_range(text_area)
+ for {
+ doc_view <- Document_View.get(text_area)
+ rendering = doc_view.get_rendering()
+ tip <- rendering.tooltip(caret_range, control)
+ loc0 <- Option(text_area.offsetToXY(caret_range.start))
+ } {
+ val loc = new Point(loc0.x, loc0.y + painter.getLineHeight / 2)
+ val results = rendering.snapshot.command_results(tip.range)
+ Pretty_Tooltip(view, painter, loc, rendering, results, tip)
+ }
+ }
}
--- a/src/Tools/jEdit/src/jEdit.props Sat Feb 29 16:38:59 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Sat Feb 29 17:16:17 2020 +0100
@@ -229,6 +229,8 @@
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
isabelle.increase-font-size2.shortcut=C+EQUALS
+isabelle.message.label=Show message
+isabelle.message.shortcut=CS+m
isabelle.newline.label=Newline with indentation of Isabelle keywords
isabelle.newline.shortcut=ENTER
isabelle.options.label=Isabelle options
@@ -246,6 +248,8 @@
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
isabelle.toggle-node-required.label=Toggle node required
isabelle.toggle-node-required.shortcut=C+e SPACE
+isabelle.tooltip.label=Show tooltip
+isabelle.tooltip.shortcut=CS+b
isabelle.update-state.label=Update state output
isabelle.update-state.shortcut=S+ENTER
lang.usedefaultlocale=false