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