src/Tools/jEdit/src/query_operation.scala
author wenzelm
Fri Aug 09 12:25:24 2013 +0200 (2013-08-09 ago)
changeset 52932 eb7d7c0034b5
parent 52931 ac6648c0c0fb
child 52934 bfb6873df88e
permissions -rw-r--r--
removed command location is considered finished, and its overlay removed eventually;
apply_query: empty output;
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@52932
     5
document overlays.
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@52932
    24
      operation_name: String,
wenzelm@52932
    25
      consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
wenzelm@52932
    26
    new Query_Operation(view, operation_name, consume_output)
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@52932
    32
  consume_output: (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@52877
    37
  /* implicit state -- owned by Swing thread */
wenzelm@52874
    38
wenzelm@52877
    39
  private object Status extends Enumeration
wenzelm@52875
    40
  {
wenzelm@52877
    41
    val WAITING = Value("waiting")
wenzelm@52877
    42
    val RUNNING = Value("running")
wenzelm@52877
    43
    val FINISHED = Value("finished")
wenzelm@52875
    44
  }
wenzelm@52875
    45
wenzelm@52865
    46
  private var current_location: Option[Command] = None
wenzelm@52865
    47
  private var current_query: List[String] = Nil
wenzelm@52876
    48
  private var current_update_pending = false
wenzelm@52865
    49
  private var current_output: List[XML.Tree] = Nil
wenzelm@52877
    50
  private var current_status = Status.FINISHED
wenzelm@52931
    51
  private var current_exec_id = Document_ID.none
wenzelm@52876
    52
wenzelm@52876
    53
  private def reset_state()
wenzelm@52876
    54
  {
wenzelm@52876
    55
    current_location = None
wenzelm@52876
    56
    current_query = Nil
wenzelm@52876
    57
    current_update_pending = false
wenzelm@52876
    58
    current_output = Nil
wenzelm@52877
    59
    current_status = Status.FINISHED
wenzelm@52931
    60
    current_exec_id = Document_ID.none
wenzelm@52876
    61
  }
wenzelm@52865
    62
wenzelm@52865
    63
  private def remove_overlay()
wenzelm@52865
    64
  {
wenzelm@52865
    65
    Swing_Thread.require()
wenzelm@52865
    66
wenzelm@52865
    67
    for {
wenzelm@52865
    68
      command <- current_location
wenzelm@52865
    69
      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
wenzelm@52865
    70
      model <- PIDE.document_model(buffer)
wenzelm@52865
    71
    } model.remove_overlay(command, operation_name, instance :: current_query)
wenzelm@52865
    72
  }
wenzelm@52865
    73
wenzelm@52877
    74
wenzelm@52877
    75
  /* animation */
wenzelm@52877
    76
wenzelm@52877
    77
  val animation = new Label
wenzelm@52877
    78
wenzelm@52877
    79
  private val passive_icon =
wenzelm@52877
    80
    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
wenzelm@52877
    81
  private val active_icons =
wenzelm@52877
    82
    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
wenzelm@52877
    83
      JEdit_Lib.load_image_icon(name).getImage)
wenzelm@52877
    84
wenzelm@52877
    85
  private val animation_icon =
wenzelm@52877
    86
    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
wenzelm@52877
    87
  animation.icon = animation_icon
wenzelm@52877
    88
wenzelm@52877
    89
  private def animation_update()
wenzelm@52877
    90
  {
wenzelm@52877
    91
    animation_icon.stop
wenzelm@52878
    92
    current_status match {
wenzelm@52878
    93
      case Status.WAITING =>
wenzelm@52878
    94
        animation.tooltip = "Waiting for evaluation of query context ..."
wenzelm@52878
    95
        animation_icon.setRate(5)
wenzelm@52878
    96
        animation_icon.start
wenzelm@52878
    97
      case Status.RUNNING =>
wenzelm@52878
    98
        animation.tooltip = "Running query operation ..."
wenzelm@52878
    99
        animation_icon.setRate(15)
wenzelm@52878
   100
        animation_icon.start
wenzelm@52878
   101
      case Status.FINISHED =>
wenzelm@52878
   102
        animation.tooltip = null
wenzelm@52877
   103
    }
wenzelm@52877
   104
  }
