# HG changeset patch
# User wenzelm
# Date 1375715642 -7200
# Node ID 02a7e7180ee57f2bd391dbb060bcad6eb2f7418b
# Parent  c2da0d3b974dfeaff05997d8211fe1bf4309a5c2
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;

diff -r c2da0d3b974d -r 02a7e7180ee5 src/Pure/PIDE/query_operation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/query_operation.ML	Mon Aug 05 17:14:02 2013 +0200
@@ -0,0 +1,30 @@
+(*  Title:      Pure/PIDE/query_operation.ML
+    Author:     Makarius
+
+One-shot query operations via asynchronous print functions and temporary
+document overlay.
+*)
+
+signature QUERY_OPERATION =
+sig
+  val register: string -> (Toplevel.state -> string list -> string) -> unit
+end;
+
+structure Query_Operation: QUERY_OPERATION =
+struct
+
+fun register name f =
+  Command.print_function name
+    (fn {args = instance :: args, ...} =>
+        SOME {delay = NONE, pri = 0, persistent = false,
+          print_fn = fn _ => fn state =>
+            let
+              val msg = XML.Elem ((Markup.writelnN, []), [XML.Text (f state args)])
+                handle exn =>
+                  if Exn.is_interrupt exn then reraise exn
+                  else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
+            in Output.result [(Markup.instanceN, instance)] (YXML.string_of msg) end}
+      | _ => NONE);
+
+end;
+
diff -r c2da0d3b974d -r 02a7e7180ee5 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Aug 05 16:12:03 2013 +0200
+++ b/src/Pure/ROOT	Mon Aug 05 17:14:02 2013 +0200
@@ -158,6 +158,7 @@
     "PIDE/execution.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
+    "PIDE/query_operation.ML"
     "PIDE/xml.ML"
     "PIDE/yxml.ML"
     "Proof/extraction.ML"
diff -r c2da0d3b974d -r 02a7e7180ee5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 05 16:12:03 2013 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 05 17:14:02 2013 +0200
@@ -269,6 +269,7 @@
 use "Thy/present.ML";
 use "PIDE/execution.ML";
 use "PIDE/command.ML";
+use "PIDE/query_operation.ML";
 use "Thy/thy_load.ML";
 use "Thy/thy_info.ML";
 use "PIDE/document.ML";
diff -r c2da0d3b974d -r 02a7e7180ee5 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Aug 05 16:12:03 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 05 17:14:02 2013 +0200
@@ -605,7 +605,7 @@
 
 
 
-(** command syntax **)
+(** Isar command syntax **)
 
 local
 
@@ -647,28 +647,10 @@
 
 
 
-(** print function **)
-
-val find_theoremsN = "find_theorems";
+(** PIDE query operation **)
 
-val _ = Command.print_function find_theoremsN
-  (fn {args, ...} =>
-    (case args of
-      [instance, query] =>
-      SOME {delay = NONE, pri = 0, persistent = false,
-        print_fn = fn _ => fn state =>
-          let
-            val msg =
-              XML.Elem ((Markup.writelnN, []),
-                [XML.Text
-                  (Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query)))])
-              handle exn =>
-                if Exn.is_interrupt exn then reraise exn
-                else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
-          in
-            Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)]
-              (YXML.string_of msg)
-          end}
-    | _ => NONE));
+val _ =
+  Query_Operation.register "find_theorems" (fn state => fn query =>
+    Pretty.string_of (pretty_theorems_cmd state NONE false (maps parse_query query)));
 
 end;
diff -r c2da0d3b974d -r 02a7e7180ee5 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 05 16:12:03 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 05 17:14:02 2013 +0200
@@ -35,6 +35,7 @@
   "src/pretty_text_area.scala"
   "src/pretty_tooltip.scala"
   "src/protocol_dockable.scala"
+  "src/query_operation.scala"
   "src/raw_output_dockable.scala"
   "src/readme_dockable.scala"
   "src/rendering.scala"
