src/Pure/PIDE/query_operation.scala
author wenzelm
Wed Sep 25 11:12:59 2013 +0200 (2013-09-25 ago)
changeset 53872 6e69f9ca8f1c
parent 53844 71f103629327
child 54310 6ddeb83eb67a
permissions -rw-r--r--
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
     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.foreach(command =>
    57       editor.remove_overlay(command, operation_name, instance :: current_query))
    58   }
    59 
    60 
    61   /* content update */
    62 
    63   private def content_update()
    64   {
    65     Swing_Thread.require()
    66 
    67 
    68     /* snapshot */
    69 
    70     val (snapshot, state, removed) =
    71       current_location match {
    72         case Some(cmd) =>
    73           val snapshot = editor.node_snapshot(cmd.node_name)
    74           val state = snapshot.state.command_state(snapshot.version, cmd)
    75           val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
    76           (snapshot, state, removed)
    77         case None =>
    78           (Document.Snapshot.init, Command.empty.init_state, true)
    79       }
    80 
    81     val results =
    82       (for {
    83         (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
    84         if props.contains((Markup.INSTANCE, instance))
    85       } yield elem).toList
    86 
    87 
    88     /* output */
    89 
    90     val new_output =
    91       for {
    92         XML.Elem(_, List(XML.Elem(markup, body))) <- results
    93         if Markup.messages.contains(markup.name)
    94       } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
    95 
    96 
    97     /* status */
    98 
    99     def get_status(name: String, status: Query_Operation.Status.Value)
   100         : Option[Query_Operation.Status.Value] =
   101       results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
   102 
   103     val new_status =
   104       if (removed) Query_Operation.Status.REMOVED
   105       else
   106         get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
   107         get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
   108         Query_Operation.Status.WAITING
   109 
   110     if (new_status == Query_Operation.Status.RUNNING)
   111       results.collectFirst(
   112       {
   113         case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
   114         if elem.name == Markup.RUNNING => id
   115       }).foreach(id => current_exec_id = id)
   116 
   117 
   118     /* state update */
   119 
   120     if (current_output != new_output || current_status != new_status) {
   121       if (snapshot.is_outdated)
   122         current_update_pending = true
   123       else {
   124         current_update_pending = false
   125         if (current_output != new_output && !removed) {
   126           current_output = new_output
   127           consume_output(snapshot, state.results, new_output)
   128         }
   129         if (current_status != new_status) {
   130           current_status = new_status
   131           consume_status(new_status)
   132           if (new_status == Query_Operation.Status.REMOVED) {
   133             remove_overlay()
   134             editor.flush()
   135           }
   136         }
   137       }
   138     }
   139   }
   140 
   141 
   142   /* query operations */
   143 
   144   def cancel_query(): Unit =
   145     Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
   146 
   147   def apply_query(query: List[String])
   148   {
   149     Swing_Thread.require()
   150 
   151     editor.current_node_snapshot(editor_context) match {
   152       case Some(snapshot) =>
   153         remove_overlay()
   154         reset_state()
   155         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   156         editor.current_command(editor_context, snapshot) match {
   157           case Some(command) =>
   158             current_location = Some(command)
   159             current_query = query
   160             current_status = Query_Operation.Status.WAITING
   161             editor.insert_overlay(command, operation_name, instance :: query)
   162           case None =>
   163         }
   164         consume_status(current_status)
   165         editor.flush()
   166       case None =>
   167     }
   168   }
   169 
   170   def locate_query()
   171   {
   172     Swing_Thread.require()
   173 
   174     for {
   175       command <- current_location
   176       snapshot = editor.node_snapshot(command.node_name)
   177       link <- editor.hyperlink_command(snapshot, command)
   178     } link.follow(editor_context)
   179   }
   180 
   181 
   182   /* main actor */
   183 
   184   private val main_actor = actor {
   185     loop {
   186       react {
   187         case changed: Session.Commands_Changed =>
   188           current_location match {
   189             case Some(command)
   190             if current_update_pending ||
   191               (current_status != Query_Operation.Status.REMOVED &&
   192                 changed.commands.contains(command)) =>
   193               Swing_Thread.later { content_update() }
   194             case _ =>
   195           }
   196         case bad =>
   197           java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
   198       }
   199     }
   200   }
   201 
   202   def activate() {
   203     editor.session.commands_changed += main_actor
   204   }
   205 
   206   def deactivate() {
   207     editor.session.commands_changed -= main_actor
   208     remove_overlay()
   209   }
   210 }