PIDE support for find_consts;
authorwenzelm
Sat Apr 26 21:49:31 2014 +0200 (2014-04-26)
changeset 56758d203b9c400a2
parent 56757 d6fdf08282f3
child 56759 790f7562cd0e
PIDE support for find_consts;
src/Pure/Tools/find_consts.ML
src/Tools/jEdit/src/find_dockable.scala
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sat Apr 26 21:16:50 2014 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Apr 26 21:49:31 2014 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4        Strict of string
     1.5      | Loose of string
     1.6      | Name of string
     1.7 +  val read_query: Position.T -> string -> (bool * criterion) list
     1.8    val find_consts : Proof.context -> (bool * criterion) list -> unit
     1.9  end;
    1.10  
    1.11 @@ -69,7 +70,7 @@
    1.12  
    1.13  (* find_consts *)
    1.14  
    1.15 -fun find_consts ctxt raw_criteria =
    1.16 +fun pretty_consts ctxt raw_criteria =
    1.17    let
    1.18      val thy = Proof_Context.theory_of ctxt;
    1.19      val low_ranking = 10000;
    1.20 @@ -120,7 +121,9 @@
    1.21        else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
    1.22      Pretty.str "" ::
    1.23      map (pretty_const ctxt) matches
    1.24 -  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
    1.25 +  end |> Pretty.fbreaks |> curry Pretty.blk 0;
    1.26 +
    1.27 +fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
    1.28  
    1.29  
    1.30  (* command syntax *)
    1.31 @@ -132,15 +135,37 @@
    1.32    Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
    1.33    Parse.xname >> Loose;
    1.34  
    1.35 +val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    1.36 +
    1.37  in
    1.38  
    1.39 +fun read_query pos str =
    1.40 +  Outer_Syntax.scan pos str
    1.41 +  |> filter Token.is_proper
    1.42 +  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    1.43 +  |> #1;
    1.44 +
    1.45  val _ =
    1.46    Outer_Syntax.improper_command @{command_spec "find_consts"}
    1.47 -    "find constants by name/type patterns"
    1.48 -    (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
    1.49 -      >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    1.50 +    "find constants by name / type patterns"
    1.51 +    (query >> (fn spec =>
    1.52 +      Toplevel.keep (fn st =>
    1.53 +        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
    1.54  
    1.55  end;
    1.56  
    1.57 +
    1.58 +(* PIDE query operation *)
    1.59 +
    1.60 +val _ =
    1.61 +  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
    1.62 +    (case try Toplevel.context_of state of
    1.63 +      SOME ctxt =>
    1.64 +        let
    1.65 +          val [query_arg] = args;
    1.66 +          val query = read_query Position.none query_arg;
    1.67 +        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    1.68 +    | NONE => error "Unknown context"));
    1.69 +
    1.70  end;
    1.71  
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 21:16:50 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 21:49:31 2014 +0200
     2.3 @@ -21,11 +21,11 @@
     2.4  
     2.5  object Find_Dockable
     2.6  {
     2.7 -  private abstract class Operation
     2.8 +  private abstract class Operation(view: View)
     2.9    {
    2.10 +    val pretty_text_area = new Pretty_Text_Area(view)
    2.11      def query_operation: Query_Operation[View]
    2.12      def query: JComponent
    2.13 -    def pretty_text_area: Pretty_Text_Area
    2.14      def page: TabbedPane.Page
    2.15    }
    2.16  }
    2.17 @@ -75,11 +75,8 @@
    2.18  
    2.19    /* find theorems */
    2.20  
    2.21 -  private val find_theorems = new Find_Dockable.Operation
    2.22 +  private val find_theorems = new Find_Dockable.Operation(view)
    2.23    {
    2.24 -    val pretty_text_area = new Pretty_Text_Area(view)
    2.25 -
    2.26 -
    2.27      /* query */
    2.28  
    2.29      private val process_indicator = new Process_Indicator
    2.30 @@ -104,7 +101,7 @@
    2.31      val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
    2.32  
    2.33  
    2.34 -    /* controls */
    2.35 +    /* GUI page */
    2.36  
    2.37      private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
    2.38        tooltip = "Limit of displayed results"
    2.39 @@ -124,9 +121,6 @@
    2.40        reactions += { case ButtonClicked(_) => apply_query() }
    2.41      }
    2.42  
    2.43 -
    2.44 -    /* GUI page */
    2.45 -
    2.46      private val controls: List[Component] =
    2.47        List(query_label, Component.wrap(query), limit, allow_dups,
    2.48          process_indicator.component, apply_button, zoom)
    2.49 @@ -139,9 +133,53 @@
    2.50    }
    2.51  
    2.52  
    2.53 +  /* find consts */
    2.54 +
    2.55 +  private val find_consts = new Find_Dockable.Operation(view)
    2.56 +  {
    2.57 +    /* query */
    2.58 +
    2.59 +    private val process_indicator = new Process_Indicator
    2.60 +
    2.61 +    val query_operation =
    2.62 +      new Query_Operation(PIDE.editor, view, "find_consts",
    2.63 +        consume_status(process_indicator, _),
    2.64 +        (snapshot, results, body) =>
    2.65 +          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
    2.66 +
    2.67 +    private def apply_query()
    2.68 +    {
    2.69 +      query_operation.apply_query(List(query.getText))
    2.70 +    }
    2.71 +
    2.72 +    private val query_label = new Label("Search criteria:") {
    2.73 +      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
    2.74 +    }
    2.75 +
    2.76 +    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
    2.77 +
    2.78 +
    2.79 +    /* GUI page */
    2.80 +
    2.81 +    private val apply_button = new Button("Apply") {
    2.82 +      tooltip = "Find constants by name / type patterns"
    2.83 +      reactions += { case ButtonClicked(_) => apply_query() }
    2.84 +    }
    2.85 +
    2.86 +    private val controls: List[Component] =
    2.87 +      List(query_label, Component.wrap(query), process_indicator.component, apply_button, zoom)
    2.88 +
    2.89 +    val page =
    2.90 +      new TabbedPane.Page("Constants", new BorderPanel {
    2.91 +        add(new Wrap_Panel(Wrap_Panel.Alignment.Right)(controls:_*), BorderPanel.Position.North)
    2.92 +        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
    2.93 +      }, apply_button.tooltip)
    2.94 +  }
    2.95 +
    2.96 +
    2.97    /* operations */
    2.98  
    2.99 -  private val operations = List(find_theorems)
   2.100 +  private val operations = List(find_theorems, find_consts)
   2.101  
   2.102    private val tabs = new TabbedPane { for (op <- operations) pages += op.page }
   2.103    set_content(tabs)