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