src/Tools/jEdit/src/proofdocument/session.scala
changeset 34817 b4efd0ef2f3e
parent 34816 d33312514220
child 34818 7df68a8f0e3e
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:18:50 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:26:08 2009 +0100
@@ -106,7 +106,7 @@
       raw_results.event(result)
 
       val target: Option[Session.Entity] =
-        Position.id_of(result.props) match {
+        Position.get_id(result.props) match {
           case None => None
           case Some(id) => entities.get(id)
         }