# HG changeset patch
# User wenzelm
# Date 1376057868 -7200
# Node ID 07093b66fc9d609973ce94fab0f48208a9c09b60
# Parent  28407b5f1c72726b5854a0a16a81346ec0fc219e
more GUI options;

diff -r 28407b5f1c72 -r 07093b66fc9d src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:49:50 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 16:17:48 2013 +0200
@@ -576,10 +576,13 @@
 (** PIDE query operation **)
 
 val _ =
-  Query_Operation.register "find_theorems" (fn st => fn args =>
+  Query_Operation.register "find_theorems" (fn st => fn [limit_arg, allow_dups_arg, query_arg] =>
     if can Toplevel.context_of st then
-      Pretty.string_of
-        (pretty_theorems (proof_state st) NONE false (maps (read_query Position.none) args))
+      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");
 
 end;
diff -r 28407b5f1c72 -r 07093b66fc9d src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 15:49:50 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 16:17:48 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, Component}
+import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label}
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout
@@ -105,7 +105,11 @@
 
   /* controls */
 
-  private def clicked { find_theorems.apply_query(List(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:")
 
   private val query = new HistoryTextField("isabelle-find-theorems") {
     override def processKeyEvent(evt: KeyEvent)
@@ -117,7 +121,16 @@
     setColumns(40)
   }
 
-  private val query_wrapped = Component.wrap(query)
+  private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
+    tooltip = "Limit of displayed results"
+    verifier = (s: String) =>
+      s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+  }
+
+  private val allow_dups = new CheckBox("Duplicates") {
+    tooltip = "Allow duplicates in result (faster for large theories)"
+    selected = false
+  }
 
   private val apply_query = new Button("Apply") {
     tooltip = "Find theorems meeting specified criteria"
@@ -135,6 +148,7 @@
 
   private val controls =
     new FlowPanel(FlowPanel.Alignment.Right)(
-      query_wrapped, process_indicator.component, apply_query, locate_query, zoom)
+      query_label, Component.wrap(query), limit, allow_dups,
+      process_indicator.component, apply_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }