src/Tools/jEdit/src/prover/Command.scala

   def markup_node(desc: String, begin: Int, end: Int, kind: MarkupNode.Kind) =
     new MarkupNode(this, begin, end, Nil, id,
                    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)
+  }
 }