diff -r c2da0d3b974d -r 02a7e7180ee5 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 16:12:03 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 17:14:02 2013 +0200
@@ -25,27 +25,22 @@
 {
   Swing_Thread.require()
 
-
-  /* component state -- owned by Swing thread */
-
-  private val FIND_THEOREMS = "find_theorems"
-  private val instance = Document_ID.make().toString
-
-  private var zoom_factor = 100
-  private var current_location: Option[Command] = None
-  private var current_query: String = ""
-  private var current_result = false
-  private var current_snapshot = Document.State.init.snapshot()
-  private var current_state = Command.empty.init_state
-  private var current_output: List[XML.Tree] = Nil
-
-
-  /* pretty text area */
-
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
 
+  /* query operation */
+
+  private val find_theorems =
+    Query_Operation(view, "find_theorems",
+      (snapshot, results, body) =>
+        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+
+  /* resize */
+
+  private var zoom_factor = 100
+
   private def handle_resize()
   {
     Swing_Thread.require()
@@ -54,98 +49,12 @@
       (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
   }
 
-  private def remove_overlay()
-  {
-    Swing_Thread.require()
-
-    for {
-      command <- current_location
-      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
-      model <- PIDE.document_model(buffer)
-    } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query))
-  }
-
-  private def handle_update()
-  {
-    Swing_Thread.require()
-
-    val (new_snapshot, new_state) =
-      Document_View(view.getTextArea) match {
-        case Some(doc_view) =>
-          val snapshot = doc_view.model.snapshot()
-          if (!snapshot.is_outdated) {
-            current_location match {
-              case Some(cmd) =>
-                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
-              case None =>
-                (Document.State.init.snapshot(), Command.empty.init_state)
-            }
-          }
-          else (current_snapshot, current_state)
-        case None => (current_snapshot, current_state)
-      }
-
-    val new_output =
-      (for {
-        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
-          new_state.results.entries
-        if props.contains((Markup.KIND, FIND_THEOREMS))
-        if props.contains((Markup.INSTANCE, instance))
-      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
-
-    if (new_output != current_output)
-      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
+  private val delay_resize =
+    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
 
-    if (!new_output.isEmpty) {
-      current_result = true
-      remove_overlay()
-      PIDE.flush_buffers()
-    }
-
-    current_snapshot = new_snapshot
-    current_state = new_state
-    current_output = new_output
-  }
-
-  private def apply_query(query: String)
-  {
-    Swing_Thread.require()
-
-    Document_View(view.getTextArea) match {
-      case Some(doc_view) =>
-        val snapshot = doc_view.model.snapshot()
-        remove_overlay()
-        current_location = None
-        current_query = ""
-        current_result = false
-        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
-          case Some(command) =>
-            current_location = Some(command)
-            current_query = query
-            doc_view.model.insert_overlay(command, FIND_THEOREMS, List(instance, query))
-          case None =>
-        }
-        PIDE.flush_buffers()
-      case None =>
-    }
-  }
-
-  private def locate_query()
-  {
-    Swing_Thread.require()
-
-    current_location match {
-      case Some(command) =>
-        val snapshot = PIDE.session.snapshot(command.node_name)
-        val commands = snapshot.node.commands
-        if (commands.contains(command)) {
-          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
-          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-          Hyperlink(command.node_name.node, line, column).follow(view)
-        }
-      case None =>
-    }
-  }
+  addComponentListener(new ComponentAdapter {
+    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+  })
 
 
   /* main actor */
@@ -155,12 +64,6 @@
       react {
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
-        case changed: Session.Commands_Changed =>
-          current_location match {
-            case Some(command) if !current_result && changed.commands.contains(command) =>
-              Swing_Thread.later { handle_update() }
-            case _ =>
-          }
         case bad =>
           java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
       }
@@ -172,30 +75,20 @@
     Swing_Thread.require()
 
     PIDE.session.global_options += main_actor
-    PIDE.session.commands_changed += main_actor
     handle_resize()
+    find_theorems.activate()
   }
 
   override def exit()
   {
     Swing_Thread.require()
 
+    find_theorems.deactivate()
     PIDE.session.global_options -= main_actor
-    PIDE.session.commands_changed -= main_actor
     delay_resize.revoke()
   }
 
 
-  /* resize */
-
-  private val delay_resize =
-    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-  })
-
-
   /* controls */
 
   private val query = new HistoryTextArea("isabelle-find-theorems") {
@@ -208,12 +101,12 @@
 
   private val find = new Button("Find") {
     tooltip = "Find theorems meeting specified criteria"
-    reactions += { case ButtonClicked(_) => apply_query(query.getText) }
+    reactions += { case ButtonClicked(_) => find_theorems.apply_query(List(query.getText)) }
   }
 
   private val locate = new Button("Locate") {
     tooltip = "Locate context of current query within source text"
-    reactions += { case ButtonClicked(_) => locate_query() }
+    reactions += { case ButtonClicked(_) => find_theorems.locate_query() }
   }
 
   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
diff -r c2da0d3b974d -r 02a7e7180ee5 src/Tools/jEdit/src/query_operation.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 05 17:14:02 2013 +0200
@@ -0,0 +1,153 @@
+/*  Title:      Tools/jEdit/src/query_operation.scala
+    Author:     Makarius
+
+One-shot query operations via asynchronous print functions and temporary
+document overlay.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import org.gjt.sp.jedit.View
+
+
+object Query_Operation
+{
+  def apply(
+      view: View,
+      name: String,
+      consume: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
+    new Query_Operation(view, name, consume)
+}
+
+final class Query_Operation private(
+  view: View,
+  operation_name: String,
+  consume_result: (Document.Snapshot, Command.Results, XML.Body) => Unit)
+{
+  private val instance = Document_ID.make().toString
+
+
+  /* implicit state -- owned by Swing thread */
+
+  private var current_location: Option[Command] = None
+  private var current_query: List[String] = Nil
+  private var current_result = false
+  private var current_snapshot = Document.State.init.snapshot()
+  private var current_state = Command.empty.init_state
+  private var current_output: List[XML.Tree] = Nil
+
+  private def remove_overlay()
+  {
+    Swing_Thread.require()
+
+    for {
+      command <- current_location
+      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
+      model <- PIDE.document_model(buffer)
+    } model.remove_overlay(command, operation_name, instance :: current_query)
+  }
+
+  private def handle_result()
+  {
+    Swing_Thread.require()
+
+    val (new_snapshot, new_state) =
+      Document_View(view.getTextArea) match {
+        case Some(doc_view) =>
+          val snapshot = doc_view.model.snapshot()
+          current_location match {
+            case Some(cmd) =>
+              (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+            case None =>
+              (Document.State.init.snapshot(), Command.empty.init_state)
+          }
+        case None => (current_snapshot, current_state)
+      }
+
+    val new_output =
+      (for {
+        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
+          new_state.results.entries
+        if props.contains((Markup.INSTANCE, instance))
+      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
+
+    if (new_output != current_output)
+      consume_result(new_snapshot, new_state.results, new_output)
+
+    if (!new_output.isEmpty) {
+      current_result = true
+      remove_overlay()
+      PIDE.flush_buffers()
+    }
+
+    current_snapshot = new_snapshot
+    current_state = new_state
+    current_output = new_output
+  }
+
+  def apply_query(query: List[String])
+  {
+    Swing_Thread.require()
+
+    Document_View(view.getTextArea) match {
+      case Some(doc_view) =>
+        val snapshot = doc_view.model.snapshot()
+        remove_overlay()
+        current_location = None
+        current_query = Nil
+        current_result = false
+        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
+          case Some(command) =>
+            current_location = Some(command)
+            current_query = query
+            doc_view.model.insert_overlay(command, operation_name, instance :: query)
+          case None =>
+        }
+        PIDE.flush_buffers()
+      case None =>
+    }
+  }
+
+  def locate_query()
+  {
+    Swing_Thread.require()
+
+    current_location match {
+      case Some(command) =>
+        val snapshot = PIDE.session.snapshot(command.node_name)
+        val commands = snapshot.node.commands
+        if (commands.contains(command)) {
+          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
+          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+          Hyperlink(command.node_name.node, line, column).follow(view)
+        }
+      case None =>
+    }
+  }
+
+
+  /* main actor */
+
+  private val main_actor = actor {
+    loop {
+      react {
+        case changed: Session.Commands_Changed =>
+          current_location match {
+            case Some(command) if !current_result && changed.commands.contains(command) =>
+              Swing_Thread.later { handle_result() }
+            case _ =>
+          }
+        case bad =>
+          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  def activate() { PIDE.session.commands_changed += main_actor }
+  def deactivate() { PIDE.session.commands_changed -= main_actor }
+}