src/Pure/Tools/find_consts.ML
changeset 62848 e4140efe699e
parent 61335 43848476063c
child 62969 9f394a16c557
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Apr 04 16:14:22 2016 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Apr 04 17:02:34 2016 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4        Strict of string
     1.5      | Loose of string
     1.6      | Name of string
     1.7 +  val pretty_consts: Proof.context -> (bool * criterion) list -> Pretty.T
     1.8 +  val query_parser: (bool * criterion) list parser
     1.9    val read_query: Position.T -> string -> (bool * criterion) list
    1.10    val find_consts : Proof.context -> (bool * criterion) list -> unit
    1.11  end;
    1.12 @@ -138,25 +140,18 @@
    1.13    Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
    1.14    Parse.typ >> Loose;
    1.15  
    1.16 -val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    1.17 -
    1.18  val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
    1.19  
    1.20  in
    1.21  
    1.22 +val query_parser = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
    1.23 +
    1.24  fun read_query pos str =
    1.25    Token.explode query_keywords pos str
    1.26    |> filter Token.is_proper
    1.27 -  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    1.28 +  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query_parser --| Scan.ahead Parse.eof)))
    1.29    |> #1;
    1.30  
    1.31 -val _ =
    1.32 -  Outer_Syntax.command @{command_keyword find_consts}
    1.33 -    "find constants by name / type patterns"
    1.34 -    (query >> (fn spec =>
    1.35 -      Toplevel.keep (fn st =>
    1.36 -        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
    1.37 -
    1.38  end;
    1.39  
    1.40