src/Tools/jEdit/src/query_operation.scala
author wenzelm
Mon Aug 12 11:49:58 2013 +0200 (2013-08-12 ago)
changeset 52972 8fd8e1c14988
parent 52971 31926d2c04ee
child 52974 908e8a36e975
permissions -rw-r--r--
tuned signature;
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@52865
    14
wenzelm@52865
    15
import org.gjt.sp.jedit.View
wenzelm@52865
    16
wenzelm@52865
    17
wenzelm@52865
    18
object Query_Operation
wenzelm@52865
    19
{
wenzelm@52935
    20
  object Status extends Enumeration
wenzelm@52935
    21
  {
wenzelm@52935
    22
    val WAITING = Value("waiting")
wenzelm@52935
    23
    val RUNNING = Value("running")
wenzelm@52935
    24
    val FINISHED = Value("finished")
wenzelm@52935
    25
  }
wenzelm@52865
    26
}
wenzelm@52865
    27
wenzelm@52971
    28
class Query_Operation(
wenzelm@52971
    29
  editor: Editor[View],
wenzelm@52865
    30
  view: View,
wenzelm@52865
    31
  operation_name: String,
wenzelm@52935
    32
  consume_status: Query_Operation.Status.Value => Unit,
wenzelm@52932
    33
  consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
wenzelm@52865
    34
{
wenzelm@52865
    35
  private val instance = Document_ID.make().toString
wenzelm@52865
    36
wenzelm@52865
    37
wenzelm@52877
    38
  /* implicit state -- owned by Swing thread */
wenzelm@52874
    39
wenzelm@52865
    40
  private var current_location: Option[Command] = None
wenzelm@52865
    41
  private var current_query: List[String] = Nil
wenzelm@52876
    42
  private var current_update_pending = false
wenzelm@52865
    43
  private var current_output: List[XML.Tree] = Nil
wenzelm@52935
    44
  private var current_status = Query_Operation.Status.FINISHED
wenzelm@52931
    45
  private var current_exec_id = Document_ID.none
wenzelm@52876
    46
wenzelm@52876
    47
  private def reset_state()
wenzelm@52876
    48
  {
wenzelm@52876
    49
    current_location = None
wenzelm@52876
    50
    current_query = Nil
wenzelm@52876
    51
    current_update_pending = false
wenzelm@52876
    52
    current_output = Nil
wenzelm@52935
    53
    current_status = Query_Operation.Status.FINISHED
wenzelm@52931
    54
    current_exec_id = Document_ID.none
wenzelm@52876
    55
  }
wenzelm@52865
    56
wenzelm@52865
    57
  private def remove_overlay()
wenzelm@52865
    58
  {
wenzelm@52865
    59
    Swing_Thread.require()
wenzelm@52865
    60
wenzelm@52865
    61
    for {
wenzelm@52865
    62
      command <- current_location
wenzelm@52865
    63
      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
wenzelm@52865
    64
      model <- PIDE.document_model(buffer)
wenzelm@52865
    65
    } model.remove_overlay(command, operation_name, instance :: current_query)
wenzelm@52865
    66
  }
wenzelm@52865
    67
wenzelm@52877
    68
wenzelm@52877
    69
  /* content update */
wenzelm@52877
    70
wenzelm@52877
    71
  private def content_update()
wenzelm@52865
    72
  {
wenzelm@52865
    73
    Swing_Thread.require()
wenzelm@52865
    74
wenzelm@52876
    75
wenzelm@52876
    76
    /* snapshot */
wenzelm@52876
    77
wenzelm@52932
    78
    val (snapshot, state, removed) =
wenzelm@52876
    79
      current_location match {
wenzelm@52876
    80
        case Some(cmd) =>
wenzelm@52876
    81
          val snapshot = PIDE.document_snapshot(cmd.node_name)
wenzelm@52876
    82
          val state = snapshot.state.command_state(snapshot.version, cmd)
wenzelm@52932
    83
          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
wenzelm@52932
    84
          (snapshot, state, removed)
wenzelm@52876
    85
        case None =>
wenzelm@52972
    86
          (Document.Snapshot.init, Command.empty.init_state, true)
wenzelm@52865
    87
      }
wenzelm@52865
    88
wenzelm@52876
    89
    val results =
wenzelm@52876
    90
      (for {
wenzelm@52931
    91
        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
wenzelm@52876
    92
        if props.contains((Markup.INSTANCE, instance))
wenzelm@52931
    93
      } yield elem).toList
wenzelm@52876
    94
wenzelm@52876
    95
wenzelm@52876
    96
    /* output */
wenzelm@52876
    97
wenzelm@52865
    98
    val new_output =
wenzelm@52876
    99
      for {
wenzelm@52931
   100
        XML.Elem(_, List(XML.Elem(markup, body))) <- results
wenzelm@52876
   101
        if Markup.messages.contains(markup.name)
wenzelm@52931
   102
      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
wenzelm@52876
   103
wenzelm@52876
   104
wenzelm@52876
   105
    /* status */
wenzelm@52865
   106
wenzelm@52935
   107
    def get_status(name: String, status: Query_Operation.Status.Value)
wenzelm@52935
   108
        : Option[Query_Operation.Status.Value] =
wenzelm@52931
   109
      results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
wenzelm@52876
   110
wenzelm@52876
   111
    val new_status =
wenzelm@52935
   112
      if (removed) Query_Operation.Status.FINISHED
wenzelm@52932
   113
      else
wenzelm@52935
   114
        get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
wenzelm@52935
   115
        get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
wenzelm@52935
   116
        Query_Operation.Status.WAITING
wenzelm@52876
   117
wenzelm@52935
   118
    if (new_status == Query_Operation.Status.RUNNING)
wenzelm@52931
   119
      results.collectFirst(
wenzelm@52931
   120
      {
wenzelm@52931
   121
        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
wenzelm@52931
   122
        if elem.name == Markup.RUNNING => id
wenzelm@52931
   123
      }).foreach(id => current_exec_id = id)
wenzelm@52931
   124
wenzelm@52876
   125
wenzelm@52876
   126
    /* state update */
wenzelm@52865
   127
wenzelm@52876
   128
    if (current_output != new_output || current_status != new_status) {
wenzelm@52876
   129
      if (snapshot.is_outdated)
wenzelm@52876
   130
        current_update_pending = true
wenzelm@52876
   131
      else {
wenzelm@52877
   132
        current_update_pending = false
wenzelm@52932
   133
        if (current_output != new_output && !removed) {
wenzelm@52877
   134
          current_output = new_output
wenzelm@52932
   135
          consume_output(snapshot, state.results, new_output)
wenzelm@52877
   136
        }
wenzelm@52877
   137
        if (current_status != new_status) {
wenzelm@52877
   138
          current_status = new_status
wenzelm@52935
   139
          consume_status(new_status)
wenzelm@52935
   140
          if (new_status == Query_Operation.Status.FINISHED) {
wenzelm@52877
   141
            remove_overlay()
wenzelm@52877
   142
            PIDE.flush_buffers()
wenzelm@52876
   143
          }
wenzelm@52877
   144
        }
wenzelm@52876
   145
      }
wenzelm@52865
   146
    }
wenzelm@52865
   147
  }
wenzelm@52865
   148
wenzelm@52877
   149
wenzelm@52931
   150
  /* query operations */
wenzelm@52931
   151
wenzelm@52931
   152
  def cancel_query(): Unit =
wenzelm@52971
   153
    Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
wenzelm@52877
   154
wenzelm@52865
   155
  def apply_query(query: List[String])
wenzelm@52865
   156
  {
wenzelm@52865
   157
    Swing_Thread.require()
wenzelm@52865
   158
wenzelm@52865
   159
    Document_View(view.getTextArea) match {
wenzelm@52865
   160
      case Some(doc_view) =>
wenzelm@52865
   161
        val snapshot = doc_view.model.snapshot()
wenzelm@52865
   162
        remove_overlay()
wenzelm@52876
   163
        reset_state()
wenzelm@52972
   164
        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
wenzelm@52865
   165
        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
wenzelm@52865
   166
          case Some(command) =>
wenzelm@52865
   167
            current_location = Some(command)
wenzelm@52865
   168
            current_query = query
wenzelm@52935
   169
            current_status = Query_Operation.Status.WAITING
wenzelm@52865
   170
            doc_view.model.insert_overlay(command, operation_name, instance :: query)
wenzelm@52865
   171
          case None =>
wenzelm@52865
   172
        }
wenzelm@52935
   173
        consume_status(current_status)
wenzelm@52865
   174
        PIDE.flush_buffers()
wenzelm@52865
   175
      case None =>
wenzelm@52865
   176
    }
wenzelm@52865
   177
  }
wenzelm@52865
   178
wenzelm@52865
   179
  def locate_query()
wenzelm@52865
   180
  {
wenzelm@52865
   181
    Swing_Thread.require()
wenzelm@52865
   182
wenzelm@52865
   183
    current_location match {
wenzelm@52865
   184
      case Some(command) =>
wenzelm@52876
   185
        val snapshot = PIDE.document_snapshot(command.node_name)
wenzelm@52865
   186
        val commands = snapshot.node.commands
wenzelm@52865
   187
        if (commands.contains(command)) {
wenzelm@52876
   188
          // FIXME revert offset (!?)
wenzelm@52865
   189
          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
wenzelm@52865
   190
          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@52865
   191
          Hyperlink(command.node_name.node, line, column).follow(view)
wenzelm@52865
   192
        }
wenzelm@52865
   193
      case None =>
wenzelm@52865
   194
    }
wenzelm@52865
   195
  }
wenzelm@52865
   196
wenzelm@52865
   197
wenzelm@52865
   198
  /* main actor */
wenzelm@52865
   199
wenzelm@52865
   200
  private val main_actor = actor {
wenzelm@52865
   201
    loop {
wenzelm@52865
   202
      react {
wenzelm@52865
   203
        case changed: Session.Commands_Changed =>
wenzelm@52865
   204
          current_location match {
wenzelm@52876
   205
            case Some(command)
wenzelm@52876
   206
            if current_update_pending ||
wenzelm@52935
   207
              (current_status != Query_Operation.Status.FINISHED &&
wenzelm@52935
   208
                changed.commands.contains(command)) =>
wenzelm@52877
   209
              Swing_Thread.later { content_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@52971
   218
  def activate() { editor.session.commands_changed += main_actor }
wenzelm@52971
   219
  def deactivate() { editor.session.commands_changed -= main_actor }
wenzelm@52865
   220
}