more explicit status for query operation;
authorwenzelm
Tue Aug 06 21:08:04 2013 +0200 (2013-08-06 ago)
changeset 5287678989972d5b8
parent 52875 e2d5c3ff5c3f
child 52877 9a26ec5739dd
more explicit status for query operation;
avoid output with outdated snapshot;
animation rate according to status;
added PIDE.document_snapshot convenience -- independent of availability of physical buffer;
src/Pure/PIDE/markup.scala
src/Pure/PIDE/query_operation.ML
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/query_operation.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Aug 06 17:30:09 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Aug 06 21:08:04 2013 +0200
     1.3 @@ -245,6 +245,8 @@
     1.4    val FINISHED = "finished"
     1.5    val FAILED = "failed"
     1.6  
     1.7 +  val WAITING = "waiting"
     1.8 +
     1.9  
    1.10    /* interactive documents */
    1.11  
    1.12 @@ -283,9 +285,10 @@
    1.13    val WARNING_MESSAGE = "warning_message"
    1.14    val ERROR_MESSAGE = "error_message"
    1.15  
    1.16 -  val message: String => String =
    1.17 +  val messages =
    1.18      Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
    1.19 -        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
    1.20 +        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
    1.21 +  val message: String => String = messages.withDefault((s: String) => s)
    1.22  
    1.23    val Return_Code = new Properties.Int("return_code")
    1.24  
     2.1 --- a/src/Pure/PIDE/query_operation.ML	Tue Aug 06 17:30:09 2013 +0200
     2.2 +++ b/src/Pure/PIDE/query_operation.ML	Tue Aug 06 21:08:04 2013 +0200
     2.3 @@ -19,11 +19,17 @@
     2.4          SOME {delay = NONE, pri = 0, persistent = false,
     2.5            print_fn = fn _ => fn state =>
     2.6              let
     2.7 +              fun result s = Output.result [(Markup.instanceN, instance)] s;
     2.8 +              fun status m = result (Markup.markup_only m);
     2.9 +
    2.10 +              val _ = status Markup.running;
    2.11                val msg = XML.Elem ((Markup.writelnN, []), [XML.Text (f state args)])
    2.12                  handle exn =>
    2.13                    if Exn.is_interrupt exn then reraise exn
    2.14                    else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
    2.15 -            in Output.result [(Markup.instanceN, instance)] (YXML.string_of msg) end}
    2.16 +              val _ = result (YXML.string_of msg);
    2.17 +              val _ = status Markup.finished;
    2.18 +            in () end}
    2.19        | _ => NONE);
    2.20  
    2.21  end;
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 06 17:30:09 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 06 21:08:04 2013 +0200
     3.3 @@ -50,6 +50,20 @@
     3.4  
     3.5    /* document model and view */
     3.6  
     3.7 +  def document_snapshot(name: Document.Node.Name): Document.Snapshot =
     3.8 +  {
     3.9 +    Swing_Thread.require()
    3.10 +
    3.11 +    JEdit_Lib.jedit_buffer(name.node) match {
    3.12 +      case Some(buffer) =>
    3.13 +        document_model(buffer) match {
    3.14 +          case Some(model) => model.snapshot
    3.15 +          case None => session.snapshot(name)
    3.16 +        }
    3.17 +      case None => session.snapshot(name)
    3.18 +    }
    3.19 +  }
    3.20 +
    3.21    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    3.22    def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
    3.23  
     4.1 --- a/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 17:30:09 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:08:04 2013 +0200
     4.3 @@ -44,7 +44,7 @@
     4.4  
     4.5    val animation = new Label
     4.6    private val animation_icon =
     4.7 -    new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer)
     4.8 +    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
     4.9    animation.icon = animation_icon
    4.10  
    4.11    private def animation_rate(rate: Int)
    4.12 @@ -61,10 +61,18 @@
    4.13  
    4.14    private var current_location: Option[Command] = None
    4.15    private var current_query: List[String] = Nil
    4.16 -  private var current_result = false
    4.17 -  private var current_snapshot = Document.State.init.snapshot()
    4.18 -  private var current_state = Command.empty.init_state
    4.19 +  private var current_update_pending = false
    4.20    private var current_output: List[XML.Tree] = Nil
    4.21 +  private var current_status = Markup.FINISHED
    4.22 +
    4.23 +  private def reset_state()
    4.24 +  {
    4.25 +    current_location = None
    4.26 +    current_query = Nil
    4.27 +    current_update_pending = false
    4.28 +    current_output = Nil
    4.29 +    current_status = Markup.FINISHED
    4.30 +  }
    4.31  
    4.32    private def remove_overlay()
    4.33    {
    4.34 @@ -77,43 +85,72 @@
    4.35      } model.remove_overlay(command, operation_name, instance :: current_query)
    4.36    }
    4.37  
    4.38 -  private def handle_result()
    4.39 +  private def handle_update()
    4.40    {
    4.41      Swing_Thread.require()
    4.42  
    4.43 -    val (new_snapshot, new_state) =
    4.44 -      Document_View(view.getTextArea) match {
    4.45 -        case Some(doc_view) =>
    4.46 -          val snapshot = doc_view.model.snapshot()
    4.47 -          current_location match {
    4.48 -            case Some(cmd) =>
    4.49 -              (snapshot, snapshot.state.command_state(snapshot.version, cmd))
    4.50 -            case None =>
    4.51 -              (Document.State.init.snapshot(), Command.empty.init_state)
    4.52 -          }
    4.53 -        case None => (current_snapshot, current_state)
    4.54 +
    4.55 +    /* snapshot */
    4.56 +
    4.57 +    val (snapshot, state) =
    4.58 +      current_location match {
    4.59 +        case Some(cmd) =>
    4.60 +          val snapshot = PIDE.document_snapshot(cmd.node_name)
    4.61 +          val state = snapshot.state.command_state(snapshot.version, cmd)
    4.62 +          (snapshot, state)
    4.63 +        case None =>
    4.64 +          (Document.State.init.snapshot(), Command.empty.init_state)
    4.65        }
    4.66  
    4.67 +    val results =
    4.68 +      (for {
    4.69 +        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- state.results.entries
    4.70 +        if props.contains((Markup.INSTANCE, instance))
    4.71 +      } yield body).toList
    4.72 +
    4.73 +
    4.74 +    /* output */
    4.75 +
    4.76      val new_output =
    4.77 -      (for {
    4.78 -        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
    4.79 -          new_state.results.entries
    4.80 -        if props.contains((Markup.INSTANCE, instance))
    4.81 -      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
    4.82 +      for {
    4.83 +        List(XML.Elem(markup, body)) <- results
    4.84 +        if Markup.messages.contains(markup.name)
    4.85 +      }
    4.86 +      yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
    4.87 +
    4.88 +
    4.89 +    /* status */
    4.90  
    4.91 -    if (new_output != current_output)
    4.92 -      consume_result(new_snapshot, new_state.results, new_output)
    4.93 +    def status(name: String): Option[String] =
    4.94 +      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => name })
    4.95 +
    4.96 +    val new_status =
    4.97 +      status(Markup.FINISHED) orElse status(Markup.RUNNING) getOrElse Markup.WAITING
    4.98 +
    4.99 +
   4.100 +    /* state update */
   4.101  
   4.102 -    if (!new_output.isEmpty) {
   4.103 -      current_result = true
   4.104 -      animation_rate(0)
   4.105 -      remove_overlay()
   4.106 -      PIDE.flush_buffers()
   4.107 +    if (current_output != new_output || current_status != new_status) {
   4.108 +      if (snapshot.is_outdated)
   4.109 +        current_update_pending = true
   4.110 +      else {
   4.111 +        if (current_output != new_output)
   4.112 +          consume_result(snapshot, state.results, new_output)
   4.113 +        if (current_status != new_status)
   4.114 +          new_status match {
   4.115 +            case Markup.WAITING => animation_rate(5)
   4.116 +            case Markup.RUNNING => animation_rate(15)
   4.117 +            case Markup.FINISHED =>
   4.118 +              animation_rate(0)
   4.119 +              remove_overlay()
   4.120 +              PIDE.flush_buffers()
   4.121 +            case _ =>
   4.122 +          }
   4.123 +        current_output = new_output
   4.124 +        current_status = new_status
   4.125 +        current_update_pending = false
   4.126 +      }
   4.127      }
   4.128 -
   4.129 -    current_snapshot = new_snapshot
   4.130 -    current_state = new_state
   4.131 -    current_output = new_output
   4.132    }
   4.133  
   4.134    def apply_query(query: List[String])
   4.135 @@ -124,14 +161,14 @@
   4.136        case Some(doc_view) =>
   4.137          val snapshot = doc_view.model.snapshot()
   4.138          remove_overlay()
   4.139 -        current_location = None
   4.140 -        current_query = Nil
   4.141 -        current_result = false
   4.142 -        animation_rate(10)
   4.143 +        reset_state()
   4.144 +        animation_rate(0)
   4.145          snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
   4.146            case Some(command) =>
   4.147              current_location = Some(command)
   4.148              current_query = query
   4.149 +            current_status = Markup.WAITING
   4.150 +            animation_rate(5)
   4.151              doc_view.model.insert_overlay(command, operation_name, instance :: query)
   4.152            case None =>
   4.153          }
   4.154 @@ -146,9 +183,10 @@
   4.155  
   4.156      current_location match {
   4.157        case Some(command) =>
   4.158 -        val snapshot = PIDE.session.snapshot(command.node_name)
   4.159 +        val snapshot = PIDE.document_snapshot(command.node_name)
   4.160          val commands = snapshot.node.commands
   4.161          if (commands.contains(command)) {
   4.162 +          // FIXME revert offset (!?)
   4.163            val sources = commands.iterator.takeWhile(_ != command).map(_.source)
   4.164            val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   4.165            Hyperlink(command.node_name.node, line, column).follow(view)
   4.166 @@ -165,8 +203,10 @@
   4.167        react {
   4.168          case changed: Session.Commands_Changed =>
   4.169            current_location match {
   4.170 -            case Some(command) if !current_result && changed.commands.contains(command) =>
   4.171 -              Swing_Thread.later { handle_result() }
   4.172 +            case Some(command)
   4.173 +            if current_update_pending ||
   4.174 +              (current_status != Markup.FINISHED && changed.commands.contains(command)) =>
   4.175 +              Swing_Thread.later { handle_update() }
   4.176              case _ =>
   4.177            }
   4.178          case bad =>