proper tooltip (amending fd8a65b026f1);
authorwenzelm
Mon, 14 Aug 2017 15:40:48 +0200
changeset 66416 e20ce089a14d
parent 66415 96ad7d5ff613
child 66417 1f46b6693b56
proper tooltip (amending fd8a65b026f1);
src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 15:30:26 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 15:40:48 2017 +0200
@@ -47,7 +47,7 @@
         val index_location = peer.indexToLocation(index)
         if (index >= 0 && in_checkbox(index_location, point))
           tooltip = "Mark as required for continuous checking"
-        if (index >= 0 && in_label(index_location, point))
+        else if (index >= 0 && in_label(index_location, point))
           tooltip = "theory " + quote(listData(index).theory)
         else
           tooltip = null