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