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