src/Tools/jEdit/src/proofdocument/session.scala
changeset 34817 b4efd0ef2f3e
parent 34816 d33312514220
child 34818 7df68a8f0e3e
equal deleted inserted replaced
34816:d33312514220 34817:b4efd0ef2f3e
   104     def handle_result(result: Isabelle_Process.Result)
   104     def handle_result(result: Isabelle_Process.Result)
   105     {
   105     {
   106       raw_results.event(result)
   106       raw_results.event(result)
   107 
   107 
   108       val target: Option[Session.Entity] =
   108       val target: Option[Session.Entity] =
   109         Position.id_of(result.props) match {
   109         Position.get_id(result.props) match {
   110           case None => None
   110           case None => None
   111           case Some(id) => entities.get(id)
   111           case Some(id) => entities.get(id)
   112         }
   112         }
   113       if (target.isDefined) target.get.consume(this, result.message)
   113       if (target.isDefined) target.get.consume(this, result.message)
   114       else if (result.kind == Isabelle_Process.Kind.STATUS) {
   114       else if (result.kind == Isabelle_Process.Kind.STATUS) {