src/Pure/PIDE/query_operation.scala
author wenzelm
Mon Oct 07 12:28:19 2013 +0200 (2013-10-07 ago)
changeset 54310 6ddeb83eb67a
parent 53872 6e69f9ca8f1c
child 54325 2c4155003352
permissions -rw-r--r--
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;
     1 /*  Title:      Pure/PIDE/query_operation.scala
     2     Author:     Makarius
     3 
     4 One-shot query operations via asynchronous print functions and temporary
     5 document overlays.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.actors.Actor._
    12 
    13 
    14 object Query_Operation
    15 {
    16   object Status extends Enumeration
    17   {
    18     val WAITING = Value("waiting")
    19     val RUNNING = Value("running")
    20     val FINISHED = Value("finished")
    21     val REMOVED = Value("removed")
    22   }
    23 }
    24 
    25 class Query_Operation[Editor_Context](
    26   editor: Editor[Editor_Context],
    27   editor_context: Editor_Context,
    28   operation_name: String,
    29   consume_status: Query_Operation.Status.Value => Unit,
    30   consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
    31 {
    32   private val instance = Document_ID.make().toString
    33 
    34 
    35   /* implicit state -- owned by Swing thread */
    36 
    37   private var current_location: Option[Command] = None
    38   private var current_query: List[String] = Nil
    39   private var current_update_pending = false
    40   private var current_output: List[XML.Tree] = Nil
    41   private var current_status = Query_Operation.Status.REMOVED
    42   private var current_exec_id = Document_ID.none
    43 
    44   private def reset_state()
    45   {
    46     current_location = None
    47     current_query = Nil
    48     current_update_pending = false
    49     current_output = Nil
    50     current_status = Query_Operation.Status.REMOVED
    51     current_exec_id = Document_ID.none
    52   }
    53 
    54   private def remove_overlay()
    55   {
    56     current_location match {
    57       case None =>
    58       case Some(command) =>
    59         editor.remove_overlay(command, operation_name, instance :: current_query)
    60         editor.flush()
    61     }
    62   }
    63 
    64 
    65   /* content update */
    66 
    67   private def content_update()
    68   {
    69     Swing_Thread.require()
    70 
    71 
    72     /* snapshot */
    73 
    74     val (snapshot, state, removed) =
    75       current_location match {
    76         case Some(cmd) =>
    77           val snapshot = editor.node_snapshot(cmd.node_name)
    78           val state = snapshot.state.command_state(snapshot.version, cmd)
    79           val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
    80           (snapshot, state, removed)
    81         case None =>
    82           (Document.Snapshot.init, Command.empty.init_state, true)
    83       }
    84 
    85     val results =
    86       (for {
    87         (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
    88         if props.contains((Markup.INSTANCE, instance))
    89       } yield elem).toList
    90 
    91 
    92     /* output */
    93 
    94     val new_output =
    95       for {
    96         XML.Elem(_, List(XML.Elem(markup, body))) <- results
    97         if Markup.messages.contains(markup.name)
    98       } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
    99 
   100 
   101     /* status */
   102 
   103     def get_status(name: String, status: Query_Operation.Status.Value)
   104         : Option[Query_Operation.Status.Value] =
   105       results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
   106 
   107     val new_status =
   108       if (removed) Query_Operation.Status.REMOVED
   109       else
   110         get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
   111         get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
   112         Query_Operation.Status.WAITING
   113 
   114     if (new_status == Query_Operation.Status.RUNNING)
   115       results.collectFirst(
   116       {
   117         case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
   118         if elem.name == Markup.RUNNING => id
   119       }).foreach(id => current_exec_id = id)
   120 
   121 
   122     /* state update */
   123 
   124     if (current_output != new_output || current_status != new_status) {
   125       if (snapshot.is_outdated)
   126         current_update_pending = true
   127       else {
   128         current_update_pending = false
   129         if (current_output != new_output && !removed) {
   130           current_output = new_output
   131           consume_output(snapshot, state.results, new_output)
   132         }
   133         if (current_status != new_status) {
   134           current_status = new_status
   135           consume_status(new_status)
   136           if (new_status == Query_Operation.Status.REMOVED)
   137             remove_overlay()
   138         }
   139       }
   140     }
   141   }
   142 
   143 
   144   /* query operations */
   145 
   146   def cancel_query(): Unit =
   147     Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
   148 
   149   def apply_query(query: List[String])
   150   {
   151     Swing_Thread.require()
   152 
   153     editor.current_node_snapshot(editor_context) match {
   154       case Some(snapshot) =>
   155         remove_overlay()
   156         reset_state()
   157         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   158         editor.current_command(editor_context, snapshot) match {
   159           case Some(command) =>
   160             current_location = Some(command)
   161             current_query = query
   162             current_status = Query_Operation.Status.WAITING
   163             editor.insert_overlay(command, operation_name, instance :: query)
   164           case None =>
   165         }
   166         consume_status(current_status)
   167         editor.flush()
   168       case None =>
   169     }
   170   }
   171 
   172   def locate_query()
   173   {
   174     Swing_Thread.require()
   175 
   176     for {
   177       command <- current_location
   178       snapshot = editor.node_snapshot(command.node_name)
   179       link <- editor.hyperlink_command(snapshot, command)
   180     } link.follow(editor_context)
   181   }
   182 
   183 
   184   /* main actor */
   185 
   186   private val main_actor = actor {
   187     loop {
   188       react {
   189         case changed: Session.Commands_Changed =>
   190           current_location match {
   191             case Some(command)
   192             if current_update_pending ||
   193               (current_status != Query_Operation.Status.REMOVED &&
   194                 changed.commands.contains(command)) =>
   195               Swing_Thread.later { content_update() }
   196             case _ =>
   197           }
   198         case bad =>
   199           java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
   200       }
   201     }
   202   }
   203 
   204   def activate() {
   205     editor.session.commands_changed += main_actor
   206   }
   207 
   208   def deactivate() {
   209     editor.session.commands_changed -= main_actor
   210     remove_overlay()
   211   }
   212 }