# HG changeset patch
# User wenzelm
# Date 1375452126 -7200
# Node ID e71b5160f242f63235816ce090803745518d2aec
# Parent  9fff9f78240ad8838739f9de7ed2dd20e54f205a
minimal print function "find_theorems", which merely echos its arguments;

diff -r 9fff9f78240a -r e71b5160f242 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 16:00:14 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 16:02:06 2013 +0200
@@ -636,4 +636,16 @@
 
 end;
 
+
+
+(** print function **)
+
+val _ = Command.print_function "find_theorems"
+  (fn {args, ...} =>
+    if null args then NONE
+    else
+      SOME {delay = NONE, pri = 0, persistent = false,
+        print_fn = fn _ => fn st =>
+          writeln (cat_lines ("find_theorems" :: args))});
+
 end;
diff -r 9fff9f78240a -r e71b5160f242 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 16:00:14 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 16:02:06 2013 +0200
@@ -28,11 +28,16 @@
 
   /* component state -- owned by Swing thread */
 
+  private val identification = Document_ID.make().toString
+
   private var zoom_factor = 100
   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 var current_location: Option[Command] = None
+  private var current_query: String = ""
+
+  private val FIND_THEOREMS = "find_theorems"
 
 
   /* pretty text area */
@@ -54,14 +59,35 @@
     Swing_Thread.require()
   }
 
-  private def apply_query(text: String)
+  private def clear_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(identification, current_query))
+
+    current_location = None
+    current_query = ""
+  }
+
+  private def apply_query(query: String)
+  {
+    Swing_Thread.require()
+
+    clear_overlay()
     Document_View(view.getTextArea) match {
       case Some(doc_view) =>
         val snapshot = doc_view.model.snapshot()
-        current_location = snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1)
+        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.add_overlay(command, FIND_THEOREMS, List(identification, query))
+          case None =>
+        }
       case None =>
     }
   }