src/Pure/PIDE/query_operation.scala
author wenzelm
Sat Mar 01 22:46:31 2014 +0100 (2014-03-01)
changeset 55828 42ac3cfb89f6
parent 55618 995162143ef4
child 56299 8201790fdeb9
permissions -rw-r--r--
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
wenzelm@52981
     1
/*  Title:      Pure/PIDE/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@52981
     8
package isabelle
wenzelm@52865
     9
wenzelm@52865
    10
wenzelm@52865
    11
import scala.actors.Actor._
wenzelm@52865
    12
wenzelm@52865
    13
wenzelm@52865
    14
object Query_Operation
wenzelm@52865
    15
{
wenzelm@52935
    16
  object Status extends Enumeration
wenzelm@52935
    17
  {
wenzelm@52935
    18
    val WAITING = Value("waiting")
wenzelm@52935
    19
    val RUNNING = Value("running")
wenzelm@52935
    20
    val FINISHED = Value("finished")
wenzelm@52935
    21
  }
wenzelm@52865
    22
}
wenzelm@52865
    23
wenzelm@52980
    24
class Query_Operation[Editor_Context](
wenzelm@52980
    25
  editor: Editor[Editor_Context],
wenzelm@52980
    26
  editor_context: Editor_Context,
wenzelm@52865
    27
  operation_name: String,
wenzelm@52935
    28
  consume_status: Query_Operation.Status.Value => Unit,
wenzelm@52932
    29
  consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
wenzelm@52865
    30
{
wenzelm@52865
    31
  private val instance = Document_ID.make().toString
wenzelm@52865
    32
wenzelm@52865
    33
wenzelm@52877
    34
  /* implicit state -- owned by Swing thread */
wenzelm@52874
    35
wenzelm@52865
    36
  private var current_location: Option[Command] = None
wenzelm@52865
    37
  private var current_query: List[String] = Nil
wenzelm@52876
    38
  private var current_update_pending = false
wenzelm@52865
    39
  private var current_output: List[XML.Tree] = Nil
wenzelm@54640
    40
  private var current_status = Query_Operation.Status.FINISHED
wenzelm@52931
    41
  private var current_exec_id = Document_ID.none
wenzelm@52876
    42
wenzelm@52876
    43
  private def reset_state()
wenzelm@52876
    44
  {
wenzelm@52876
    45
    current_location = None
wenzelm@52876
    46
    current_query = Nil
wenzelm@52876
    47
    current_update_pending = false
wenzelm@52876
    48
    current_output = Nil
wenzelm@54640
    49
    current_status = Query_Operation.Status.FINISHED
wenzelm@52931
    50
    current_exec_id = Document_ID.none
wenzelm@52876
    51
  }
wenzelm@52865
    52
wenzelm@52865
    53
  private def remove_overlay()
wenzelm@52865
    54
  {
wenzelm@54310
    55
    current_location match {
wenzelm@54310
    56
      case None =>
wenzelm@54310
    57
      case Some(command) =>
wenzelm@54310
    58
        editor.remove_overlay(command, operation_name, instance :: current_query)
wenzelm@54310
    59
        editor.flush()
wenzelm@54310
    60
    }
wenzelm@52865
    61
  }
wenzelm@52865
    62
wenzelm@52877
    63
wenzelm@52877
    64
  /* content update */
wenzelm@52877
    65
wenzelm@52877
    66
  private def content_update()
