src/Tools/jEdit/src/proofdocument/session.scala

     def handle_result(result: Isabelle_Process.Result)
     {
       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)
         }
       if (target.isDefined) target.get.consume(this, result.message)
       else if (result.kind == Isabelle_Process.Kind.STATUS) {