# HG changeset patch
# User immler@in.tum.de
# Date 1242992615 -7200
# Node ID cdf914c78ff2aa6d37543f650fba6c30fb36b5b8
# Parent  8a70c2de32d313662df659e0da07a4bdf8c23184
ML types in tooltip

diff -r 8a70c2de32d3 -r cdf914c78ff2 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri May 22 13:43:35 2009 +0200
@@ -33,7 +33,7 @@
     if (prover_setup.isDefined) {
         val document = prover_setup.get.prover.document
         for (command <- document.commands)
-          data.root.add(command.highlight_node.swing_node(document))
+          data.root.add(command.markup_root.swing_node(document))
         
         if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     } else {
diff -r 8a70c2de32d3 -r cdf914c78ff2 src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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
diff -r 8a70c2de32d3 -r cdf914c78ff2 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:35 2009 +0200
@@ -99,4 +99,11 @@
                    if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
                    desc, kind)
 
+  def type_at(pos: Int): String = {
+    val types = markup_root.filter(_.kind match {case MarkupNode.TypeNode() => true case _ => false})
+    types.flatten(_.flatten).
+      find(t => t.start <= pos && t.stop > pos).
+      map(t => "\"" + t.content + "\" : " + t.desc).
+      getOrElse(null)
+  }
 }