wenzelm@52877
   105
wenzelm@52877
   106
wenzelm@52877
   107
  /* content update */
wenzelm@52877
   108
wenzelm@52877
   109
  private def content_update()
wenzelm@52865
   110
  {
wenzelm@52865
   111
    Swing_Thread.require()
wenzelm@52865
   112
wenzelm@52876
   113
wenzelm@52876
   114
    /* snapshot */
wenzelm@52876
   115
wenzelm@52932
   116
    val (snapshot, state, removed) =
wenzelm@52876
   117
      current_location match {
wenzelm@52876
   118
        case Some(cmd) =>
wenzelm@52876
   119
          val snapshot = PIDE.document_snapshot(cmd.node_name)
wenzelm@52876
   120
          val state = snapshot.state.command_state(snapshot.version, cmd)
wenzelm@52932
   121
          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
wenzelm@52932
   122
          (snapshot, state, removed)
wenzelm@52876
   123
        case None =>
wenzelm@52932
   124
          (Document.State.init.snapshot(), Command.empty.init_state, true)
wenzelm@52865
   125
      }
wenzelm@52865
   126
wenzelm@52876
   127
    val results =
wenzelm@52876
   128
      (for {
wenzelm@52931
   129
        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
wenzelm@52876
   130
        if props.contains((Markup.INSTANCE, instance))
wenzelm@52931
   131
      } yield elem).toList
wenzelm@52876
   132
wenzelm@52876
   133
wenzelm@52876
   134
    /* output */
wenzelm@52876
   135
wenzelm@52865
   136
    val new_output =
wenzelm@52876
   137
      for {
wenzelm@52931
   138
        XML.Elem(_, List(XML.Elem(markup, body))) <- results
wenzelm@52876
   139
        if Markup.messages.contains(markup.name)
wenzelm@52931
   140
      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
wenzelm@52876
   141
wenzelm@52876
   142
wenzelm@52876
   143
    /* status */
wenzelm@52865
   144
wenzelm@52877
   145
    def get_status(name: String, status: Status.Value): Option[Status.Value] =
wenzelm@52931
   146
      results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
wenzelm@52876
   147
wenzelm@52876
   148
    val new_status =
wenzelm@52932
   149
      if (removed) Status.FINISHED
wenzelm@52932
   150
      else
wenzelm@52932
   151
        get_status(Markup.FINISHED, Status.FINISHED) orElse
wenzelm@52932
   152
        get_status(Markup.RUNNING, Status.RUNNING) getOrElse
wenzelm@52932
   153
        Status.WAITING
wenzelm@52876
   154
wenzelm@52931
   155
    if (new_status == Status.RUNNING)
wenzelm@52931
   156
      results.collectFirst(
wenzelm@52931
   157
      {
wenzelm@52931
   158
        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
wenzelm@52931
   159
        if elem.name == Markup.RUNNING => id
wenzelm@52931
   160
      }).foreach(id => current_exec_id = id)
wenzelm@52931
   161
wenzelm@52876
   162
wenzelm@52876
   163
    /* state update */
wenzelm@52865
   164
wenzelm@52876
   165
    if (current_output != new_output || current_status != new_status) {
wenzelm@52876
   166
      if (snapshot.is_outdated)
wenzelm@52876
   167
        current_update_pending = true
wenzelm@52876
   168
      else {
wenzelm@52877
   169
        current_update_pending = false
wenzelm@52932
   170
        if (current_output != new_output && !removed) {
wenzelm@52877
   171
          current_output = new_output
wenzelm@52932
   172
          consume_output(snapshot, state.results, new_output)
wenzelm@52877
   173
        }
wenzelm@52877
   174
        if (current_status != new_status) {
wenzelm@52877
   175
          current_status = new_status
wenzelm@52877
   176
          animation_update()
wenzelm@52877
   177
          if (new_status == Status.FINISHED) {
wenzelm@52877
   178
            remove_overlay()
wenzelm@52877
   179
            PIDE.flush_buffers()
wenzelm@52876
   180
          }
wenzelm@52877
   181
        }
wenzelm@52876
   182
      }
wenzelm@52865
   183
    }
wenzelm@52865
   184
  }
wenzelm@52865
   185
wenzelm@52877
   186
wenzelm@52931
   187
  /* query operations */
wenzelm@52931
   188
wenzelm@52931
   189
  def cancel_query(): Unit =
wenzelm@52931
   190
    Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) }
