# HG changeset patch
# User wenzelm
# Date 1383757476 -3600
# Node ID e358b79b533a4676cccbba0f034c055d0472fe60
# Parent  13bfdbcfbbfbb6632d069d749a4c344ba9fb9c9d
tuned tooltips;

diff -r 13bfdbcfbbfb -r e358b79b533a src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Thu Oct 17 17:14:06 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Nov 06 18:04:36 2013 +0100
@@ -105,7 +105,11 @@
   }
 
   private val query_label = new Label("Search criteria:") {
-    tooltip = "Search criteria for find operation"
+    tooltip =
+      GUI.tooltip_lines(List(
+        "Search criteria for find operation, e.g.",
+        "",
+        "  \"_ = _\" \"op +\" name: Group -name: monoid"))
   }
 
   private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
diff -r 13bfdbcfbbfb -r e358b79b533a src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Oct 17 17:14:06 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Nov 06 18:04:36 2013 +0100
@@ -136,7 +136,11 @@
   }
 
   private val provers_label = new Label("Provers:") {
-    tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")"
+    tooltip =
+      GUI.tooltip_lines(List(
+        "Automatic provers as space-separated list, e.g.",
+        "",
+        "  e spass remote_vampire"))
   }
 
   private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {