equal
deleted
inserted
replaced
48 /* real time parameters */ // FIXME properties or settings (!?) |
48 /* real time parameters */ // FIXME properties or settings (!?) |
49 |
49 |
50 val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement) |
50 val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement) |
51 val output_delay = Time.seconds(0.1) // prover output (markup, common messages) |
51 val output_delay = Time.seconds(0.1) // prover output (markup, common messages) |
52 val update_delay = Time.seconds(0.5) // GUI layout updates |
52 val update_delay = Time.seconds(0.5) // GUI layout updates |
|
53 val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.) |
53 |
54 |
54 |
55 |
55 /* pervasive event buses */ |
56 /* pervasive event buses */ |
56 |
57 |
57 val global_settings = new Event_Bus[Session.Global_Settings.type] |
58 val global_settings = new Event_Bus[Session.Global_Settings.type] |
184 |
185 |
185 /* actor messages */ |
186 /* actor messages */ |
186 |
187 |
187 private case class Start(timeout: Time, args: List[String]) |
188 private case class Start(timeout: Time, args: List[String]) |
188 private case object Interrupt |
189 private case object Interrupt |
|
190 private case class Check_Loaded_Files(ask: List[String] => Boolean) |
189 private case class Init_Node(name: String, master_dir: String, |
191 private case class Init_Node(name: String, master_dir: String, |
190 header: Document.Node_Header, perspective: Text.Perspective, text: String) |
192 header: Document.Node_Header, perspective: Text.Perspective, text: String) |
191 private case class Edit_Node(name: String, master_dir: String, |
193 private case class Edit_Node(name: String, master_dir: String, |
192 header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit]) |
194 header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit]) |
193 private case class Change_Node( |
195 private case class Change_Node( |
369 reply(()) |
371 reply(()) |
370 |
372 |
371 case Interrupt if prover.isDefined => |
373 case Interrupt if prover.isDefined => |
372 prover.get.interrupt |
374 prover.get.interrupt |
373 |
375 |
|
376 case Check_Loaded_Files(ask) => // FIXME |
|
377 |
374 case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined => |
378 case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined => |
375 // FIXME compare with existing node |
379 // FIXME compare with existing node |
376 handle_edits(name, master_dir, header, |
380 handle_edits(name, master_dir, header, |
377 List(Document.Node.Clear(), |
381 List(Document.Node.Clear(), |
378 Document.Node.Edits(List(Text.Edit.insert(0, text))), |
382 Document.Node.Edits(List(Text.Edit.insert(0, text))), |
411 |
415 |
412 def stop() { command_change_buffer !? Stop; session_actor !? Stop } |
416 def stop() { command_change_buffer !? Stop; session_actor !? Stop } |
413 |
417 |
414 def interrupt() { session_actor ! Interrupt } |
418 def interrupt() { session_actor ! Interrupt } |
415 |
419 |
|
420 def check_loaded_files(ask: List[String] => Boolean) |
|
421 { |
|
422 session_actor ! Check_Loaded_Files(ask) |
|
423 } |
|
424 |
416 // FIXME simplify signature |
425 // FIXME simplify signature |
417 def init_node(name: String, master_dir: String, |
426 def init_node(name: String, master_dir: String, |
418 header: Document.Node_Header, perspective: Text.Perspective, text: String) |
427 header: Document.Node_Header, perspective: Text.Perspective, text: String) |
419 { session_actor !? Init_Node(name, master_dir, header, perspective, text) } |
428 { session_actor !? Init_Node(name, master_dir, header, perspective, text) } |
420 |
429 |