enable search in pre-loaded theory;
authorwenzelm
Fri Aug 09 17:25:47 2013 +0200 (2013-08-09)
changeset 5294314ddcc0ad7df
parent 52942 07093b66fc9d
child 52944 4b053d8d0e7e
enable search in pre-loaded theory;
src/Pure/Tools/find_theorems.ML
src/Tools/jEdit/src/find_dockable.scala
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 16:17:48 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 17:25:47 2013 +0200
     1.3 @@ -576,13 +576,17 @@
     1.4  (** PIDE query operation **)
     1.5  
     1.6  val _ =
     1.7 -  Query_Operation.register "find_theorems" (fn st => fn [limit_arg, allow_dups_arg, query_arg] =>
     1.8 -    if can Toplevel.context_of st then
     1.9 -      let
    1.10 -        val opt_limit = Int.fromString limit_arg;
    1.11 -        val rem_dups = allow_dups_arg = "false";
    1.12 -        val criteria = read_query Position.none query_arg;
    1.13 -      in Pretty.string_of (pretty_theorems (proof_state st) opt_limit rem_dups criteria) end
    1.14 -    else error "Unknown context");
    1.15 +  Query_Operation.register "find_theorems"
    1.16 +    (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
    1.17 +      if can Toplevel.context_of st then
    1.18 +        let
    1.19 +          val state =
    1.20 +            if context_arg = "" then proof_state st
    1.21 +            else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
    1.22 +          val opt_limit = Int.fromString limit_arg;
    1.23 +          val rem_dups = allow_dups_arg = "false";
    1.24 +          val criteria = read_query Position.none query_arg;
    1.25 +        in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
    1.26 +      else error "Unknown context");
    1.27  
    1.28  end;
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 16:17:48 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 09 17:25:47 2013 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  
     2.5  import scala.actors.Actor._
     2.6  
     2.7 -import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label}
     2.8 +import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
     2.9  import scala.swing.event.ButtonClicked
    2.10  
    2.11  import java.awt.BorderLayout
    2.12 @@ -106,7 +106,8 @@
    2.13    /* controls */
    2.14  
    2.15    private def clicked {
    2.16 -    find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
    2.17 +    find_theorems.apply_query(
    2.18 +      List(limit.text, allow_dups.selected.toString, context.selection.item.name, query.getText))
    2.19    }
    2.20  
    2.21    private val query_label = new Label("Search criteria:")
    2.22 @@ -121,6 +122,19 @@
    2.23      setColumns(40)
    2.24    }
    2.25  
    2.26 +  private case class Context_Entry(val name: String, val description: String)
    2.27 +  {
    2.28 +    override def toString = description
    2.29 +  }
    2.30 +
    2.31 +  private val context_entries =
    2.32 +    new Context_Entry("", "context") ::
    2.33 +      PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
    2.34 +
    2.35 +  private val context = new ComboBox[Context_Entry](context_entries) {
    2.36 +    tooltip = "Search in pre-loaded theory (default: context of current command)"
    2.37 +  }
    2.38 +
    2.39    private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
    2.40      tooltip = "Limit of displayed results"
    2.41      verifier = (s: String) =>
    2.42 @@ -148,7 +162,7 @@
    2.43  
    2.44    private val controls =
    2.45      new FlowPanel(FlowPanel.Alignment.Right)(
    2.46 -      query_label, Component.wrap(query), limit, allow_dups,
    2.47 +      query_label, Component.wrap(query), context, limit, allow_dups,
    2.48        process_indicator.component, apply_query, locate_query, zoom)
    2.49    add(controls.peer, BorderLayout.NORTH)
    2.50  }