# HG changeset patch
# User wenzelm
# Date 1502718048 -7200
# Node ID e20ce089a14d2194ee39f790c9bfa30c9b39a239
# Parent  96ad7d5ff6137d58ec882275c1f09b387da4b6b3
proper tooltip (amending fd8a65b026f1);

diff -r 96ad7d5ff613 -r e20ce089a14d 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