# HG changeset patch
# User wenzelm
# Date 1397925461 -7200
# Node ID 798ba1c2da12cabcd085dd34cc0e9641c325081a
# Parent  5de64a07b0e3173e63b4974da2cbd78d7c516a2f
removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;

diff -r 5de64a07b0e3 -r 798ba1c2da12 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Apr 19 17:33:51 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 19 18:37:41 2014 +0200
@@ -546,10 +546,8 @@
   Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
     if can Toplevel.context_of st then
       let
-        val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
-        val state =
-          if context_arg = "" then proof_state st
-          else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
+        val [limit_arg, allow_dups_arg, query_arg] = args;
+        val state = proof_state st;
         val opt_limit = Int.fromString limit_arg;
         val rem_dups = allow_dups_arg = "false";
         val criteria = read_query Position.none query_arg;
diff -r 5de64a07b0e3 -r 798ba1c2da12 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 19 17:33:51 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 19 18:37:41 2014 +0200
@@ -99,9 +99,9 @@
 
   /* controls */
 
-  private def clicked {
-    find_theorems.apply_query(
-      List(limit.text, allow_dups.selected.toString, context.selection.item.name, query.getText))
+  private def clicked
+  {
+    find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
   }
 
   private val query_label = new Label("Search criteria:") {
@@ -124,19 +124,6 @@
     setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
   }
 
-  private case class Context_Entry(val name: String, val description: String)
-  {
-    override def toString = description
-  }
-
-  private val context_entries =
-    new Context_Entry("", "current context") ::
-      PIDE.resources.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) =>
@@ -159,7 +146,7 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      query_label, Component.wrap(query), context, limit, allow_dups,
+      query_label, Component.wrap(query), limit, allow_dups,
       process_indicator.component, apply_query, zoom)
   add(controls.peer, BorderLayout.NORTH)