src/Tools/jEdit/src/query_operation.scala
author wenzelm
Tue Aug 06 21:08:04 2013 +0200 (2013-08-06 ago)
changeset 52876 78989972d5b8
parent 52875 e2d5c3ff5c3f
child 52877 9a26ec5739dd
permissions -rw-r--r--
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;
wenzelm@52865
     1
/*  Title:      Tools/jEdit/src/query_operation.scala
wenzelm@52865
     2
    Author:     Makarius
wenzelm@52865
     3
wenzelm@52865
     4
One-shot query operations via asynchronous print functions and temporary
wenzelm@52865
     5
document overlay.
wenzelm@52865
     6
*/
wenzelm@52865
     7
wenzelm@52865
     8
package isabelle.jedit
wenzelm@52865
     9
wenzelm@52865
    10
wenzelm@52865
    11
import isabelle._
wenzelm@52865
    12
wenzelm@52865
    13
import scala.actors.Actor._
wenzelm@52874
    14
import scala.swing.Label
wenzelm@52865
    15
wenzelm@52865
    16
import org.gjt.sp.jedit.View
wenzelm@52874
    17
import org.gjt.sp.jedit.gui.AnimatedIcon
wenzelm@52865
    18
wenzelm@52865
    19
wenzelm@52865
    20
object Query_Operation
wenzelm@52865
    21
{
wenzelm@52865
    22
  def apply(
wenzelm@52865
    23
      view: View,
wenzelm@52865
    24
      name: String,
wenzelm@52865
    25
      consume: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
wenzelm@52865
    26
    new Query_Operation(view, name, consume)
wenzelm@52865
    27
}
wenzelm@52865
    28
wenzelm@52865
    29
final class Query_Operation private(
wenzelm@52865
    30
  view: View,
wenzelm@52865
    31
  operation_name: String,
wenzelm@52865
    32
  consume_result: (Document.Snapshot, Command.Results, XML.Body) => Unit)
wenzelm@52865
    33
{
wenzelm@52865
    34
  private val instance = Document_ID.make().toString
wenzelm@52865
    35
wenzelm@52865
    36
wenzelm@52875
    37
  /* animation */
wenzelm@52874
    38
wenzelm@52874
    39
  private val passive_icon =
wenzelm@52874
    40
    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
wenzelm@52874
    41
  private val active_icons =
wenzelm@52874
    42
    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
wenzelm@52874
    43
      JEdit_Lib.load_image_icon(name).getImage)
wenzelm@52874
    44
wenzelm@52874
    45
  val animation = new Label
wenzelm@52875
    46
  private val animation_icon =
wenzelm@52876
    47
    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
wenzelm@52874
    48
  animation.icon = animation_icon
wenzelm@52874
    49
wenzelm@52875
    50
  private def animation_rate(rate: Int)
wenzelm@52875
    51
  {
wenzelm@52875
    52
    animation_icon.stop
wenzelm@52875
    53
    if (rate > 0) {
wenzelm@52875
    54
      animation_icon.setRate(rate)
wenzelm@52875
    55
      animation_icon.start
wenzelm@52875
    56
    }
wenzelm@52875
    57
  }
wenzelm@52875
    58
wenzelm@52874
    59
wenzelm@52865
    60
  /* implicit state -- owned by Swing thread */
wenzelm@52865
    61
wenzelm@52865
    62
  private var current_location: Option[Command] = None
wenzelm@52865
    63
  private var current_query: List[String] = Nil
wenzelm@52876
    64
  private var current_update_pending = false
wenzelm@52865
    65
  private var current_output: List[XML.Tree] = Nil
wenzelm@52876
    66
  private var current_status = Markup.FINISHED
wenzelm@52876
    67
wenzelm@52876
    68
  private def reset_state()
wenzelm@52876
    69
  {
wenzelm@52876
    70
    current_location = None
wenzelm@52876
    71
    current_query = Nil
wenzelm@52876
    72
    current_update_pending = false
wenzelm@52876
    73
    current_output = Nil
wenzelm@52876
    74
    current_status = Markup.FINISHED
wenzelm@52876
    75
  }
wenzelm@52865
    76
wenzelm@52865
    77
  private def remove_overlay()
wenzelm@52865
    78
  {
wenzelm@52865
    79
    Swing_Thread.require()
wenzelm@52865
    80
wenzelm@52865
    81
    for {
wenzelm@52865
    82
      command <- current_location
wenzelm@52865
    83
      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
wenzelm@52865
    84
      model <- PIDE.document_model(buffer)
wenzelm@52865
    85
    } model.remove_overlay(command, operation_name, instance :: current_query)
wenzelm@52865
    86
  }
wenzelm@52865
    87
wenzelm@52876
    88
  private def handle_update()
wenzelm@52865
    89
  {
wenzelm@52865
    90
    Swing_Thread.require()
wenzelm@52865
    91
wenzelm@52876
    92
wenzelm@52876
    93
    /* snapshot */
wenzelm@52876
    94
wenzelm@52876
    95
    val (snapshot, state) =
wenzelm@52876
    96
      current_location match {
wenzelm@52876
    97
        case Some(cmd) =>
wenzelm@52876
    98
          val snapshot = PIDE.document_snapshot(cmd.node_name)
wenzelm@52876
    99
          val state = snapshot.state.command_state(snapshot.version, cmd)
wenzelm@52876
   100
          (snapshot, state)
wenzelm@52876
   101
        case None =>
wenzelm@52876
   102
          (Document.State.init.snapshot(), Command.empty.init_state)
wenzelm@52865
   103
      }
wenzelm@52865
   104
wenzelm@52876
   105
    val results =
wenzelm@52876
   106
      (for {
wenzelm@52876
   107
        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- state.results.entries
wenzelm@52876
   108
        if props.contains((Markup.INSTANCE, instance))
wenzelm@52876
   109
      } yield body).toList
wenzelm@52876
   110
wenzelm@52876
   111
wenzelm@52876
   112
    /* output */
wenzelm@52876
   113
wenzelm@52865
   114
    val new_output =
wenzelm@52876
   115
      for {
wenzelm@52876
   116
        List(XML.Elem(markup, body)) <- results
wenzelm@52876
   117
        if Markup.messages.contains(markup.name)
wenzelm@52876
   118
      }
wenzelm@52876
   119
      yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
wenzelm@52876
   120
wenzelm@52876
   121
wenzelm@52876
   122
    /* status */
wenzelm@52865
   123
wenzelm@52876
   124
    def status(name: String): Option[String] =
wenzelm@52876
   125
      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => name })
wenzelm@52876
   126
wenzelm@52876
   127
    val new_status =
wenzelm@52876
   128
      status(Markup.FINISHED) orElse status(Markup.RUNNING) getOrElse Markup.WAITING
wenzelm@52876
   129
wenzelm@52876
   130
wenzelm@52876
   131
    /* state update */
wenzelm@52865
   132
wenzelm@52876
   133
    if (current_output != new_output || current_status != new_status) {
wenzelm@52876
   134
      if (snapshot.is_outdated)
wenzelm@52876
   135
        current_update_pending = true
wenzelm@52876
   136
      else {
wenzelm@52876
   137
        if (current_output != new_output)
wenzelm@52876
   138
          consume_result(snapshot, state.results, new_output)
wenzelm@52876
   139
        if (current_status != new_status)
wenzelm@52876
   140
          new_status match {
wenzelm@52876
   141
            case Markup.WAITING => animation_rate(5)
wenzelm@52876
   142
            case Markup.RUNNING => animation_rate(15)
wenzelm@52876
   143
            case Markup.FINISHED =>
wenzelm@52876
   144
              animation_rate(0)
wenzelm@52876
   145
              remove_overlay()
wenzelm@52876
   146
              PIDE.flush_buffers()
wenzelm@52876
   147
            case _ =>
wenzelm@52876
   148
          }
wenzelm@52876
   149
        current_output = new_output
wenzelm@52876
   150
        current_status = new_status
wenzelm@52876
   151
        current_update_pending = false
wenzelm@52876
   152
      }
wenzelm@52865
   153
    }
