From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 11 Jan 2005 16:05:23 +0000 (+0000)
Subject: added search commands
X-Git-Tag: V_0_1_0~145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9701a8bee17d66e49a5cff28dc62963c54fadc6b;p=helm.git

added search commands
---

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 28b256c86..8c678de93 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -88,10 +88,14 @@ type thm_flavour =
   * true means inductive, false coinductive *)
 type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
+type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+
 type 'term command =
   | Abort
   | Baseuri of string option (** get/set base uri *)
   | Check of 'term
+  | Search_pat of search_kind * string  (* searches with string pattern *)
+  | Search_term of search_kind * 'term  (* searches with term pattern *)
   | Proof
   | Qed of string option
       (** name.
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bc021c134..05927a193 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -96,6 +96,12 @@ let pp_flavour = function
   | `Remark -> "Remark"
   | `Theorem -> "Theorem"
 
+let pp_search_kind = function
+  | `Locate -> "locate"
+  | `Hint -> "hint"
+  | `Match -> "match"
+  | `Elim -> "elim"
+
 let pp_command = function
   | Abort -> "Abort"
   | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
@@ -107,6 +113,10 @@ let pp_command = function
   | Quit -> "Quit"
   | Redo None -> "Redo"
   | Redo (Some n) -> sprintf "Redo %d" n
+  | Search_pat (kind, pat) ->
+      sprintf "search %s \"%s\"" (pp_search_kind kind) pat
+  | Search_term (kind, term) ->
+      sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
   | Inductive (params, types) ->
       let pp_params = function
         | [] -> ""