src/Pure/PIDE/query_operation.scala
author wenzelm
Fri Oct 11 23:12:04 2013 +0200 (2013-10-11 ago)
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;
     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         if (!snapshot.is_outdated) {
   159           editor.current_command(editor_context, snapshot) match {
   160             case Some(command) =>
   161               current_location = Some(command)
   162               current_query = query
   163               current_status = Query_Operation.Status.WAITING
   164               editor.insert_overlay(command, operation_name, instance :: query)
   165             case None =>
   166           }
   167         }
   168         consume_status(current_status)
   169         editor.flush()
   170       case None =>
   171     }
   172   }
   173 
   174   def locate_query()
   175   {
   176     Swing_Thread.require()
   177 
   178     for {
   179       command <- current_location
   180       snapshot = editor.node_snapshot(command.node_name)
   181       link <- editor.hyperlink_command(snapshot, command)
   182     } link.follow(editor_context)
   183   }
   184 
   185 
   186   /* main actor */
   187 
   188   private val main_actor = actor {
   189     loop {
   190       react {
   191         case changed: Session.Commands_Changed =>
   192           current_location match {
   193             case Some(command)
   194             if current_update_pending ||
   195               (current_status != Query_Operation.Status.REMOVED &&
   196                 changed.commands.contains(command)) =>
   197               Swing_Thread.later { content_update() }
   198             case _ =>
   199           }
   200         case bad =>
   201           java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
   202       }
   203     }
   204   }
   205 
   206   def activate() {
   207     editor.session.commands_changed += main_actor
   208   }
   209 
   210   def deactivate() {
   211     editor.session.commands_changed -= main_actor
   212     remove_overlay()
   213     reset_state()
   214     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   215     consume_status(current_status)
   216   }
   217 }