Command.toString: include id for debugging;
authorwenzelm
Thu May 27 00:47:15 2010 +0200 (2010-05-27)
changeset 371294c83696b340e
parent 37128 1b6a4d9f397a
child 37130 7f18edbbf618
Command.toString: include id for debugging;
Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus;
State.+ without side-effect on event bus;
Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results;
Document_View: tuned commands_changed handling and caret listening;
Document_View.selected_command: proper function, not event handler state;
Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);
src/Pure/PIDE/command.scala
src/Pure/PIDE/state.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed May 26 18:19:36 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu May 27 00:47:15 2010 +0200
     1.3 @@ -13,6 +13,9 @@
     1.4  import scala.collection.mutable
     1.5  
     1.6  
     1.7 +case class Command_Set(set: Set[Command])
     1.8 +
     1.9 +
    1.10  object Command
    1.11  {
    1.12    object Status extends Enumeration
    1.13 @@ -29,10 +32,10 @@
    1.14      command_id: Option[String], offset: Option[Int])
    1.15  }
    1.16  
    1.17 -
    1.18  class Command(
    1.19      val id: Isar_Document.Command_ID,
    1.20 -    val span: Thy_Syntax.Span)
    1.21 +    val span: Thy_Syntax.Span,
    1.22 +    val static_parent: Option[Command] = None)
    1.23    extends Session.Entity
    1.24  {
    1.25    /* classification */
    1.26 @@ -42,7 +45,9 @@
    1.27    def is_malformed: Boolean = !is_command && !is_ignored
    1.28  
    1.29    def name: String = if (is_command) span.head.content else ""
    1.30 -  override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
    1.31 +  override def toString =
    1.32 +    if (is_command) name + "(" + id + ")"
    1.33 +    else if (is_ignored) "<ignored>" else "<malformed>"
    1.34  
    1.35  
    1.36    /* source text */
    1.37 @@ -59,15 +64,17 @@
    1.38    @volatile protected var state = new State(this)
    1.39    def current_state: State = state
    1.40  
    1.41 -  private case class Consume(session: Session, message: XML.Tree)
    1.42 +  private case class Consume(message: XML.Tree, forward: Command => Unit)
    1.43    private case object Assign
    1.44  
    1.45    private val accumulator = actor {
    1.46      var assigned = false
    1.47      loop {
    1.48        react {
    1.49 -        case Consume(session: Session, message: XML.Tree) if !assigned =>
    1.50 -          state = state.+(session, message)
    1.51 +        case Consume(message, forward) if !assigned =>
    1.52 +          val old_state = state
    1.53 +          state = old_state + message
    1.54 +          if (!(state eq old_state)) forward(static_parent getOrElse this)
    1.55  
    1.56          case Assign =>
    1.57            assigned = true  // single assignment
    1.58 @@ -78,11 +85,14 @@
    1.59      }
    1.60    }
    1.61  
    1.62 -  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
    1.63 +  def consume(message: XML.Tree, forward: Command => Unit)
    1.64 +  {
    1.65 +    accumulator ! Consume(message, forward)
    1.66 +  }
    1.67  
    1.68    def assign_state(state_id: Isar_Document.State_ID): Command =
    1.69    {
    1.70 -    val cmd = new Command(state_id, span)
    1.71 +    val cmd = new Command(state_id, span, Some(this))
    1.72      accumulator !? Assign
    1.73      cmd.state = current_state
    1.74      cmd
     2.1 --- a/src/Pure/PIDE/state.scala	Wed May 26 18:19:36 2010 +0200
     2.2 +++ b/src/Pure/PIDE/state.scala	Thu May 27 00:47:15 2010 +0200
     2.3 @@ -70,50 +70,45 @@
     2.4  
     2.5    /* message dispatch */
     2.6  
     2.7 -  def + (session: Session, message: XML.Tree): State =
     2.8 -  {
     2.9 -    val changed: State =
    2.10 -      message match {
    2.11 -        case XML.Elem(Markup.STATUS, _, elems) =>
    2.12 -          (this /: elems)((state, elem) =>
    2.13 -            elem match {
    2.14 -              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    2.15 -              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    2.16 -              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    2.17 -              case XML.Elem(kind, atts, body) =>
    2.18 -                atts match {
    2.19 -                  case Position.Range(begin, end) =>
    2.20 -                    if (kind == Markup.ML_TYPING) {
    2.21 -                      val info = Pretty.string_of(body, margin = 40)
    2.22 -                      state.add_markup(
    2.23 -                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
    2.24 +  def + (message: XML.Tree): State =
    2.25 +    message match {
    2.26 +      case XML.Elem(Markup.STATUS, _, elems) =>
    2.27 +        (this /: elems)((state, elem) =>
    2.28 +          elem match {
    2.29 +            case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    2.30 +            case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    2.31 +            case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    2.32 +            case XML.Elem(kind, atts, body) =>
    2.33 +              atts match {
    2.34 +                case Position.Range(begin, end) =>
    2.35 +                  if (kind == Markup.ML_TYPING) {
    2.36 +                    val info = Pretty.string_of(body, margin = 40)
    2.37 +                    state.add_markup(
    2.38 +                      command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
    2.39 +                  }
    2.40 +                  else if (kind == Markup.ML_REF) {
    2.41 +                    body match {
    2.42 +                      case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    2.43 +                        state.add_markup(command.markup_node(
    2.44 +                          begin - 1, end - 1,
    2.45 +                          Command.RefInfo(
    2.46 +                            Position.get_file(atts),
    2.47 +                            Position.get_line(atts),
    2.48 +                            Position.get_id(atts),
    2.49 +                            Position.get_offset(atts))))
    2.50 +                      case _ => state
    2.51                      }
    2.52 -                    else if (kind == Markup.ML_REF) {
    2.53 -                      body match {
    2.54 -                        case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    2.55 -                          state.add_markup(command.markup_node(
    2.56 -                            begin - 1, end - 1,
    2.57 -                            Command.RefInfo(
    2.58 -                              Position.get_file(atts),
    2.59 -                              Position.get_line(atts),
    2.60 -                              Position.get_id(atts),
    2.61 -                              Position.get_offset(atts))))
    2.62 -                        case _ => state
    2.63 -                      }
    2.64 -                    }
    2.65 -                    else {
    2.66 -                      state.add_markup(
    2.67 -                        command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
    2.68 -                    }
    2.69 -                  case _ => state
    2.70 -                }
    2.71 -              case _ =>
    2.72 -                System.err.println("ignored status report: " + elem)
    2.73 -                state
    2.74 -            })
    2.75 -        case _ => add_result(message)
    2.76 -      }
    2.77 -    if (!(this eq changed)) session.command_change.event(command)
    2.78 -    changed
    2.79 -  }
    2.80 +                  }
    2.81 +                  else {
    2.82 +                    state.add_markup(
    2.83 +                      command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
    2.84 +                  }
    2.85 +                case _ => state
    2.86 +              }
    2.87 +            case _ =>
    2.88 +              System.err.println("ignored status report: " + elem)
    2.89 +              state
    2.90 +          })
    2.91 +      case _ => add_result(message)
    2.92 +    }
    2.93  }
     3.1 --- a/src/Pure/System/session.scala	Wed May 26 18:19:36 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Thu May 27 00:47:15 2010 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4    trait Entity
     3.5    {
     3.6      val id: Entity_ID
     3.7 -    def consume(session: Session, message: XML.Tree): Unit
     3.8 +    def consume(message: XML.Tree, forward: Command => Unit): Unit
     3.9    }
    3.10  }
    3.11  
    3.12 @@ -37,9 +37,7 @@
    3.13    val global_settings = new Event_Bus[Session.Global_Settings.type]
    3.14    val raw_results = new Event_Bus[Isabelle_Process.Result]
    3.15    val raw_output = new Event_Bus[Isabelle_Process.Result]
    3.16 -  val results = new Event_Bus[Command]
    3.17 -
    3.18 -  val command_change = new Event_Bus[Command]
    3.19 +  val commands_changed = new Event_Bus[Command_Set]
    3.20  
    3.21  
    3.22    /* unique ids */
    3.23 @@ -66,7 +64,7 @@
    3.24    private case object Stop
    3.25    private case class Begin_Document(path: String)
    3.26  
    3.27 -  private val session_actor = actor {
    3.28 +  private lazy val session_actor = actor {
    3.29  
    3.30      var prover: Isabelle_Process with Isar_Document = null
    3.31  
    3.32 @@ -118,7 +116,7 @@
    3.33            case None => None
    3.34            case Some(id) => lookup_entity(id)
    3.35          }
    3.36 -      if (target.isDefined) target.get.consume(this, result.message)
    3.37 +      if (target.isDefined) target.get.consume(result.message, indicate_command_change)
    3.38        else if (result.kind == Isabelle_Process.Kind.STATUS) {
    3.39          // global status message
    3.40          result.body match {
    3.41 @@ -239,6 +237,52 @@
    3.42    }
    3.43  
    3.44  
    3.45 +
    3.46 +  /** buffered command changes -- delay_first discipline **/
    3.47 +
    3.48 +  private lazy val command_change_buffer = actor {
    3.49 +    import scala.compat.Platform.currentTime
    3.50 +
    3.51 +    var changed: Set[Command] = Set()
    3.52 +    var flush_time: Option[Long] = None
    3.53 +
    3.54 +    def flush_timeout: Long =
    3.55 +      flush_time match {
    3.56 +        case None => 5000L
    3.57 +        case Some(time) => (time - currentTime) max 0
    3.58 +      }
    3.59 +
    3.60 +    def flush()
    3.61 +    {
    3.62 +      if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
    3.63 +      changed = Set()
    3.64 +      flush_time = None
    3.65 +    }
    3.66 +
    3.67 +    def invoke()
    3.68 +    {
    3.69 +      val now = currentTime
    3.70 +      flush_time match {
    3.71 +        case None => flush_time = Some(now + 100)
    3.72 +        case Some(time) => if (now >= time) flush()
    3.73 +      }
    3.74 +    }
    3.75 +
    3.76 +    loop {
    3.77 +      reactWithin(flush_timeout) {
    3.78 +        case command: Command => changed += command; invoke()
    3.79 +        case TIMEOUT => flush()
    3.80 +        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    3.81 +      }
    3.82 +    }
    3.83 +  }
    3.84 +
    3.85 +  def indicate_command_change(command: Command)
    3.86 +  {
    3.87 +    command_change_buffer ! command
    3.88 +  }
    3.89 +
    3.90 +
    3.91    /* main methods */
    3.92  
    3.93    def start(timeout: Int, args: List[String]): Option[String] =
     4.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed May 26 18:19:36 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 00:47:15 2010 +0200
     4.3 @@ -69,7 +69,7 @@
     4.4  }
     4.5  
     4.6  
     4.7 -class Document_View(model: Document_Model, text_area: TextArea)
     4.8 +class Document_View(val model: Document_Model, text_area: TextArea)
     4.9  {
    4.10    private val session = model.session
    4.11  
    4.12 @@ -79,38 +79,22 @@
    4.13    @volatile private var document = model.recent_document()
    4.14  
    4.15  
    4.16 -  /* buffer of changed commands -- owned by Swing thread */
    4.17 -
    4.18 -  @volatile private var changed_commands: Set[Command] = Set()
    4.19 +  /* commands_changed_actor */
    4.20  
    4.21 -  private val changed_delay = Swing_Thread.delay_first(100) {
    4.22 -    if (!changed_commands.isEmpty) {
    4.23 -      document = model.recent_document()
    4.24 -      for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
    4.25 -        update_syntax(cmd)
    4.26 -        invalidate_line(cmd)
    4.27 -        overview.repaint()
    4.28 -      }
    4.29 -      changed_commands = Set()
    4.30 -    }
    4.31 -  }
    4.32 -
    4.33 -
    4.34 -  /* command change actor */
    4.35 -
    4.36 -  private case object Exit
    4.37 -
    4.38 -  private val command_change_actor = actor {
    4.39 +  private val commands_changed_actor = actor {
    4.40      loop {
    4.41        react {
    4.42 -        case command: Command =>  // FIXME rough filtering according to document family!?
    4.43 +        case Command_Set(changed) =>
    4.44            Swing_Thread.now {
    4.45 -            changed_commands += command
    4.46 -            changed_delay()
    4.47 +            document = model.recent_document()
    4.48 +            // FIXME cover doc states as well!!?
    4.49 +            for (command <- changed if document.commands.contains(command)) {
    4.50 +              update_syntax(command)
    4.51 +              invalidate_line(command)
    4.52 +              overview.repaint()
    4.53 +            }
    4.54            }
    4.55  
    4.56 -        case Exit => reply(()); exit()
    4.57 -
    4.58          case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
    4.59        }
    4.60      }
    4.61 @@ -153,24 +137,23 @@
    4.62    }
    4.63  
    4.64  
    4.65 -  /* caret_listener */
    4.66 +  /* caret handling */
    4.67  
    4.68 -  private var _selected_command: Command = null
    4.69 -  private def selected_command = _selected_command
    4.70 -  private def selected_command_=(cmd: Command)
    4.71 -  {
    4.72 -    _selected_command = cmd
    4.73 -    session.results.event(cmd)
    4.74 -  }
    4.75 +  def selected_command: Option[Command] =
    4.76 +    document.command_at(text_area.getCaretPosition) match {
    4.77 +      case Some((command, _)) => Some(command)
    4.78 +      case None => None
    4.79 +    }
    4.80  
    4.81    private val caret_listener = new CaretListener
    4.82    {
    4.83 +    private var last_selected_command: Option[Command] = None
    4.84      override def caretUpdate(e: CaretEvent)
    4.85      {
    4.86 -      document.command_at(e.getDot) match {
    4.87 -        case Some((command, command_start)) if (selected_command != command) =>
    4.88 -          selected_command = command
    4.89 -        case _ =>
    4.90 +      val selected = selected_command
    4.91 +      if (selected != last_selected_command) {
    4.92 +        last_selected_command = selected
    4.93 +        if (selected.isDefined) session.indicate_command_change(selected.get)
    4.94        }
    4.95      }
    4.96    }
    4.97 @@ -192,9 +175,6 @@
    4.98    {
    4.99      val (start, stop) = model.lines_of_command(document, cmd)
   4.100      text_area.invalidateLineRange(start, stop)
   4.101 -
   4.102 -    if (selected_command == cmd)
   4.103 -      session.results.event(cmd)
   4.104    }
   4.105  
   4.106    private def invalidate_all() =
   4.107 @@ -289,13 +269,12 @@
   4.108        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   4.109      text_area.addCaretListener(caret_listener)
   4.110      text_area.addLeftOfScrollBar(overview)
   4.111 -    session.command_change += command_change_actor
   4.112 +    session.commands_changed += commands_changed_actor
   4.113    }
   4.114  
   4.115    private def deactivate()
   4.116    {
   4.117 -    session.command_change -= command_change_actor
   4.118 -    command_change_actor !? Exit
   4.119 +    session.commands_changed -= commands_changed_actor
   4.120      text_area.removeLeftOfScrollBar(overview)
   4.121      text_area.removeCaretListener(caret_listener)
   4.122      text_area.getPainter.removeExtension(text_area_extension)
     5.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed May 26 18:19:36 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 00:47:15 2010 +0200
     5.3 @@ -99,13 +99,19 @@
     5.4          case Session.Global_Settings => handle_resize()
     5.5          case Render(body) => html_panel.render(body)
     5.6  
     5.7 -        case cmd: Command =>
     5.8 +        case Command_Set(changed) =>
     5.9            Swing_Thread.now {
    5.10 -            if (follow.selected) Document_Model(view.getBuffer) else None
    5.11 -          } match {
    5.12 -            case None =>
    5.13 -            case Some(model) =>
    5.14 -              html_panel.render(filtered_results(model.recent_document, cmd))
    5.15 +            if (follow.selected) {
    5.16 +              Document_View(view.getTextArea) match {
    5.17 +                case Some(doc_view) =>
    5.18 +                  doc_view.selected_command match {
    5.19 +                    case Some(cmd) if changed.contains(cmd) =>
    5.20 +                      html_panel.render(filtered_results(doc_view.model.recent_document, cmd))
    5.21 +                    case _ =>
    5.22 +                  }
    5.23 +                case None =>
    5.24 +              }
    5.25 +            }
    5.26            }
    5.27  
    5.28          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    5.29 @@ -115,13 +121,13 @@
    5.30  
    5.31    override def init()
    5.32    {
    5.33 -    Isabelle.session.results += main_actor
    5.34 +    Isabelle.session.commands_changed += main_actor
    5.35      Isabelle.session.global_settings += main_actor
    5.36    }
    5.37  
    5.38    override def exit()
    5.39    {
    5.40 -    Isabelle.session.results -= main_actor
    5.41 +    Isabelle.session.commands_changed -= main_actor
    5.42      Isabelle.session.global_settings -= main_actor
    5.43    }
    5.44