wenzelm@52865
   154
  }
wenzelm@52865
   155
wenzelm@52865
   156
  def apply_query(query: List[String])
wenzelm@52865
   157
  {
wenzelm@52865
   158
    Swing_Thread.require()
wenzelm@52865
   159
wenzelm@52865
   160
    Document_View(view.getTextArea) match {
wenzelm@52865
   161
      case Some(doc_view) =>
wenzelm@52865
   162
        val snapshot = doc_view.model.snapshot()
wenzelm@52865
   163
        remove_overlay()
wenzelm@52876
   164
        reset_state()
wenzelm@52876
   165
        animation_rate(0)
wenzelm@52865
   166
        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
wenzelm@52865
   167
          case Some(command) =>
wenzelm@52865
   168
            current_location = Some(command)
wenzelm@52865
   169
            current_query = query
wenzelm@52876
   170
            current_status = Markup.WAITING
wenzelm@52876
   171
            animation_rate(5)
wenzelm@52865
   172
            doc_view.model.insert_overlay(command, operation_name, instance :: query)
wenzelm@52865
   173
          case None =>
wenzelm@52865
   174
        }
wenzelm@52865
   175
        PIDE.flush_buffers()
wenzelm@52865
   176
      case None =>
wenzelm@52865
   177
    }
wenzelm@52865
   178
  }
wenzelm@52865
   179
wenzelm@52865
   180
  def locate_query()
wenzelm@52865
   181
  {
wenzelm@52865
   182
    Swing_Thread.require()
wenzelm@52865
   183
wenzelm@52865
   184
    current_location match {
wenzelm@52865
   185
      case Some(command) =>
wenzelm@52876
   186
        val snapshot = PIDE.document_snapshot(command.node_name)
wenzelm@52865
   187
        val commands = snapshot.node.commands
wenzelm@52865
   188
        if (commands.contains(command)) {
wenzelm@52876
   189
          // FIXME revert offset (!?)
wenzelm@52865
   190
          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
wenzelm@52865
   191
          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@52865
   192
          Hyperlink(command.node_name.node, line, column).follow(view)
wenzelm@52865
   193
        }
wenzelm@52865
   194
      case None =>
wenzelm@52865
   195
    }
wenzelm@52865
   196
  }
wenzelm@52865
   197
wenzelm@52865
   198
wenzelm@52865
   199
  /* main actor */
wenzelm@52865
   200
wenzelm@52865
   201
  private val main_actor = actor {
wenzelm@52865
   202
    loop {
wenzelm@52865
   203
      react {
wenzelm@52865
   204
        case changed: Session.Commands_Changed =>
wenzelm@52865
   205
          current_location match {
wenzelm@52876
   206
            case Some(command)
wenzelm@52876
   207
            if current_update_pending ||
wenzelm@52876
   208
              (current_status != Markup.FINISHED && changed.commands.contains(command)) =>
wenzelm@52876
   209
              Swing_Thread.later { handle_update() }
wenzelm@52865
   210
            case _ =>
wenzelm@52865
   211
          }
wenzelm@52865
   212
        case bad =>
wenzelm@52865
   213
          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
wenzelm@52865
   214
      }
wenzelm@52865
   215
    }
wenzelm@52865
   216
  }
wenzelm@52865
   217
wenzelm@52865
   218
  def activate() { PIDE.session.commands_changed += main_actor }
wenzelm@52865
   219
  def deactivate() { PIDE.session.commands_changed -= main_actor }
wenzelm@52865
   220
}