equal
deleted
inserted
replaced
87 future.cancel(true) |
87 future.cancel(true) |
88 fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "") |
88 fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "") |
89 } |
89 } |
90 |
90 |
91 private def invoke_scala( |
91 private def invoke_scala( |
92 prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized |
92 prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized |
93 { |
93 { |
94 msg.properties match { |
94 msg.properties match { |
95 case Markup.Invoke_Scala(name, id) => |
95 case Markup.Invoke_Scala(name, id) => |
96 futures += (id -> |
96 futures += (id -> |
97 default_thread_pool.submit(() => |
97 default_thread_pool.submit(() => |
103 case _ => false |
103 case _ => false |
104 } |
104 } |
105 } |
105 } |
106 |
106 |
107 private def cancel_scala( |
107 private def cancel_scala( |
108 prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized |
108 prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized |
109 { |
109 { |
110 msg.properties match { |
110 msg.properties match { |
111 case Markup.Cancel_Scala(id) => |
111 case Markup.Cancel_Scala(id) => |
112 futures.get(id) match { |
112 futures.get(id) match { |
113 case Some(future) => cancel(prover, id, future) |
113 case Some(future) => cancel(prover, id, future) |