From 5716f9072fc8a7d46324e91cca970489c59cc590 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jul 2006 12:09:46 +0000
Subject: [PATCH] GrafiteAst.Search_pat and GrafiteAst.Search_term (both
 unused) removed.

---
 helm/software/components/grafite/grafiteAst.ml              | 6 ------
 helm/software/components/grafite/grafiteAstPp.ml            | 4 ----
 .../components/grafite_parser/grafiteDisambiguate.ml        | 4 +---
 helm/software/matita/matitaScript.ml                        | 2 --
 4 files changed, 1 insertion(+), 15 deletions(-)

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 73ae34584..6c6b3786f 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -104,16 +104,10 @@ type 'term macro =
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
-(*   | Abort of loc *)
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
   | Quit of loc
-(*   | Redo of loc * int option
-  | Undo of loc * int option *)
-(*   | Print of loc * print_kind *)
-  | Search_pat of loc * search_kind * string  (* searches with string pattern *)
-  | Search_term of loc * search_kind * 'term  (* searches with term pattern *)
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index b95df8d36..c5bbe8f19 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -182,10 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | 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) (term_pp term)
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
 
diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b02d57e67..396d169e7 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -327,6 +327,4 @@ let disambiguate_macro
    | GrafiteAst.WLocate _ as macro ->
       metasenv,macro
    | GrafiteAst.Quit _
-   | GrafiteAst.Print _
-   | GrafiteAst.Search_pat _
-   | GrafiteAst.Search_term _ -> assert false
+   | GrafiteAst.Print _ -> assert false
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 5674063e9..a6842d832 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -291,8 +291,6 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
   (* TODO *)
   | TA.Quit _ -> failwith "not implemented"
   | TA.Print (_,kind) -> failwith "not implemented"
-  | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
-  | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff
 lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
-- 
2.39.2