--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Fri May 22 13:43:35 2009 +0200
@@ -212,6 +212,16 @@
gfx.setColor(saved_color)
}
+ override def getToolTipText(x: Int, y: Int) = {
+ val document = prover.document
+ val offset = from_current(document.id, text_area.xyToOffset(x, y))
+ val cmd = document.find_command_at(offset)
+ if (cmd != null) {
+ document.token_start(cmd.tokens.first)
+ cmd.type_at(offset - cmd.start(document))
+ } else null
+ }
+
/* BufferListener methods */
private var changes: List[Text.Change] = Nil