src/Pure/PIDE/query_operation.scala
author wenzelm
Fri, 11 Oct 2013 23:12:04 +0200
changeset 54327 148903e47b26
parent 54325 2c4155003352
child 54640 bbd2fa353809
permissions -rw-r--r--
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52981
c7afd884dfb2 moved generic module to its proper place;
wenzelm
parents: 52980
diff changeset
     1
/*  Title:      Pure/PIDE/query_operation.scala
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
     3
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
     4
One-shot query operations via asynchronous print functions and temporary
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
     5
document overlays.
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
     6
*/
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
     7
52981
c7afd884dfb2 moved generic module to its proper place;
wenzelm
parents: 52980
diff changeset
     8
package isabelle
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
     9
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    10
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    11
import scala.actors.Actor._
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    12
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    13
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    14
object Query_Operation
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    15
{
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    16
  object Status extends Enumeration
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    17
  {
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    18
    val WAITING = Value("waiting")
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    19
    val RUNNING = Value("running")
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    20
    val FINISHED = Value("finished")
53872
6e69f9ca8f1c explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents: 53844
diff changeset
    21
    val REMOVED = Value("removed")
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    22
  }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    23
}
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    24
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    25
class Query_Operation[Editor_Context](
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    26
  editor: Editor[Editor_Context],
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    27
  editor_context: Editor_Context,
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    28
  operation_name: String,
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
    29
  consume_status: Query_Operation.Status.Value => Unit,
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
    30
  consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    31
{
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    32
  private val instance = Document_ID.make().toString
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    33
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    34
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
    35
  /* implicit state -- owned by Swing thread */
52874
91032244e4ca query process animation;
wenzelm
parents: 52865
diff changeset
    36
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    37
  private var current_location: Option[Command] = None
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    38
  private var current_query: List[String] = Nil
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    39
  private var current_update_pending = false
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    40
  private var current_output: List[XML.Tree] = Nil
53872
6e69f9ca8f1c explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents: 53844
diff changeset
    41
  private var current_status = Query_Operation.Status.REMOVED
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
    42
  private var current_exec_id = Document_ID.none
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    43
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    44
  private def reset_state()
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    45
  {
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    46
    current_location = None
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    47
    current_query = Nil
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    48
    current_update_pending = false
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    49
    current_output = Nil
53872
6e69f9ca8f1c explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents: 53844
diff changeset
    50
    current_status = Query_Operation.Status.REMOVED
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
    51
    current_exec_id = Document_ID.none
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    52
  }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    53
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    54
  private def remove_overlay()
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    55
  {
54310
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
    56
    current_location match {
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
    57
      case None =>
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
    58
      case Some(command) =>
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
    59
        editor.remove_overlay(command, operation_name, instance :: current_query)
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
    60
        editor.flush()
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
    61
    }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    62
  }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    63
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
    64
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
    65
  /* content update */
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
    66
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
    67
  private def content_update()
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    68
  {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    69
    Swing_Thread.require()
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    70
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    71
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    72
    /* snapshot */
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    73
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
    74
    val (snapshot, state, removed) =
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    75
      current_location match {
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    76
        case Some(cmd) =>
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52972
diff changeset
    77
          val snapshot = editor.node_snapshot(cmd.node_name)
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    78
          val state = snapshot.state.command_state(snapshot.version, cmd)
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
    79
          val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
    80
          (snapshot, state, removed)
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    81
        case None =>
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52971
diff changeset
    82
          (Document.Snapshot.init, Command.empty.init_state, true)
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    83
      }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    84
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    85
    val results =
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    86
      (for {
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
    87
        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    88
        if props.contains((Markup.INSTANCE, instance))
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
    89
      } yield elem).toList
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    90
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    91
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    92
    /* output */
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    93
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
    94
    val new_output =
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    95
      for {
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
    96
        XML.Elem(_, List(XML.Elem(markup, body))) <- results
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    97
        if Markup.messages.contains(markup.name)
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
    98
      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
    99
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   100
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   101
    /* status */
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   102
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   103
    def get_status(name: String, status: Query_Operation.Status.Value)
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   104
        : Option[Query_Operation.Status.Value] =
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   105
      results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   106
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   107
    val new_status =
53872
6e69f9ca8f1c explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents: 53844
diff changeset
   108
      if (removed) Query_Operation.Status.REMOVED
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
   109
      else
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   110
        get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   111
        get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   112
        Query_Operation.Status.WAITING
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   113
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   114
    if (new_status == Query_Operation.Status.RUNNING)
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   115
      results.collectFirst(
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   116
      {
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   117
        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   118
        if elem.name == Markup.RUNNING => id
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   119
      }).foreach(id => current_exec_id = id)
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   120
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   121
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   122
    /* state update */
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   123
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   124
    if (current_output != new_output || current_status != new_status) {
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   125
      if (snapshot.is_outdated)
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   126
        current_update_pending = true
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   127
      else {
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   128
        current_update_pending = false
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
   129
        if (current_output != new_output && !removed) {
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   130
          current_output = new_output
52932
eb7d7c0034b5 removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents: 52931
diff changeset
   131
          consume_output(snapshot, state.results, new_output)
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   132
        }
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   133
        if (current_status != new_status) {
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   134
          current_status = new_status
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   135
          consume_status(new_status)
54310
6ddeb83eb67a clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents: 53872
diff changeset
   136
          if (new_status == Query_Operation.Status.REMOVED)
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   137
            remove_overlay()
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   138
        }
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   139
      }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   140
    }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   141
  }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   142
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   143
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   144
  /* query operations */
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   145
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52890
diff changeset
   146
  def cancel_query(): Unit =
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents: 52935
diff changeset
   147
    Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   148
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   149
  def apply_query(query: List[String])
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   150
  {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   151
    Swing_Thread.require()
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   152
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   153
    editor.current_node_snapshot(editor_context) match {
52978
37fbb3fde380 prefer PIDE editor operations;
wenzelm
parents: 52977
diff changeset
   154
      case Some(snapshot) =>
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   155
        remove_overlay()
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   156
        reset_state()
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52971
diff changeset
   157
        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
54325
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   158
        if (!snapshot.is_outdated) {
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   159
          editor.current_command(editor_context, snapshot) match {
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   160
            case Some(command) =>
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   161
              current_location = Some(command)
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   162
              current_query = query
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   163
              current_status = Query_Operation.Status.WAITING
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   164
              editor.insert_overlay(command, operation_name, instance :: query)
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   165
            case None =>
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 54310
diff changeset
   166
          }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   167
        }
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   168
        consume_status(current_status)
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52972
diff changeset
   169
        editor.flush()
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   170
      case None =>
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   171
    }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   172
  }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   173
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   174
  def locate_query()
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   175
  {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   176
    Swing_Thread.require()
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   177
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   178
    for {
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   179
      command <- current_location
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   180
      snapshot = editor.node_snapshot(command.node_name)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   181
      link <- editor.hyperlink_command(snapshot, command)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   182
    } link.follow(editor_context)
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   183
  }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   184
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   185
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   186
  /* main actor */
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   187
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   188
  private val main_actor = actor {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   189
    loop {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   190
      react {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   191
        case changed: Session.Commands_Changed =>
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   192
          current_location match {
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   193
            case Some(command)
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52875
diff changeset
   194
            if current_update_pending ||
53872
6e69f9ca8f1c explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents: 53844
diff changeset
   195
              (current_status != Query_Operation.Status.REMOVED &&
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52934
diff changeset
   196
                changed.commands.contains(command)) =>
52877
9a26ec5739dd tuned -- more explicit type Status.Value;
wenzelm
parents: 52876
diff changeset
   197
              Swing_Thread.later { content_update() }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   198
            case _ =>
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   199
          }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   200
        case bad =>
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   201
          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   202
      }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   203
    }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   204
  }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   205
53840
wenzelm
parents: 53000
diff changeset
   206
  def activate() {
wenzelm
parents: 53000
diff changeset
   207
    editor.session.commands_changed += main_actor
wenzelm
parents: 53000
diff changeset
   208
  }
53000
50d06647cf24 more cleanup;
wenzelm
parents: 52981
diff changeset
   209
50d06647cf24 more cleanup;
wenzelm
parents: 52981
diff changeset
   210
  def deactivate() {
50d06647cf24 more cleanup;
wenzelm
parents: 52981
diff changeset
   211
    editor.session.commands_changed -= main_actor
50d06647cf24 more cleanup;
wenzelm
parents: 52981
diff changeset
   212
    remove_overlay()
54327
148903e47b26 more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
wenzelm
parents: 54325
diff changeset
   213
    reset_state()
148903e47b26 more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
wenzelm
parents: 54325
diff changeset
   214
    consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
148903e47b26 more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
wenzelm
parents: 54325
diff changeset
   215
    consume_status(current_status)
53000
50d06647cf24 more cleanup;
wenzelm
parents: 52981
diff changeset
   216
  }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff changeset
   217
}