# HG changeset patch
# User wenzelm
# Date 1376061947 -7200
# Node ID 14ddcc0ad7df012aadbd178746e5af347303072b
# Parent  07093b66fc9d609973ce94fab0f48208a9c09b60
enable search in pre-loaded theory;

diff -r 07093b66fc9d -r 14ddcc0ad7df src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 16:17:48 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 17:25:47 2013 +0200
@@ -576,13 +576,17 @@
 (** PIDE query operation **)
 
 val _ =
-  Query_Operation.register "find_theorems" (fn st => fn [limit_arg, allow_dups_arg, query_arg] =>
-    if can Toplevel.context_of st then
-      let
-        val opt_limit = Int.fromString limit_arg;
-        val rem_dups = allow_dups_arg = "false";
-        val criteria = read_query Position.none query_arg;
-      in Pretty.string_of (pretty_theorems (proof_state st) opt_limit rem_dups criteria) end
-    else error "Unknown context");
+  Query_Operation.register "find_theorems"
+    (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
+      if can Toplevel.context_of st then
+        let
+          val state =
+            if context_arg = "" then proof_state st
+            else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
+          val opt_limit = Int.fromString limit_arg;
+          val rem_dups = allow_dups_arg = "false";
+          val criteria = read_query Position.none query_arg;
+        in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
+      else error "Unknown context");
 
 end;
diff -r 07093b66fc9d -r 14ddcc0ad7df src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 16:17:48 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 17:25:47 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label}
+import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout
@@ -106,7 +106,8 @@
   /* controls */
 
   private def clicked {
-    find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
+    find_theorems.apply_query(
+      List(limit.text, allow_dups.selected.toString, context.selection.item.name, query.getText))
   }
 
   private val query_label = new Label("Search criteria:")
@@ -121,6 +122,19 @@
     setColumns(40)
   }
 
+  private case class Context_Entry(val name: String, val description: String)
+  {
+    override def toString = description
+  }
+
+  private val context_entries =
+    new Context_Entry("", "context") ::
+      PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
+
+  private val context = new ComboBox[Context_Entry](context_entries) {
+    tooltip = "Search in pre-loaded theory (default: context of current command)"
+  }
+
   private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
     tooltip = "Limit of displayed results"
     verifier = (s: String) =>
@@ -148,7 +162,7 @@
 
   private val controls =
     new FlowPanel(FlowPanel.Alignment.Right)(
-      query_label, Component.wrap(query), limit, allow_dups,
+      query_label, Component.wrap(query), context, limit, allow_dups,
       process_indicator.component, apply_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }