# HG changeset patch
# User wenzelm
# Date 1398541771 -7200
# Node ID d203b9c400a219de209ba87ea83b6dd7a3cd47af
# Parent  d6fdf08282f39d9e3d84c3fd5a25587e84c24892
PIDE support for find_consts;

diff -r d6fdf08282f3 -r d203b9c400a2 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat Apr 26 21:16:50 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML	Sat Apr 26 21:49:31 2014 +0200
@@ -11,6 +11,7 @@
       Strict of string
     | Loose of string
     | Name of string
+  val read_query: Position.T -> string -> (bool * criterion) list
   val find_consts : Proof.context -> (bool * criterion) list -> unit
 end;
 
@@ -69,7 +70,7 @@
 
 (* find_consts *)
 
-fun find_consts ctxt raw_criteria =
+fun pretty_consts ctxt raw_criteria =
   let
     val thy = Proof_Context.theory_of ctxt;
     val low_ranking = 10000;
@@ -120,7 +121,9 @@
       else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
     Pretty.str "" ::
     map (pretty_const ctxt) matches
-  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
+  end |> Pretty.fbreaks |> curry Pretty.blk 0;
+
+fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
 
 
 (* command syntax *)
@@ -132,15 +135,37 @@
   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   Parse.xname >> Loose;
 
+val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
+
 in
 
+fun read_query pos str =
+  Outer_Syntax.scan pos str
+  |> filter Token.is_proper
+  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
+  |> #1;
+
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_consts"}
-    "find constants by name/type patterns"
-    (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
-      >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
+    "find constants by name / type patterns"
+    (query >> (fn spec =>
+      Toplevel.keep (fn st =>
+        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
 
 end;
 
+
+(* PIDE query operation *)
+
+val _ =
+  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
+    (case try Toplevel.context_of state of
+      SOME ctxt =>
+        let
+          val [query_arg] = args;
+          val query = read_query Position.none query_arg;
+        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
+    | NONE => error "Unknown context"));
+
 end;
 
diff -r d6fdf08282f3 -r d203b9c400a2 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 21:16:50 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 21:49:31 2014 +0200
@@ -21,11 +21,11 @@
 
 object Find_Dockable
 {
-  private abstract class Operation
+  private abstract class Operation(view: View)
   {
+    val pretty_text_area = new Pretty_Text_Area(view)
     def query_operation: Query_Operation[View]
     def query: JComponent
-    def pretty_text_area: Pretty_Text_Area
     def page: TabbedPane.Page
   }
 }
@@ -75,11 +75,8 @@
 
   /* find theorems */
 
-  private val find_theorems = new Find_Dockable.Operation
+  private val find_theorems = new Find_Dockable.Operation(view)
   {
-    val pretty_text_area = new Pretty_Text_Area(view)
-
-
     /* query */
 
     private val process_indicator = new Process_Indicator
@@ -104,7 +101,7 @@
     val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
 
 
-    /* controls */
+    /* GUI page */
 
     private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
       tooltip = "Limit of displayed results"
@@ -124,9 +121,6 @@
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-
-    /* GUI page */
-
     private val controls: List[Component] =
       List(query_label, Component.wrap(query), limit, allow_dups,
         process_indicator.component, apply_button, zoom)
@@ -139,9 +133,53 @@
   }
 
 
+  /* find consts */
+
+  private val find_consts = new Find_Dockable.Operation(view)
+  {
+    /* query */
+
+    private val process_indicator = new Process_Indicator
+
+    val query_operation =
+      new Query_Operation(PIDE.editor, view, "find_consts",
+        consume_status(process_indicator, _),
+        (snapshot, results, body) =>
+          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+    private def apply_query()
+    {
+      query_operation.apply_query(List(query.getText))
+    }
+
+    private val query_label = new Label("Search criteria:") {
+      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
+    }
+
+    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
+
+
+    /* GUI page */
+
+    private val apply_button = new Button("Apply") {
+      tooltip = "Find constants by name / type patterns"
+      reactions += { case ButtonClicked(_) => apply_query() }
+    }
+
+    private val controls: List[Component] =
+      List(query_label, Component.wrap(query), process_indicator.component, apply_button, zoom)
+
+    val page =
+      new TabbedPane.Page("Constants", new BorderPanel {
+        add(new Wrap_Panel(Wrap_Panel.Alignment.Right)(controls:_*), BorderPanel.Position.North)
+        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+      }, apply_button.tooltip)
+  }
+
+
   /* operations */
 
-  private val operations = List(find_theorems)
+  private val operations = List(find_theorems, find_consts)
 
   private val tabs = new TabbedPane { for (op <- operations) pages += op.page }
   set_content(tabs)