src/Pure/PIDE/query_operation.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 66110 8b433b6f302f
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
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@61546
    19
wenzelm@61546
    20
  object State
wenzelm@61546
    21
  {
wenzelm@61546
    22
    val empty: State = State()
wenzelm@61546
    23
wenzelm@61546
    24
    def make(command: Command, query: List[String]): State =
wenzelm@61546
    25
      State(instance = Document_ID.make().toString,
wenzelm@61546
    26
        location = Some(command),
wenzelm@61546
    27
        query = query,
wenzelm@61546
    28
        status = Status.WAITING)
wenzelm@61546
    29
  }
wenzelm@61546
    30
wenzelm@61546
    31
  sealed case class State(
wenzelm@61546
    32
    instance: String = Document_ID.none.toString,
wenzelm@61546
    33
    location: Option[Command] = None,
wenzelm@61546
    34
    query: List[String] = Nil,
wenzelm@61546
    35
    update_pending: Boolean = false,
wenzelm@61546
    36
    output: List[XML.Tree] = Nil,
wenzelm@61546
    37
    status: Status.Value = Status.FINISHED,
wenzelm@61546
    38
    exec_id: Document_ID.Exec = Document_ID.none)
wenzelm@52865
    39
}
wenzelm@52865
    40
wenzelm@52980
    41
class Query_Operation[Editor_Context](
wenzelm@52980
    42
  editor: Editor[Editor_Context],
wenzelm@52980
    43
  editor_context: Editor_Context,
wenzelm@52865
    44
  operation_name: String,
wenzelm@52935
    45
  consume_status: Query_Operation.Status.Value => Unit,
wenzelm@52932
    46
  consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
wenzelm@52865
    47
{
wenzelm@61206
    48
  private val print_function = operation_name + "_query"
wenzelm@52865
    49
wenzelm@52865
    50
wenzelm@66094
    51
  /* implicit state -- owned by editor thread */
wenzelm@52874
    52
wenzelm@61546
    53
  private val current_state = Synchronized(Query_Operation.State.empty)
wenzelm@61210
    54
wenzelm@61546
    55
  def get_location: Option[Command] = current_state.value.location
wenzelm@52865
    56
wenzelm@52865
    57
  private def remove_overlay()
wenzelm@52865
    58
  {
wenzelm@61546
    59
    val state = current_state.value
wenzelm@61546
    60
    for (command <- state.location) {
wenzelm@61546
    61
      editor.remove_overlay(command, print_function, state.instance :: state.query)
wenzelm@54310
    62
    }
wenzelm@52865
    63
  }
wenzelm@52865
    64
wenzelm@52877
    65
wenzelm@52877
    66
  /* content update */
wenzelm@52877
    67
wenzelm@52877
    68
  private def content_update()
wenzelm@52865
    69
  {
wenzelm@66094
    70
    editor.require_dispatcher {}
wenzelm@52865
    71
wenzelm@52876
    72
wenzelm@52876
    73
    /* snapshot */
wenzelm@52876
    74
wenzelm@61546
    75
    val state0 = current_state.value
wenzelm@61546
    76
wenzelm@61546
    77
    val (snapshot, command_results, results, removed) =
wenzelm@61546
    78
      state0.location match {
wenzelm@52876
    79
        case Some(cmd) =>
wenzelm@52974
    80
          val snapshot = editor.node_snapshot(cmd.node_name)
wenzelm@65195
    81
          val command_results = snapshot.command_results(cmd)
wenzelm@61546
    82
          val results =
wenzelm@61546
    83
            (for {
wenzelm@61546
    84
              (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
wenzelm@61546
    85
              if props.contains((Markup.INSTANCE, state0.instance))
wenzelm@61546
    86
            } yield elem).toList
wenzelm@52932
    87
          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
wenzelm@61546
    88
          (snapshot, command_results, results, removed)
wenzelm@52876
    89
        case None =>
wenzelm@61546
    90
          (Document.Snapshot.init, Command.Results.empty, Nil, true)
wenzelm@52865
    91
      }
wenzelm@52865
    92
wenzelm@52876
    93
wenzelm@52876
    94
wenzelm@54640
    95
    /* resolve sendback: static command id */
wenzelm@54640
    96
wenzelm@54640
    97
    def resolve_sendback(body: XML.Body): XML.Body =
wenzelm@54640
    98
    {
wenzelm@61546
    99
      state0.location match {
wenzelm@54640
   100
        case None => body
wenzelm@54640
   101
        case Some(command) =>
wenzelm@54640
   102
          def resolve(body: XML.Body): XML.Body =
wenzelm@54640
   103
            body map {
wenzelm@54640
   104
              case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
wenzelm@54640
   105
              case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
wenzelm@54640
   106
                val props1 =
wenzelm@54640
   107
                  props.map({
wenzelm@63805
   108
                    case (Markup.ID, Value.Long(id)) if id == state0.exec_id =>
wenzelm@63805
   109
                      (Markup.ID, Value.Long(command.id))
wenzelm@54640
   110
                    case p => p
wenzelm@54640
   111
                  })
wenzelm@54640
   112
                XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
wenzelm@54640
   113
              case XML.Elem(m, b) => XML.Elem(m, resolve(b))
wenzelm@54640
   114
              case t => t
wenzelm@54640
   115
            }
wenzelm@54640
   116
          resolve(body)
wenzelm@54640
   117
      }
wenzelm@54640
   118
    }
wenzelm@54640
   119
wenzelm@54640
   120
wenzelm@52876
   121
    /* output */
wenzelm@52876
   122
wenzelm@52865
   123
    val new_output =
wenzelm@52876
   124
      for {
wenzelm@52931
   125
        XML.Elem(_, List(XML.Elem(markup, body))) <- results
wenzelm@52876
   126
        if Markup.messages.contains(markup.name)
wenzelm@54640
   127
        body1 = resolve_sendback(body)
wenzelm@54640
   128
      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
wenzelm@52876
   129
wenzelm@52876
   130
wenzelm@52876
   131
    /* status */
wenzelm@52865
   132
wenzelm@52935
   133
    def get_status(name: String, status: Query_Operation.Status.Value)
wenzelm@52935
   134
        : Option[Query_Operation.Status.Value] =
wenzelm@52931
   135
      results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
wenzelm@52876
   136
wenzelm@52876
   137
    val new_status =
wenzelm@54640
   138
      if (removed) Query_Operation.Status.FINISHED
wenzelm@52932
   139
      else
wenzelm@52935
   140
        get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
wenzelm@52935
   141
        get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
wenzelm@52935
   142
        Query_Operation.Status.WAITING
wenzelm@52876
   143
wenzelm@61546
   144
wenzelm@61546
   145
    /* state update */
wenzelm@61546
   146
wenzelm@52935
   147
    if (new_status == Query_Operation.Status.RUNNING)
wenzelm@52931
   148
      results.collectFirst(
wenzelm@52931
   149
      {
wenzelm@52931
   150
        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
wenzelm@52931
   151
        if elem.name == Markup.RUNNING => id
wenzelm@61546
   152
      }).foreach(id => current_state.change(_.copy(exec_id = id)))
wenzelm@52865
   153
wenzelm@61546
   154
    if (state0.output != new_output || state0.status != new_status) {
wenzelm@52876
   155
      if (snapshot.is_outdated)
wenzelm@61546
   156
        current_state.change(_.copy(update_pending = true))
wenzelm@52876
   157
      else {
wenzelm@61546
   158
        current_state.change(_.copy(update_pending = false))
wenzelm@61546
   159
        if (state0.output != new_output && !removed) {
wenzelm@61546
   160
          current_state.change(_.copy(output = new_output))
wenzelm@56299
   161
          consume_output(snapshot, command_results, new_output)
wenzelm@52877
   162
        }
wenzelm@61546
   163
        if (state0.status != new_status) {
wenzelm@61546
   164
          current_state.change(_.copy(status = new_status))
wenzelm@52935
   165
          consume_status(new_status)
wenzelm@61548
   166
          if (new_status == Query_Operation.Status.FINISHED)
wenzelm@52877
   167
            remove_overlay()
wenzelm@52877
   168
        }
wenzelm@52876
   169
      }
wenzelm@52865
   170
    }
wenzelm@52865
   171
  }
wenzelm@52865
   172
wenzelm@52877
   173
wenzelm@52931
   174
  /* query operations */
wenzelm@52931
   175
wenzelm@52931
   176
  def cancel_query(): Unit =
wenzelm@66094
   177
    editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }
wenzelm@52877
   178
wenzelm@52865
   179
  def apply_query(query: List[String])
wenzelm@52865
   180
  {
wenzelm@66094
   181
    editor.require_dispatcher {}
wenzelm@52865
   182
wenzelm@52980
   183
    editor.current_node_snapshot(editor_context) match {
wenzelm@52978
   184
      case Some(snapshot) =>
wenzelm@52865
   185
        remove_overlay()
wenzelm@61546
   186
        current_state.change(_ => Query_Operation.State.empty)
wenzelm@52972
   187
        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
wenzelm@66110
   188
wenzelm@66110
   189
        editor.current_command(editor_context, snapshot) match {
wenzelm@66110
   190
          case Some(command) =>
wenzelm@66110
   191
            val state = Query_Operation.State.make(command, query)
wenzelm@66110
   192
            current_state.change(_ => state)
wenzelm@66110
   193
            editor.insert_overlay(command, print_function, state.instance :: query)
wenzelm@66110
   194
          case None =>
wenzelm@52865
   195
        }
wenzelm@66110
   196
wenzelm@61546
   197
        consume_status(current_state.value.status)
wenzelm@52974
   198
        editor.flush()
wenzelm@52865
   199
      case None =>
wenzelm@52865
   200
    }
wenzelm@52865
   201
  }
wenzelm@52865
   202
wenzelm@52865
   203
  def locate_query()
wenzelm@52865
   204
  {
wenzelm@66094
   205
    editor.require_dispatcher {}
wenzelm@52865
   206
wenzelm@61546
   207
    val state = current_state.value
wenzelm@52980
   208
    for {
wenzelm@61546
   209
      command <- state.location
wenzelm@52980
   210
      snapshot = editor.node_snapshot(command.node_name)
wenzelm@64664
   211
      link <- editor.hyperlink_command(true, snapshot, command.id)
wenzelm@52980
   212
    } link.follow(editor_context)
wenzelm@52865
   213
  }
wenzelm@52865
   214
wenzelm@52865
   215
wenzelm@56715
   216
  /* main */
wenzelm@52865
   217
wenzelm@56715
   218
  private val main =
wenzelm@56715
   219
    Session.Consumer[Session.Commands_Changed](getClass.getName) {
wenzelm@56715
   220
      case changed =>
wenzelm@61546
   221
        val state = current_state.value
wenzelm@61546
   222
        state.location match {
wenzelm@56715
   223
          case Some(command)
wenzelm@61546
   224
          if state.update_pending ||
wenzelm@61546
   225
            (state.status != Query_Operation.Status.FINISHED &&
wenzelm@56715
   226
              changed.commands.contains(command)) =>
wenzelm@66094
   227
            editor.send_dispatcher { content_update() }
wenzelm@56715
   228
          case _ =>
wenzelm@56715
   229
        }
wenzelm@52865
   230
    }
wenzelm@52865
   231
wenzelm@53840
   232
  def activate() {
wenzelm@56715
   233
    editor.session.commands_changed += main
wenzelm@53840
   234
  }
wenzelm@53000
   235
wenzelm@53000
   236
  def deactivate() {
wenzelm@56715
   237
    editor.session.commands_changed -= main
wenzelm@53000
   238
    remove_overlay()
wenzelm@61546
   239
    current_state.change(_ => Query_Operation.State.empty)
wenzelm@54327
   240
    consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
wenzelm@61546
   241
    consume_status(Query_Operation.Status.FINISHED)
wenzelm@53000
   242
  }
wenzelm@52865
   243
}