wenzelm@36676
|
1 |
/* Title: Pure/System/session.scala
|
wenzelm@36676
|
2 |
Author: Makarius
|
wenzelm@38221
|
3 |
Options: :folding=explicit:collapseFolds=1:
|
wenzelm@36676
|
4 |
|
wenzelm@36676
|
5 |
Isabelle session, potentially with running prover.
|
wenzelm@36676
|
6 |
*/
|
wenzelm@34777
|
7 |
|
wenzelm@34871
|
8 |
package isabelle
|
wenzelm@34777
|
9 |
|
wenzelm@34777
|
10 |
|
wenzelm@34820
|
11 |
import scala.actors.TIMEOUT
|
wenzelm@38226
|
12 |
import scala.actors.Actor
|
wenzelm@34777
|
13 |
import scala.actors.Actor._
|
wenzelm@34777
|
14 |
|
wenzelm@34815
|
15 |
|
wenzelm@34791
|
16 |
object Session
|
wenzelm@34791
|
17 |
{
|
wenzelm@34813
|
18 |
/* events */
|
wenzelm@34813
|
19 |
|
wenzelm@34791
|
20 |
case object Global_Settings
|
wenzelm@37849
|
21 |
case object Perspective
|
wenzelm@38849
|
22 |
case object Assignment
|
wenzelm@38360
|
23 |
case class Commands_Changed(set: Set[Command])
|
wenzelm@39630
|
24 |
|
wenzelm@39630
|
25 |
sealed abstract class Phase
|
wenzelm@39630
|
26 |
case object Inactive extends Phase
|
wenzelm@39701
|
27 |
case object Startup extends Phase // transient
|
wenzelm@39701
|
28 |
case object Failed extends Phase
|
wenzelm@39630
|
29 |
case object Ready extends Phase
|
wenzelm@39701
|
30 |
case object Shutdown extends Phase // transient
|
wenzelm@34791
|
31 |
}
|
wenzelm@34791
|
32 |
|
wenzelm@34777
|
33 |
|
wenzelm@34851
|
34 |
class Session(system: Isabelle_System)
|
wenzelm@34777
|
35 |
{
|
wenzelm@37849
|
36 |
/* real time parameters */ // FIXME properties or settings (!?)
|
wenzelm@37849
|
37 |
|
wenzelm@37849
|
38 |
// user input (e.g. text edits, cursor movement)
|
wenzelm@37849
|
39 |
val input_delay = 300
|
wenzelm@37849
|
40 |
|
wenzelm@37849
|
41 |
// prover output (markup, common messages)
|
wenzelm@37849
|
42 |
val output_delay = 100
|
wenzelm@37849
|
43 |
|
wenzelm@37849
|
44 |
// GUI layout updates
|
wenzelm@37849
|
45 |
val update_delay = 500
|
wenzelm@37849
|
46 |
|
wenzelm@37849
|
47 |
|
wenzelm@34809
|
48 |
/* pervasive event buses */
|
wenzelm@34809
|
49 |
|
wenzelm@39701
|
50 |
val phase_changed = new Event_Bus[Session.Phase]
|
wenzelm@34809
|
51 |
val global_settings = new Event_Bus[Session.Global_Settings.type]
|
wenzelm@39588
|
52 |
val raw_messages = new Event_Bus[Isabelle_Process.Result]
|
wenzelm@38360
|
53 |
val commands_changed = new Event_Bus[Session.Commands_Changed]
|
wenzelm@37849
|
54 |
val perspective = new Event_Bus[Session.Perspective.type]
|
wenzelm@38849
|
55 |
val assignments = new Event_Bus[Session.Assignment.type]
|
wenzelm@34809
|
56 |
|
wenzelm@34809
|
57 |
|
wenzelm@34778
|
58 |
/* unique ids */
|
wenzelm@34778
|
59 |
|
wenzelm@38363
|
60 |
private var id_count: Document.ID = 0
|
wenzelm@38419
|
61 |
def new_id(): Document.ID = synchronized {
|
wenzelm@38355
|
62 |
require(id_count > java.lang.Long.MIN_VALUE)
|
wenzelm@38355
|
63 |
id_count -= 1
|
wenzelm@38355
|
64 |
id_count
|
wenzelm@38355
|
65 |
}
|
wenzelm@34778
|
66 |
|
wenzelm@34778
|
67 |
|
wenzelm@34826
|
68 |
|
wenzelm@38841
|
69 |
/** buffered command changes (delay_first discipline) **/
|
wenzelm@38841
|
70 |
|
wenzelm@38841
|
71 |
private case object Stop
|
wenzelm@38841
|
72 |
|
wenzelm@39572
|
73 |
private val (_, command_change_buffer) =
|
wenzelm@39572
|
74 |
Simple_Thread.actor("command_change_buffer", daemon = true)
|
wenzelm@38841
|
75 |
//{{{
|
wenzelm@38841
|
76 |
{
|
wenzelm@38841
|
77 |
import scala.compat.Platform.currentTime
|
wenzelm@38841
|
78 |
|
wenzelm@38841
|
79 |
var changed: Set[Command] = Set()
|
wenzelm@38841
|
80 |
var flush_time: Option[Long] = None
|
wenzelm@38841
|
81 |
|
wenzelm@38841
|
82 |
def flush_timeout: Long =
|
wenzelm@38841
|
83 |
flush_time match {
|
wenzelm@38841
|
84 |
case None => 5000L
|
wenzelm@38841
|
85 |
case Some(time) => (time - currentTime) max 0
|
wenzelm@38841
|
86 |
}
|
wenzelm@38841
|
87 |
|
wenzelm@38841
|
88 |
def flush()
|
wenzelm@38841
|
89 |
{
|
wenzelm@38841
|
90 |
if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
|
wenzelm@38841
|
91 |
changed = Set()
|
wenzelm@38841
|
92 |
flush_time = None
|
wenzelm@38841
|
93 |
}
|
wenzelm@38841
|
94 |
|
wenzelm@38841
|
95 |
def invoke()
|
wenzelm@38841
|
96 |
{
|
wenzelm@38841
|
97 |
val now = currentTime
|
wenzelm@38841
|
98 |
flush_time match {
|
wenzelm@38841
|
99 |
case None => flush_time = Some(now + output_delay)
|
wenzelm@38841
|
100 |
case Some(time) => if (now >= time) flush()
|
wenzelm@38841
|
101 |
}
|
wenzelm@38841
|
102 |
}
|
wenzelm@38841
|
103 |
|
wenzelm@38841
|
104 |
var finished = false
|
wenzelm@38841
|
105 |
while (!finished) {
|
wenzelm@38841
|
106 |
receiveWithin(flush_timeout) {
|
wenzelm@38841
|
107 |
case command: Command => changed += command; invoke()
|
wenzelm@38841
|
108 |
case TIMEOUT => flush()
|
wenzelm@39630
|
109 |
case Stop => finished = true; reply(())
|
wenzelm@38841
|
110 |
case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
|
wenzelm@38841
|
111 |
}
|
wenzelm@38841
|
112 |
}
|
wenzelm@38841
|
113 |
}
|
wenzelm@38841
|
114 |
//}}}
|
wenzelm@38841
|
115 |
|
wenzelm@38841
|
116 |
|
wenzelm@38841
|
117 |
|
wenzelm@38841
|
118 |
/** main protocol actor **/
|
wenzelm@34809
|
119 |
|
wenzelm@34851
|
120 |
@volatile private var syntax = new Outer_Syntax(system.symbols)
|
wenzelm@38569
|
121 |
def current_syntax(): Outer_Syntax = syntax
|
wenzelm@34809
|
122 |
|
wenzelm@39626
|
123 |
@volatile private var reverse_syslog = List[XML.Elem]()
|
wenzelm@39629
|
124 |
def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
|
wenzelm@39626
|
125 |
|
wenzelm@39630
|
126 |
@volatile private var _phase: Session.Phase = Session.Inactive
|
wenzelm@39630
|
127 |
def phase = _phase
|
wenzelm@39633
|
128 |
private def phase_=(new_phase: Session.Phase)
|
wenzelm@39630
|
129 |
{
|
wenzelm@39630
|
130 |
_phase = new_phase
|
wenzelm@39701
|
131 |
phase_changed.event(new_phase)
|
wenzelm@39630
|
132 |
}
|
wenzelm@39630
|
133 |
|
wenzelm@38841
|
134 |
private val global_state = new Volatile(Document.State.init)
|
wenzelm@38841
|
135 |
def current_state(): Document.State = global_state.peek()
|
wenzelm@34816
|
136 |
|
wenzelm@39593
|
137 |
private case object Interrupt_Prover
|
wenzelm@38841
|
138 |
private case class Edit_Version(edits: List[Document.Node_Text_Edit])
|
wenzelm@39630
|
139 |
private case class Start(timeout: Int, args: List[String])
|
wenzelm@34777
|
140 |
|
wenzelm@39572
|
141 |
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
|
wenzelm@38639
|
142 |
{
|
wenzelm@34809
|
143 |
var prover: Isabelle_Process with Isar_Document = null
|
wenzelm@34809
|
144 |
|
wenzelm@34809
|
145 |
|
wenzelm@34809
|
146 |
/* document changes */
|
wenzelm@34809
|
147 |
|
wenzelm@38227
|
148 |
def handle_change(change: Document.Change)
|
wenzelm@38221
|
149 |
//{{{
|
wenzelm@34809
|
150 |
{
|
wenzelm@38848
|
151 |
val previous = change.previous.get_finished
|
wenzelm@39698
|
152 |
val (node_edits, version) = change.result.get_finished
|
wenzelm@38366
|
153 |
|
wenzelm@38848
|
154 |
var former_assignment = global_state.peek().the_assignment(previous).get_finished
|
wenzelm@38370
|
155 |
for {
|
wenzelm@38370
|
156 |
(name, Some(cmd_edits)) <- node_edits
|
wenzelm@38370
|
157 |
(prev, None) <- cmd_edits
|
wenzelm@38417
|
158 |
removed <- previous.nodes(name).commands.get_after(prev)
|
wenzelm@38370
|
159 |
} former_assignment -= removed
|
wenzelm@38370
|
160 |
|
wenzelm@38150
|
161 |
val id_edits =
|
wenzelm@38150
|
162 |
node_edits map {
|
wenzelm@38150
|
163 |
case (name, None) => (name, None)
|
wenzelm@38150
|
164 |
case (name, Some(cmd_edits)) =>
|
wenzelm@38370
|
165 |
val ids =
|
wenzelm@38150
|
166 |
cmd_edits map {
|
wenzelm@38150
|
167 |
case (c1, c2) =>
|
wenzelm@38150
|
168 |
val id1 = c1.map(_.id)
|
wenzelm@38150
|
169 |
val id2 =
|
wenzelm@38150
|
170 |
c2 match {
|
wenzelm@38150
|
171 |
case None => None
|
wenzelm@38150
|
172 |
case Some(command) =>
|
wenzelm@38841
|
173 |
if (global_state.peek().lookup_command(command.id).isEmpty) {
|
wenzelm@38841
|
174 |
global_state.change(_.define_command(command))
|
wenzelm@38150
|
175 |
prover.define_command(command.id, system.symbols.encode(command.source))
|
wenzelm@38150
|
176 |
}
|
wenzelm@38150
|
177 |
Some(command.id)
|
wenzelm@38150
|
178 |
}
|
wenzelm@38150
|
179 |
(id1, id2)
|
wenzelm@38150
|
180 |
}
|
wenzelm@38370
|
181 |
(name -> Some(ids))
|
wenzelm@38150
|
182 |
}
|
wenzelm@39698
|
183 |
global_state.change(_.define_version(version, former_assignment))
|
wenzelm@39698
|
184 |
prover.edit_version(previous.id, version.id, id_edits)
|
wenzelm@34809
|
185 |
}
|
wenzelm@38221
|
186 |
//}}}
|
wenzelm@34809
|
187 |
|
wenzelm@34809
|
188 |
|
wenzelm@34809
|
189 |
/* prover results */
|
wenzelm@34809
|
190 |
|
wenzelm@34836
|
191 |
def bad_result(result: Isabelle_Process.Result)
|
wenzelm@34836
|
192 |
{
|
wenzelm@37041
|
193 |
System.err.println("Ignoring prover result: " + result.message.toString)
|
wenzelm@34836
|
194 |
}
|
wenzelm@34836
|
195 |
|
wenzelm@34809
|
196 |
def handle_result(result: Isabelle_Process.Result)
|
wenzelm@38221
|
197 |
//{{{
|
wenzelm@34809
|
198 |
{
|
wenzelm@39588
|
199 |
raw_messages.event(result)
|
wenzelm@34799
|
200 |
|
wenzelm@38722
|
201 |
result.properties match {
|
wenzelm@38722
|
202 |
case Position.Id(state_id) =>
|
wenzelm@38370
|
203 |
try {
|
wenzelm@38841
|
204 |
val st = global_state.change_yield(_.accumulate(state_id, result.message))
|
wenzelm@38841
|
205 |
command_change_buffer ! st.command
|
wenzelm@38370
|
206 |
}
|
wenzelm@38414
|
207 |
catch { case _: Document.State.Fail => bad_result(result) }
|
wenzelm@38722
|
208 |
case _ =>
|
wenzelm@39630
|
209 |
if (result.is_syslog) {
|
wenzelm@39630
|
210 |
reverse_syslog ::= result.message
|
wenzelm@39630
|
211 |
if (result.is_ready) phase = Session.Ready
|
wenzelm@39701
|
212 |
else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
|
wenzelm@39696
|
213 |
else if (result.is_exit) phase = Session.Inactive
|
wenzelm@39630
|
214 |
}
|
wenzelm@39626
|
215 |
else if (result.is_stdout) { }
|
wenzelm@39625
|
216 |
else if (result.is_status) {
|
wenzelm@38370
|
217 |
result.body match {
|
wenzelm@38417
|
218 |
case List(Isar_Document.Assign(id, edits)) =>
|
wenzelm@38849
|
219 |
try {
|
wenzelm@38882
|
220 |
val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
|
wenzelm@38882
|
221 |
for (cmd <- cmds) command_change_buffer ! cmd
|
wenzelm@38849
|
222 |
assignments.event(Session.Assignment)
|
wenzelm@38849
|
223 |
}
|
wenzelm@38414
|
224 |
catch { case _: Document.State.Fail => bad_result(result) }
|
wenzelm@38370
|
225 |
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
|
wenzelm@38370
|
226 |
case List(Keyword.Keyword_Decl(name)) => syntax += name
|
wenzelm@39625
|
227 |
case _ => bad_result(result)
|
wenzelm@38370
|
228 |
}
|
wenzelm@38370
|
229 |
}
|
wenzelm@39625
|
230 |
else bad_result(result)
|
wenzelm@34809
|
231 |
}
|
wenzelm@34809
|
232 |
}
|
wenzelm@38221
|
233 |
//}}}
|
wenzelm@34809
|
234 |
|
wenzelm@34820
|
235 |
|
wenzelm@39630
|
236 |
/* main loop */
|
wenzelm@34809
|
237 |
|
wenzelm@38639
|
238 |
var finished = false
|
wenzelm@38639
|
239 |
while (!finished) {
|
wenzelm@38639
|
240 |
receive {
|
wenzelm@39593
|
241 |
case Interrupt_Prover =>
|
wenzelm@39593
|
242 |
if (prover != null) prover.interrupt
|
wenzelm@39593
|
243 |
|
wenzelm@39630
|
244 |
case Edit_Version(edits) if prover != null =>
|
wenzelm@39698
|
245 |
val previous = global_state.peek().history.tip.version
|
wenzelm@38841
|
246 |
val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
|
wenzelm@38841
|
247 |
val change = global_state.change_yield(_.extend_history(previous, edits, result))
|
wenzelm@38849
|
248 |
|
wenzelm@38849
|
249 |
val this_actor = self
|
wenzelm@39698
|
250 |
change.version.map(_ => {
|
wenzelm@38849
|
251 |
assignments.await { global_state.peek().is_assigned(previous.get_finished) }
|
wenzelm@38849
|
252 |
this_actor ! change })
|
wenzelm@38849
|
253 |
|
wenzelm@38841
|
254 |
reply(())
|
wenzelm@38841
|
255 |
|
wenzelm@39630
|
256 |
case change: Document.Change if prover != null => handle_change(change)
|
wenzelm@39630
|
257 |
|
wenzelm@39630
|
258 |
case result: Isabelle_Process.Result => handle_result(result)
|
wenzelm@38841
|
259 |
|
wenzelm@39630
|
260 |
case Start(timeout, args) if prover == null =>
|
wenzelm@39701
|
261 |
if (phase == Session.Inactive || phase == Session.Failed) {
|
wenzelm@39701
|
262 |
phase = Session.Startup
|
wenzelm@39701
|
263 |
prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
|
wenzelm@39701
|
264 |
}
|
wenzelm@38841
|
265 |
|
wenzelm@39701
|
266 |
case Stop =>
|
wenzelm@39701
|
267 |
if (phase == Session.Ready) {
|
wenzelm@39701
|
268 |
global_state.change(_ => Document.State.init) // FIXME event bus!?
|
wenzelm@39701
|
269 |
phase = Session.Shutdown
|
wenzelm@39701
|
270 |
prover.terminate
|
wenzelm@39701
|
271 |
phase = Session.Inactive
|
wenzelm@39701
|
272 |
}
|
wenzelm@39630
|
273 |
finished = true
|
wenzelm@39630
|
274 |
reply(())
|
wenzelm@38850
|
275 |
|
wenzelm@34820
|
276 |
case bad if prover != null =>
|
wenzelm@34777
|
277 |
System.err.println("session_actor: ignoring bad message " + bad)
|
wenzelm@34777
|
278 |
}
|
wenzelm@34777
|
279 |
}
|
wenzelm@34777
|
280 |
}
|
wenzelm@34777
|
281 |
|
wenzelm@34809
|
282 |
|
wenzelm@37129
|
283 |
|
wenzelm@38226
|
284 |
/** main methods **/
|
wenzelm@34809
|
285 |
|
wenzelm@39630
|
286 |
def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
|
wenzelm@34820
|
287 |
|
wenzelm@39630
|
288 |
def stop() { command_change_buffer !? Stop; session_actor !? Stop }
|
wenzelm@38841
|
289 |
|
wenzelm@39593
|
290 |
def interrupt() { session_actor ! Interrupt_Prover }
|
wenzelm@39593
|
291 |
|
wenzelm@38841
|
292 |
def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
|
wenzelm@38221
|
293 |
|
wenzelm@38841
|
294 |
def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
|
wenzelm@38841
|
295 |
global_state.peek().snapshot(name, pending_edits)
|
wenzelm@34777
|
296 |
}
|