wenzelm@52865
    67
  {
wenzelm@52865
    68
    Swing_Thread.require()
wenzelm@52865
    69
wenzelm@52876
    70
wenzelm@52876
    71
    /* snapshot */
wenzelm@52876
    72
wenzelm@52932
    73
    val (snapshot, state, removed) =
wenzelm@52876
    74
      current_location match {
wenzelm@52876
    75
        case Some(cmd) =>
wenzelm@52974
    76
          val snapshot = editor.node_snapshot(cmd.node_name)
wenzelm@52876
    77
          val state = snapshot.state.command_state(snapshot.version, cmd)
wenzelm@52932
    78
          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
wenzelm@52932
    79
          (snapshot, state, removed)
wenzelm@52876
    80
        case None =>
wenzelm@52972
    81
          (Document.Snapshot.init, Command.empty.init_state, true)
wenzelm@52865
    82
      }
wenzelm@52865
    83
wenzelm@52876
    84
    val results =
wenzelm@52876
    85
      (for {
wenzelm@52931
    86
        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
wenzelm@52876
    87
        if props.contains((Markup.INSTANCE, instance))
wenzelm@52931
    88
      } yield elem).toList
wenzelm@52876
    89
wenzelm@52876
    90
wenzelm@54640
    91
    /* resolve sendback: static command id */
wenzelm@54640
    92
wenzelm@54640
    93
    def resolve_sendback(body: XML.Body): XML.Body =
wenzelm@54640
    94
    {
wenzelm@54640
    95
      current_location match {
wenzelm@54640
    96
        case None => body
wenzelm@54640
    97
        case Some(command) =>
wenzelm@54640
    98
          def resolve(body: XML.Body): XML.Body =
wenzelm@54640
    99
            body map {
wenzelm@54640
   100
              case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
wenzelm@54640
   101
              case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
wenzelm@54640
   102
                val props1 =
wenzelm@54640
   103
                  props.map({
wenzelm@54640
   104
                    case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
wenzelm@54640
   105
                      (Markup.ID, Properties.Value.Long(command.id))
wenzelm@54640
   106
                    case p => p
wenzelm@54640
   107
                  })
wenzelm@54640
   108
                XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
wenzelm@54640
   109
              case XML.Elem(m, b) => XML.Elem(m, resolve(b))
wenzelm@54640
   110
              case t => t
wenzelm@54640
   111
            }
wenzelm@54640
   112
          resolve(body)
wenzelm@54640
   113
      }
wenzelm@54640
   114
    }
wenzelm@54640
   115
wenzelm@54640
   116
wenzelm@52876
   117
    /* output */
wenzelm@52876
   118
wenzelm@52865
   119
    val new_output =
wenzelm@52876
   120
      for {
wenzelm@52931
   121
        XML.Elem(_, List(XML.Elem(markup, body))) <- results
wenzelm@52876
   122
        if Markup.messages.contains(markup.name)
wenzelm@54640
   123
        body1 = resolve_sendback(body)
wenzelm@54640
   124
      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
wenzelm@52876
   125
wenzelm@52876
   126
wenzelm@52876
   127
    /* status */
wenzelm@52865
   128
wenzelm@52935
   129
    def get_status(name: String, status: Query_Operation.Status.Value)
wenzelm@52935
   130
        : Option[Query_Operation.Status.Value] =
wenzelm@52931
   131
      results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
wenzelm@52876
   132
wenzelm@52876
   133
    val new_status =
wenzelm@54640
   134
      if (removed) Query_Operation.Status.FINISHED
wenzelm@52932
   135
      else
wenzelm@52935
   136
        get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
wenzelm@52935
   137
        get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
wenzelm@52935
   138
        Query_Operation.Status.WAITING
wenzelm@52876
   139
wenzelm@52935
   140
    if (new_status == Query_Operation.Status.RUNNING)
wenzelm@52931
   141
      results.collectFirst(
wenzelm@52931
   142
      {
wenzelm@52931
   143
        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
wenzelm@52931
   144
        if elem.name == Markup.RUNNING => id
wenzelm@52931
   145
      }).foreach(id => current_exec_id = id)
wenzelm@52931
   146
wenzelm@52876
   147
wenzelm@52876
   148
    /* state update */
wenzelm@52865
   149
wenzelm@52876
   150
    if (current_output != new_output || current_status != new_status) {
wenzelm@52876
   151
      if (snapshot.is_outdated)
wenzelm@52876
   152
        current_update_pending = true
wenzelm@52876
   153
      else {
wenzelm@52877
   154
        current_update_pending = false
wenzelm@52932
   155
        if (current_output != new_output && !removed) {
wenzelm@52877
   156
          current_output = new_output
wenzelm@52932
   157
          consume_output(snapshot, state.results, new_output)
wenzelm@52877
   158
        }
wenzelm@52877
   159
        if (current_status != new_status) {
wenzelm@52877
   160
          current_status = new_status
wenzelm@52935
   161
          consume_status(new_status)
wenzelm@54640
   162
          if (new_status == Query_Operation.Status.FINISHED)
wenzelm@52877
   163
            remove_overlay()
wenzelm@52877
   164
        }
wenzelm@52876
   165
      }
wenzelm@52865
   166
    }
wenzelm@52865
   167
  }
wenzelm@52865
   168
wenzelm@52877
   169
wenzelm@52931
   170
  /* query operations */
wenzelm@52931
   171
wenzelm@52931
   172
  def cancel_query(): Unit =
wenzelm@52971
   173
    Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
wenzelm@52877
   174
wenzelm@52865
   175
  def apply_query(query: List[String])
wenzelm@52865
   176
  {
wenzelm@52865
   177
    Swing_Thread.require()
wenzelm@52865
   178
wenzelm@52980
   179
    editor.current_node_snapshot(editor_context) match {
wenzelm@52978
   180
      case Some(snapshot) =>
wenzelm@52865
   181
        remove_overlay()
wenzelm@52876
   182
        reset_state()
wenzelm@52972
   183
        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
wenzelm@54325
   184
        if (!snapshot.is_outdated) {
wenzelm@54325
   185
          editor.current_command(editor_context, snapshot) match {
wenzelm@54325
   186
            case Some(command) =>
wenzelm@54325
   187
              current_location = Some(command)
wenzelm@54325
   188
              current_query = query
wenzelm@54325
   189
              current_status = Query_Operation.Status.WAITING
wenzelm@54325
   190
              editor.insert_overlay(command, operation_name, instance :: query)
wenzelm@54325
   191
            case None =>
wenzelm@54325
   192
          }
wenzelm@52865
   193
        }
wenzelm@52935
   194
        consume_status(current_status)
wenzelm@52974
   195
        editor.flush()
wenzelm@52865
   196
      case None =>
wenzelm@52865
   197
    }
wenzelm@52865
   198
  }
wenzelm@52865
   199
wenzelm@52865
   200
  def locate_query()
wenzelm@52865
   201
  {
wenzelm@52865
   202
    Swing_Thread.require()
wenzelm@52865
   203
wenzelm@52980
   204
    for {
wenzelm@52980
   205
      command <- current_location
wenzelm@52980
   206
      snapshot = editor.node_snapshot(command.node_name)
wenzelm@52980
   207
      link <- editor.hyperlink_command(snapshot, command)
wenzelm@52980
   208
    } link.follow(editor_context)
wenzelm@52865
   209
  }
wenzelm@52865
   210
wenzelm@52865
   211
wenzelm@52865
   212
  /* main actor */
wenzelm@52865
   213
wenzelm@52865
   214
  private val main_actor = actor {
wenzelm@52865
   215
    loop {
wenzelm@52865
   216
      react {
wenzelm@52865
   217
        case changed: Session.Commands_Changed =>
wenzelm@52865
   218
          current_location match {
wenzelm@52876
   219
            case Some(command)
wenzelm@52876
   220
            if current_update_pending ||
wenzelm@54640
   221
              (current_status != Query_Operation.Status.FINISHED &&
wenzelm@52935
   222
                changed.commands.contains(command)) =>
wenzelm@52877
   223
              Swing_Thread.later { content_update() }
wenzelm@52865
   224
            case _ =>
wenzelm@52865
   225
          }
wenzelm@52865
   226
        case bad =>
wenzelm@55618
   227
          System.err.println("Query_Operation: ignoring bad message " + bad)
wenzelm@52865
   228
      }
wenzelm@52865
   229
    }
wenzelm@52865
   230
  }
wenzelm@52865
   231
wenzelm@53840
   232
  def activate() {
wenzelm@53840
   233
    editor.session.commands_changed += main_actor
wenzelm@53840
   234
  }
wenzelm@53000
   235
wenzelm@53000
   236
  def deactivate() {
wenzelm@53000
   237
    editor.session.commands_changed -= main_actor
wenzelm@53000
   238
    remove_overlay()
wenzelm@54327
   239
    reset_state()
wenzelm@54327
   240
    consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
wenzelm@54327
   241
    consume_status(current_status)
wenzelm@53000
   242
  }
wenzelm@52865
   243
}