Session: predefined real time parameters;
authorwenzelm
Mon Jul 19 22:19:18 2010 +0200 (2010-07-19)
changeset 378494f9de312cc23
parent 37848 a33ecf47f0a0
child 37850 afb5653a3a47
Session: predefined real time parameters;
Document_View: delayed caret handling, for improved reactivity;
selected_command: proper_command_at ignores ignored commands;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Jul 19 08:59:43 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jul 19 22:19:18 2010 +0200
     1.3 @@ -162,6 +162,12 @@
     1.4      if (range.hasNext) Some(range.next) else None
     1.5    }
     1.6  
     1.7 +  def proper_command_at(i: Int): Option[Command] =
     1.8 +    command_at(i) match {
     1.9 +      case Some((command, _)) => commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    1.10 +      case None => None
    1.11 +    }
    1.12 +
    1.13  
    1.14    /* command state assignment */
    1.15  
     2.1 --- a/src/Pure/System/session.scala	Mon Jul 19 08:59:43 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Mon Jul 19 22:19:18 2010 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    /* events */
     2.5  
     2.6    case object Global_Settings
     2.7 +  case object Perspective
     2.8  
     2.9  
    2.10    /* managed entities */
    2.11 @@ -32,12 +33,25 @@
    2.12  
    2.13  class Session(system: Isabelle_System)
    2.14  {
    2.15 +  /* real time parameters */  // FIXME properties or settings (!?)
    2.16 +
    2.17 +  // user input (e.g. text edits, cursor movement)
    2.18 +  val input_delay = 300
    2.19 +
    2.20 +  // prover output (markup, common messages)
    2.21 +  val output_delay = 100
    2.22 +
    2.23 +  // GUI layout updates
    2.24 +  val update_delay = 500
    2.25 +
    2.26 +
    2.27    /* pervasive event buses */
    2.28  
    2.29    val global_settings = new Event_Bus[Session.Global_Settings.type]
    2.30    val raw_results = new Event_Bus[Isabelle_Process.Result]
    2.31    val raw_output = new Event_Bus[Isabelle_Process.Result]
    2.32    val commands_changed = new Event_Bus[Command_Set]
    2.33 +  val perspective = new Event_Bus[Session.Perspective.type]
    2.34  
    2.35  
    2.36    /* unique ids */
    2.37 @@ -263,7 +277,7 @@
    2.38      {
    2.39        val now = currentTime
    2.40        flush_time match {
    2.41 -        case None => flush_time = Some(now + 100)   // FIXME output_delay property
    2.42 +        case None => flush_time = Some(now + output_delay)
    2.43          case Some(time) => if (now >= time) flush()
    2.44        }
    2.45      }
     3.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jul 19 08:59:43 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jul 19 22:19:18 2010 +0200
     3.3 @@ -100,7 +100,7 @@
     3.4  
     3.5    private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
     3.6  
     3.7 -  private val edits_delay = Swing_Thread.delay_last(300) {  // FIXME input_delay property
     3.8 +  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
     3.9      if (!edits_buffer.isEmpty) {
    3.10        val new_change = current_change().edit(session, edits_buffer.toList)
    3.11        edits_buffer.clear
     4.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jul 19 08:59:43 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jul 19 22:19:18 2010 +0200
     4.3 @@ -211,23 +211,14 @@
     4.4  
     4.5    /* caret handling */
     4.6  
     4.7 -  def selected_command: Option[Command] =
     4.8 -    model.recent_document().command_at(text_area.getCaretPosition) match {
     4.9 -      case Some((command, _)) => Some(command)
    4.10 -      case None => None
    4.11 -    }
    4.12 +  def selected_command(): Option[Command] =
    4.13 +    model.recent_document().proper_command_at(text_area.getCaretPosition)
    4.14  
    4.15 -  private val caret_listener = new CaretListener
    4.16 -  {
    4.17 -    private var last_selected_command: Option[Command] = None
    4.18 -    override def caretUpdate(e: CaretEvent)
    4.19 -    {
    4.20 -      val selected = selected_command
    4.21 -      if (selected != last_selected_command) {
    4.22 -        last_selected_command = selected
    4.23 -        if (selected.isDefined) session.indicate_command_change(selected.get)
    4.24 -      }
    4.25 +  private val caret_listener = new CaretListener {
    4.26 +    private val delay = Swing_Thread.delay_last(session.input_delay) {
    4.27 +      session.perspective.event(Session.Perspective)
    4.28      }
    4.29 +    override def caretUpdate(e: CaretEvent) { delay() }
    4.30    }
    4.31  
    4.32  
     5.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jul 19 08:59:43 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jul 19 22:19:18 2010 +0200
     5.3 @@ -46,20 +46,21 @@
     5.4      }
     5.5    }
     5.6  
     5.7 -  private def handle_caret()
     5.8 -  {
     5.9 +  private def handle_perspective(): Boolean =
    5.10      Swing_Thread.now {
    5.11        Document_View(view.getTextArea) match {
    5.12 -        case Some(doc_view) => current_command = doc_view.selected_command
    5.13 -        case None =>
    5.14 +        case Some(doc_view) =>
    5.15 +          val cmd = doc_view.selected_command()
    5.16 +          if (current_command == cmd) false
    5.17 +          else { current_command = cmd; true }
    5.18 +        case None => false
    5.19        }
    5.20      }
    5.21 -  }
    5.22  
    5.23    private def handle_update(restriction: Option[Set[Command]] = None)
    5.24    {
    5.25      Swing_Thread.now {
    5.26 -      if (follow_caret) handle_caret()
    5.27 +      if (follow_caret) handle_perspective()
    5.28        Document_View(view.getTextArea) match {
    5.29          case Some(doc_view) =>
    5.30            current_command match {
    5.31 @@ -87,6 +88,7 @@
    5.32        react {
    5.33          case Session.Global_Settings => handle_resize()
    5.34          case Command_Set(changed) => handle_update(Some(changed))
    5.35 +        case Session.Perspective => if (handle_perspective()) handle_update()
    5.36          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    5.37        }
    5.38      }
    5.39 @@ -94,21 +96,23 @@
    5.40  
    5.41    override def init()
    5.42    {
    5.43 +    Isabelle.session.global_settings += main_actor
    5.44      Isabelle.session.commands_changed += main_actor
    5.45 -    Isabelle.session.global_settings += main_actor
    5.46 +    Isabelle.session.perspective += main_actor
    5.47    }
    5.48  
    5.49    override def exit()
    5.50    {
    5.51 +    Isabelle.session.global_settings -= main_actor
    5.52      Isabelle.session.commands_changed -= main_actor
    5.53 -    Isabelle.session.global_settings -= main_actor
    5.54 +    Isabelle.session.perspective -= main_actor
    5.55    }
    5.56  
    5.57  
    5.58    /* resize */
    5.59  
    5.60    addComponentListener(new ComponentAdapter {
    5.61 -    val delay = Swing_Thread.delay_last(500) { handle_resize() }  // FIXME update_delay property
    5.62 +    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
    5.63      override def componentResized(e: ComponentEvent) { delay() }
    5.64    })
    5.65  
    5.66 @@ -138,7 +142,7 @@
    5.67    auto_update.tooltip = "Indicate automatic update following cursor movement"
    5.68  
    5.69    private val update = new Button("Update") {
    5.70 -    reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
    5.71 +    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
    5.72    }
    5.73    update.tooltip = "Update display according to the command at cursor position"
    5.74