--- 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)
+ }
}