69 |
69 |
70 /* protocol handler */ |
70 /* protocol handler */ |
71 |
71 |
72 class Invoke_Scala extends Session.Protocol_Handler |
72 class Invoke_Scala extends Session.Protocol_Handler |
73 { |
73 { |
|
74 private var session: Session = null |
74 private var futures = Map.empty[String, Future[Unit]] |
75 private var futures = Map.empty[String, Future[Unit]] |
75 |
76 |
76 private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = |
77 override def init(init_session: Session): Unit = |
|
78 synchronized { session = init_session } |
|
79 |
|
80 private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = |
77 synchronized |
81 synchronized |
78 { |
82 { |
79 if (futures.isDefinedAt(id)) { |
83 if (futures.isDefinedAt(id)) { |
80 prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res) |
84 session.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res) |
81 futures -= id |
85 futures -= id |
82 } |
86 } |
83 } |
87 } |
84 |
88 |
85 private def cancel(prover: Prover, id: String, future: Future[Unit]) |
89 private def cancel(id: String, future: Future[Unit]) |
86 { |
90 { |
87 future.cancel |
91 future.cancel |
88 fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "") |
92 fulfill(id, Invoke_Scala.Tag.INTERRUPT, "") |
89 } |
93 } |
90 |
94 |
91 private def invoke_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized |
95 private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized |
92 { |
96 { |
93 msg.properties match { |
97 msg.properties match { |
94 case Markup.Invoke_Scala(name, id) => |
98 case Markup.Invoke_Scala(name, id) => |
95 futures += (id -> |
99 futures += (id -> |
96 Future.fork { |
100 Future.fork { |
97 val (tag, result) = Invoke_Scala.method(name, msg.text) |
101 val (tag, result) = Invoke_Scala.method(name, msg.text) |
98 fulfill(prover, id, tag, result) |
102 fulfill(id, tag, result) |
99 }) |
103 }) |
100 true |
104 true |
101 case _ => false |
105 case _ => false |
102 } |
106 } |
103 } |
107 } |
104 |
108 |
105 private def cancel_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized |
109 private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized |
106 { |
110 { |
107 msg.properties match { |
111 msg.properties match { |
108 case Markup.Cancel_Scala(id) => |
112 case Markup.Cancel_Scala(id) => |
109 futures.get(id) match { |
113 futures.get(id) match { |
110 case Some(future) => cancel(prover, id, future) |
114 case Some(future) => cancel(id, future) |
111 case None => |
115 case None => |
112 } |
116 } |
113 true |
117 true |
114 case _ => false |
118 case _ => false |
115 } |
119 } |
116 } |
120 } |
117 |
121 |
118 override def stop(prover: Prover): Unit = synchronized |
122 override def exit(): Unit = synchronized |
119 { |
123 { |
120 for ((id, future) <- futures) cancel(prover, id, future) |
124 for ((id, future) <- futures) cancel(id, future) |
121 futures = Map.empty |
125 futures = Map.empty |
122 } |
126 } |
123 |
127 |
124 val functions = Map( |
128 val functions = |
125 Markup.INVOKE_SCALA -> invoke_scala _, |
129 List( |
126 Markup.CANCEL_SCALA -> cancel_scala _) |
130 Markup.INVOKE_SCALA -> invoke_scala _, |
|
131 Markup.CANCEL_SCALA -> cancel_scala _) |
127 } |
132 } |