1/* Title: Pure/PIDE/query_operation.scala 2 Author: Makarius 3 4One-shot query operations via asynchronous print functions and temporary 5document overlays. 6*/ 7 8package isabelle 9 10 11object 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 41class 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} 244