wenzelm@52877
   191
wenzelm@52865
   192
  def apply_query(query: List[String])
wenzelm@52865
   193
  {
wenzelm@52865
   194
    Swing_Thread.require()
wenzelm@52865
   195
wenzelm@52865
   196
    Document_View(view.getTextArea) match {
wenzelm@52865
   197
      case Some(doc_view) =>
wenzelm@52865
   198
        val snapshot = doc_view.model.snapshot()
wenzelm@52865
   199
        remove_overlay()
wenzelm@52876
   200
        reset_state()
wenzelm@52932
   201
        consume_output(Document.State.init.snapshot(), Command.Results.empty, Nil)
wenzelm@52865
   202
        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
wenzelm@52865
   203
          case Some(command) =>
wenzelm@52865
   204
            current_location = Some(command)
wenzelm@52865
   205
            current_query = query
wenzelm@52877
   206
            current_status = Status.WAITING
wenzelm@52865
   207
            doc_view.model.insert_overlay(command, operation_name, instance :: query)
wenzelm@52865
   208
          case None =>
wenzelm@52865
   209
        }
wenzelm@52877
   210
        animation_update()
wenzelm@52865
   211
        PIDE.flush_buffers()
wenzelm@52865
   212
      case None =>
wenzelm@52865
   213
    }
wenzelm@52865
   214
  }
wenzelm@52865
   215
wenzelm@52865
   216
  def locate_query()
wenzelm@52865
   217
  {
wenzelm@52865
   218
    Swing_Thread.require()
wenzelm@52865
   219
wenzelm@52865
   220
    current_location match {
wenzelm@52865
   221
      case Some(command) =>
wenzelm@52876
   222
        val snapshot = PIDE.document_snapshot(command.node_name)
wenzelm@52865
   223
        val commands = snapshot.node.commands
wenzelm@52865
   224
        if (commands.contains(command)) {
wenzelm@52876
   225
          // FIXME revert offset (!?)
wenzelm@52865
   226
          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
wenzelm@52865
   227
          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@52865
   228
          Hyperlink(command.node_name.node, line, column).follow(view)
wenzelm@52865
   229
        }
wenzelm@52865
   230
      case None =>
wenzelm@52865
   231
    }
wenzelm@52865
   232
  }
wenzelm@52865
   233
wenzelm@52865
   234
wenzelm@52865
   235
  /* main actor */
wenzelm@52865
   236
wenzelm@52865
   237
  private val main_actor = actor {
wenzelm@52865
   238
    loop {
wenzelm@52865
   239
      react {
wenzelm@52865
   240
        case changed: Session.Commands_Changed =>
wenzelm@52865
   241
          current_location match {
wenzelm@52876
   242
            case Some(command)
wenzelm@52876
   243
            if current_update_pending ||
wenzelm@52877
   244
              (current_status != Status.FINISHED && changed.commands.contains(command)) =>
wenzelm@52877
   245
              Swing_Thread.later { content_update() }
wenzelm@52865
   246
            case _ =>
wenzelm@52865
   247
          }
wenzelm@52865
   248
        case bad =>
wenzelm@52865
   249
          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
wenzelm@52865
   250
      }
wenzelm@52865
   251
    }
wenzelm@52865
   252
  }
wenzelm@52865
   253
wenzelm@52865
   254
  def activate() { PIDE.session.commands_changed += main_actor }
wenzelm@52865
   255
  def deactivate() { PIDE.session.commands_changed -= main_actor }
wenzelm@52865
   256
}