src/Pure/PIDE/query_operation.scala
author wenzelm
Sat Mar 01 22:46:31 2014 +0100 (2014-03-01)
changeset 55828 42ac3cfb89f6
parent 55618 995162143ef4
child 56299 8201790fdeb9
permissions -rw-r--r--
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
     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 match {
    56       case None =>
    57       case Some(command) =>
    58         editor.remove_overlay(command, operation_name, instance :: current_query)
    59         editor.flush()
    60     }
    61   }
    62 
    63 
    64   /* content update */
    65 
    66   private def content_update()
    67   {
    68     Swing_Thread.require()
    69 
    70 
    71     /* snapshot */
    72 
    73     val (snapshot, state, removed) =
    74       current_location match {
    75         case Some(cmd) =>
    76           val snapshot = editor.node_snapshot(cmd.node_name)
    77           val state = snapshot.state.command_state(snapshot.version, cmd)
    78           val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
    79           (snapshot, state, removed)
    80         case None =>
    81           (Document.Snapshot.init, Command.empty.init_state, true)
    82       }
    83 
    84     val results =
    85       (for {
    86         (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
    87         if props.contains((Markup.INSTANCE, instance))
    88       } yield elem).toList
    89 
    90 
    91     /* resolve sendback: static command id */
    92 
    93     def resolve_sendback(body: XML.Body): XML.Body =
    94     {
    95       current_location match {
    96         case None => body
    97         case Some(command) =>
    98           def resolve(body: XML.Body): XML.Body =
    99             body map {
   100               case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
   101               case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
   102                 val props1 =
   103                   props.map({
   104                     case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
   105                       (Markup.ID, Properties.Value.Long(command.id))
   106                     case p => p
   107                   })
   108                 XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
   109               case XML.Elem(m, b) => XML.Elem(m, resolve(b))
   110               case t => t
   111             }
   112           resolve(body)
   113       }
   114     }
   115 
   116 
   117     /* output */
   118 
   119     val new_output =
   120       for {
   121         XML.Elem(_, List(XML.Elem(markup, body))) <- results
   122         if Markup.messages.contains(markup.name)
   123         body1 = resolve_sendback(body)
   124       } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
   125 
   126 
   127     /* status */
   128 
   129     def get_status(name: String, status: Query_Operation.Status.Value)
   130         : Option[Query_Operation.Status.Value] =
   131       results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
   132 
   133     val new_status =
   134       if (removed) Query_Operation.Status.FINISHED
   135       else
   136         get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
   137         get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
   138         Query_Operation.Status.WAITING
   139 
   140     if (new_status == Query_Operation.Status.RUNNING)
   141       results.collectFirst(
   142       {
   143         case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
   144         if elem.name == Markup.RUNNING => id
   145       }).foreach(id => current_exec_id = id)
   146 
   147 
   148     /* state update */
   149 
   150     if (current_output != new_output || current_status != new_status) {
   151       if (snapshot.is_outdated)
   152         current_update_pending = true
   153       else {
   154         current_update_pending = false
   155         if (current_output != new_output && !removed) {
   156           current_output = new_output
   157           consume_output(snapshot, state.results, new_output)
   158         }
   159         if (current_status != new_status) {
   160           current_status = new_status
   161           consume_status(new_status)
   162           if (new_status == Query_Operation.Status.FINISHED)
   163             remove_overlay()
   164         }
   165       }
   166     }
   167   }
   168 
   169 
   170   /* query operations */
   171 
   172   def cancel_query(): Unit =
   173     Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
   174 
   175   def apply_query(query: List[String])
   176   {
   177     Swing_Thread.require()
   178 
   179     editor.current_node_snapshot(editor_context) match {
   180       case Some(snapshot) =>
   181         remove_overlay()
   182         reset_state()
   183         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   184         if (!snapshot.is_outdated) {
   185           editor.current_command(editor_context, snapshot) match {
   186             case Some(command) =>
   187               current_location = Some(command)
   188               current_query = query
   189               current_status = Query_Operation.Status.WAITING
   190               editor.insert_overlay(command, operation_name, instance :: query)
   191             case None =>
   192           }
   193         }
   194         consume_status(current_status)
   195         editor.flush()
   196       case None =>
   197     }
   198   }
   199 
   200   def locate_query()
   201   {
   202     Swing_Thread.require()
   203 
   204     for {
   205       command <- current_location
   206       snapshot = editor.node_snapshot(command.node_name)
   207       link <- editor.hyperlink_command(snapshot, command)
   208     } link.follow(editor_context)
   209   }
   210 
   211 
   212   /* main actor */
   213 
   214   private val main_actor = actor {
   215     loop {
   216       react {
   217         case changed: Session.Commands_Changed =>
   218           current_location match {
   219             case Some(command)
   220             if current_update_pending ||
   221               (current_status != Query_Operation.Status.FINISHED &&
   222                 changed.commands.contains(command)) =>
   223               Swing_Thread.later { content_update() }
   224             case _ =>
   225           }
   226         case bad =>
   227           System.err.println("Query_Operation: ignoring bad message " + bad)
   228       }
   229     }
   230   }
   231 
   232   def activate() {
   233     editor.session.commands_changed += main_actor
   234   }
   235 
   236   def deactivate() {
   237     editor.session.commands_changed -= main_actor
   238     remove_overlay()
   239     reset_state()
   240     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
   241     consume_status(current_status)
   242   }
   243 }