# HG changeset patch
# User wenzelm
# Date 1582992977 -3600
# Node ID a80fa14bccb826f0a2b899035325caa4f406658d
# Parent  5d62f797e40cb59a852aeb9826baa1a15d69c22d
more Isabelle/jEdit actions;

diff -r 5d62f797e40c -r a80fa14bccb8 NEWS
--- 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
diff -r 5d62f797e40c -r a80fa14bccb8 src/Tools/jEdit/src/actions.xml
--- 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);
diff -r 5d62f797e40c -r a80fa14bccb8 src/Tools/jEdit/src/isabelle.scala
--- 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)
+    }
+  }
 }
diff -r 5d62f797e40c -r a80fa14bccb8 src/Tools/jEdit/src/jEdit.props
--- 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