src/Pure/PIDE/query_operation.scala
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 57612 990ffb84489b
child 60893 3c8b9b4b577c
permissions -rw-r--r--
tuned signature;
     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 object 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 
    21 class Query_Operation[Editor_Context](
    22   editor: Editor[Editor_Context],
    23   editor_context: Editor_Context,
    24   operation_name: String,
    25   consume_status: Query_Operation.Status.Value => Unit,
    26   consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
    27 {
    28   private val instance = Document_ID.make().toString
    29 
    30 
    31   /* implicit state -- owned by GUI thread */
    32 
    33   @volatile private var current_location: Option[Command] = None
    34   @volatile private var current_query: List[String] = Nil
    35   @volatile private var current_update_pending = false
    36   @volatile private var current_output: List[XML.Tree] = Nil
    37   @volatile private var current_status = Query_Operation.Status.FINISHED
    38   @volatile private var current_exec_id = Document_ID.none
    39 
    40   private def reset_state()
    41   {
    42     current_location = None
    43     current_query = Nil
    44     current_update_pending = false
    45     current_output = Nil
    46     current_status = Query_Operation.Status.FINISHED
    47     current_exec_id = Document_ID.none
    48   }
    49 
    50   private def remove_overlay()
    51   {
    52     current_location match {
    53       case None =>
    54       case Some(command) =>
    55         editor.remove_overlay(command, operation_name, instance :: current_query)
    56         editor.flush()
    57     }
    58   }
    59 
    60 
    61   /* content update */
    62 
    63   private def content_update()
    64   {
    65     GUI_Thread.require {}
    66 
    67 
    68     /* snapshot */
    69 
    70     val (snapshot, command_results, removed) =
    71       current_location match {
    72         case Some(cmd) =>
    73           val snapshot = editor.node_snapshot(cmd.node_name)
    74           val command_results = snapshot.state.command_results(snapshot.version, cmd)
    75           val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
    76           (snapshot, command_results, removed)
    77         case None =>
    78           (Document.Snapshot.init, Command.Results.empty, true)
    79       }
    80 
    81     val results =
    82       (for {
    83         (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
    84         if props.contains((Markup.INSTANCE, instance))
    85       } yield elem).toList
    86 
    87 
    88     /* resolve sendback: static command id */
    89 
    90     def resolve_sendback(body: XML.Body): XML.Body =
    91     {
    92       current_location match {
    93         case None => body
    94         case Some(command) =>
    95           def resolve(body: XML.Body): XML.Body =
    96             body map {
    97               case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
    98               case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
    99                 val props1 =
   100                   props.map({
   101                     case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
   102                       (Markup.ID, Properties.Value.Long(command.id))
   103                     case p => p
   104                   })
   105                 XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
   106               case XML.Elem(m, b) => XML.Elem(m, resolve(b))
   107               case t => t
   108             }
   109           resolve(body)
   110       }
   111     }
   112 
   113 
   114     /* output */
   115 
   116     val new_output =
   117       for {
   118         XML.Elem(_, List(XML.Elem(markup, body))) <- results
   119         if Markup.messages.contains(markup.name)
   120         body1 = resolve_sendback(body)
   121       } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
   122 
   123 
   124     /* status */
   125 
   126     def get_status(name: String, status: Query_Operation.Status.Value)
   127         : Option[Query_Operation.Status.Value] =
   128       results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
   129 
   130     val new_status =
   131       if (removed) Query_Operation.Status.FINISHED
   132       else
   133         get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
   134         get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
   135         Query_Operation.Status.WAITING
   136 
   137     if (new_status == Query_Operation.Status.RUNNING)
   138       results.collectFirst(
   139       {
   140         case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
   141         if elem.name == Markup.RUNNING => id
   142       }).foreach(id => current_exec_id = id)
   143 
   144 
   145     /* state update */
   146 
   147     if (current_output != new_output || current_status != new_status) {
   148       if (snapshot.is_outdated)
   149         current_update_pending = true
   150       else {
   151         current_update_pending = false
   152         if (current_output != new_output && !removed) {
   153           current_output = new_output
   154           consume_output(snapshot, command_results, new_output)
   155         }
   156         if (current_status != new_status) {
   157           current_status = new_status
   158           consume_status(new_status)
   159           if (new_status == Query_Operation.Status.FINISHED)
   160             remove_overlay()
   161         }
   162       }
   163     }
   164   }
   165 
   166 
   167   /* query operations */
   168 
   169   def cancel_query(): Unit =
   170     GUI_Thread.require { editor.session.cancel_exec(current_exec_id) }
   171 
   172   def apply_query(query: List[String])
   173   {
   174     GUI_Thread.require {}
   175 
   176     editor.current_node_snapshot(editor_context) match {
   177       case Some(snapshot) =>
   178         remove_overlay()
   179         reset_state()
   180         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   181         if (!snapshot.is_outdated) {
   182           editor.current_command(editor_context, snapshot) match {
   183             case Some(command) =>
   184               current_location = Some(command)
   185               current_query = query
   186               current_status = Query_Operation.Status.WAITING
   187               editor.insert_overlay(command, operation_name, instance :: query)
   188             case None =>
   189           }
   190         }
   191         consume_status(current_status)
   192         editor.flush()
   193       case None =>
   194     }
   195   }
   196 
   197   def locate_query()
   198   {
   199     GUI_Thread.require {}
   200 
   201     for {
   202       command <- current_location
   203       snapshot = editor.node_snapshot(command.node_name)
   204       link <- editor.hyperlink_command(snapshot, command)
   205     } link.follow(editor_context)
   206   }
   207 
   208 
   209   /* main */
   210 
   211   private val main =
   212     Session.Consumer[Session.Commands_Changed](getClass.getName) {
   213       case changed =>
   214         current_location match {
   215           case Some(command)
   216           if current_update_pending ||
   217             (current_status != Query_Operation.Status.FINISHED &&
   218               changed.commands.contains(command)) =>
   219             GUI_Thread.later { content_update() }
   220           case _ =>
   221         }
   222     }
   223 
   224   def activate() {
   225     editor.session.commands_changed += main
   226   }
   227 
   228   def deactivate() {
   229     editor.session.commands_changed -= main
   230     remove_overlay()
   231     reset_state()
   232     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   233     consume_status(current_status)
   234   }
   235 }