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