59 /** buffered command changes (delay_first discipline) **/ |
59 /** buffered command changes (delay_first discipline) **/ |
60 |
60 |
61 //{{{ |
61 //{{{ |
62 private case object Stop |
62 private case object Stop |
63 |
63 |
64 private val (_, command_change_buffer) = |
64 private val (_, commands_changed_buffer) = |
65 Simple_Thread.actor("command_change_buffer", daemon = true) |
65 Simple_Thread.actor("commands_changed_buffer", daemon = true) |
66 { |
66 { |
67 var changed_nodes: Set[Document.Node.Name] = Set.empty |
|
68 var changed_commands: Set[Command] = Set.empty |
|
69 def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty |
|
70 |
|
71 var flush_time: Option[Long] = None |
|
72 |
|
73 def flush_timeout: Long = |
|
74 flush_time match { |
|
75 case None => 5000L |
|
76 case Some(time) => (time - System.currentTimeMillis()) max 0 |
|
77 } |
|
78 |
|
79 def flush() |
|
80 { |
|
81 if (changed) |
|
82 commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands)) |
|
83 changed_nodes = Set.empty |
|
84 changed_commands = Set.empty |
|
85 flush_time = None |
|
86 } |
|
87 |
|
88 def invoke() |
|
89 { |
|
90 val now = System.currentTimeMillis() |
|
91 flush_time match { |
|
92 case None => flush_time = Some(now + output_delay.ms) |
|
93 case Some(time) => if (now >= time) flush() |
|
94 } |
|
95 } |
|
96 |
|
97 var finished = false |
67 var finished = false |
98 while (!finished) { |
68 while (!finished) { |
99 receiveWithin(flush_timeout) { |
69 receive { |
100 case command: Command => |
|
101 changed_nodes += command.node_name |
|
102 changed_commands += command |
|
103 invoke() |
|
104 case TIMEOUT => flush() |
|
105 case Stop => finished = true; reply(()) |
70 case Stop => finished = true; reply(()) |
106 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad) |
71 case changed: Session.Commands_Changed => commands_changed.event(changed) |
|
72 case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad) |
107 } |
73 } |
108 } |
74 } |
109 } |
75 } |
110 //}}} |
76 //}}} |
111 |
77 |
182 var prover: Option[Isabelle_Process with Isar_Document] = None |
148 var prover: Option[Isabelle_Process with Isar_Document] = None |
183 |
149 |
184 var prune_next = System.currentTimeMillis() + prune_delay.ms |
150 var prune_next = System.currentTimeMillis() + prune_delay.ms |
185 |
151 |
186 |
152 |
|
153 /* delayed command changes */ |
|
154 |
|
155 object commands_changed_delay |
|
156 { |
|
157 private var changed_nodes: Set[Document.Node.Name] = Set.empty |
|
158 private var changed_commands: Set[Command] = Set.empty |
|
159 private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty |
|
160 |
|
161 private var flush_time: Option[Long] = None |
|
162 |
|
163 def flush_timeout: Long = |
|
164 flush_time match { |
|
165 case None => 5000L |
|
166 case Some(time) => (time - System.currentTimeMillis()) max 0 |
|
167 } |
|
168 |
|
169 def flush() |
|
170 { |
|
171 if (changed) |
|
172 commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands) |
|
173 changed_nodes = Set.empty |
|
174 changed_commands = Set.empty |
|
175 flush_time = None |
|
176 } |
|
177 |
|
178 def invoke(command: Command) |
|
179 { |
|
180 changed_nodes += command.node_name |
|
181 changed_commands += command |
|
182 val now = System.currentTimeMillis() |
|
183 flush_time match { |
|
184 case None => flush_time = Some(now + output_delay.ms) |
|
185 case Some(time) => if (now >= time) flush() |
|
186 } |
|
187 } |
|
188 } |
|
189 |
|
190 |
187 /* perspective */ |
191 /* perspective */ |
188 |
192 |
189 def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective) |
193 def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective) |
190 { |
194 { |
191 val previous = global_state().tip_version |
195 val previous = global_state().tip_version |
234 |
238 |
235 def handle_assign(id: Document.Version_ID, assign: Document.Assign) |
239 def handle_assign(id: Document.Version_ID, assign: Document.Assign) |
236 //{{{ |
240 //{{{ |
237 { |
241 { |
238 val cmds = global_state.change_yield(_.assign(id, assign)) |
242 val cmds = global_state.change_yield(_.assign(id, assign)) |
239 for (cmd <- cmds) command_change_buffer ! cmd |
243 for (cmd <- cmds) commands_changed_delay.invoke(cmd) |
240 assignments.event(Session.Assignment) |
244 assignments.event(Session.Assignment) |
241 } |
245 } |
242 //}}} |
246 //}}} |
243 |
247 |
244 |
248 |
294 |
298 |
295 result.properties match { |
299 result.properties match { |
296 case Position.Id(state_id) if !result.is_raw => |
300 case Position.Id(state_id) if !result.is_raw => |
297 try { |
301 try { |
298 val st = global_state.change_yield(_.accumulate(state_id, result.message)) |
302 val st = global_state.change_yield(_.accumulate(state_id, result.message)) |
299 command_change_buffer ! st.command |
303 commands_changed_delay.invoke(st.command) |
300 } |
304 } |
301 catch { |
305 catch { |
302 case _: Document.State.Fail => bad_result(result) |
306 case _: Document.State.Fail => bad_result(result) |
303 } |
307 } |
304 case Markup.Assign_Execs if result.is_raw => |
308 case Markup.Assign_Execs if result.is_raw => |
359 /* main loop */ |
363 /* main loop */ |
360 |
364 |
361 //{{{ |
365 //{{{ |
362 var finished = false |
366 var finished = false |
363 while (!finished) { |
367 while (!finished) { |
364 receive { |
368 receiveWithin(commands_changed_delay.flush_timeout) { |
|
369 case TIMEOUT => commands_changed_delay.flush() |
|
370 |
365 case Start(timeout, args) if prover.isEmpty => |
371 case Start(timeout, args) if prover.isEmpty => |
366 if (phase == Session.Inactive || phase == Session.Failed) { |
372 if (phase == Session.Inactive || phase == Session.Failed) { |
367 phase = Session.Startup |
373 phase = Session.Startup |
368 prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document) |
374 prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document) |
369 } |
375 } |
418 |
424 |
419 /* actions */ |
425 /* actions */ |
420 |
426 |
421 def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) } |
427 def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) } |
422 |
428 |
423 def stop() { command_change_buffer !? Stop; session_actor !? Stop } |
429 def stop() { commands_changed_buffer !? Stop; session_actor !? Stop } |
424 |
430 |
425 def interrupt() { session_actor ! Interrupt } |
431 def interrupt() { session_actor ! Interrupt } |
426 |
432 |
427 def init_node(name: Document.Node.Name, |
433 def init_node(name: Document.Node.Name, |
428 header: Document.Node_Header, perspective: Text.Perspective, text: String) |
434 header: Document.Node_Header, perspective: Text.Perspective, text: String) |