X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=f38258d1e96632b4dc14e658b48ccc748a5738e2;hb=11b9b274291baa8c5462b2ce3e2a5f93a39c9d57;hp=054ad98bd5bd2e779d254179673c7fe58532cb25;hpb=c88c60d45e1502d07ebb56275c12255e7cecc290;p=helm.git

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 054ad98bd..f38258d1e 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -34,7 +34,7 @@
 (******************************************************************************)
 
   (* search arguments on which Apply tactic doesn't fail *)
-let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
  let ((_, metasenv, _, _), metano) = status in
  let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
   let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
@@ -51,52 +51,53 @@ let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status =
   let rigth_must = List.map torigth_restriction must in
   let rigth_only = Some (List.map torigth_restriction only) in
   let result =
-         MQueryGenerator.searchPattern
-          (rigth_must,[],[]) (rigth_only,None,None) in 
-        let uris =
-         List.map
-          (function uri,_ ->
-            MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
-          ) result in
-         let uris',exc =
-          let rec filter_out =
-           function
-              [] -> [],""
-            | uri::tl ->
-               let tl',exc = filter_out tl in
-                try
-                 if
-                  (try
-                   ignore
-                    (PrimitiveTactics.apply_tac
-                     ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-                      (MQueryMisc.cic_textual_parser_uri_of_string uri))
-                     ~status);
-                   true
-                  with ProofEngineTypes.Fail _ -> false)
-                 then
-                  uri::tl',exc
-                 else
-                  tl',exc
-                with
-                 e ->
-                  let exc' =
-                   "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
-                    uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
-                  in
-                   tl',exc'
-          in
-           filter_out uris
-         in
-          let html' =
-           " <h1>Objects that can actually be applied: </h1> " ^
-           String.concat "<br>" uris' ^ exc ^
-           " <h1>Number of false matches: " ^
-            string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
-           " <h1>Number of good matches: " ^
-            string_of_int (List.length uris') ^ "</h1>"
-          in
-           output_html html' ;
-           uris'
+	 MQueryInterpreter.execute mqi_handle 
+	    (MQueryGenerator.searchPattern
+		(rigth_must,[],[]) (rigth_only,None,None)) in 
+	let uris =
+	 List.map
+		(function uri,_ ->
+			MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+		) result in
+	 let uris',exc =
+		let rec filter_out =
+		 function
+				[] -> [],""
+			| uri::tl ->
+				 let tl',exc = filter_out tl in
+					try
+					 if
+						(try
+						 ignore
+							(PrimitiveTactics.apply_tac
+							 ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+								(MQueryMisc.cic_textual_parser_uri_of_string uri))
+							 ~status);
+						 true
+						with ProofEngineTypes.Fail _ -> false)
+					 then
+						uri::tl',exc
+					 else
+						tl',exc
+					with
+           (ProofEngineTypes.Fail _) as e ->
+						 let exc' =
+						  "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
+							 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
+						 in
+						  tl',exc'
+		in
+		 filter_out uris
+	 in
+		let html' =
+		 " <h1>Objects that can actually be applied: </h1> " ^
+		 String.concat "<br>" uris' ^ exc ^
+		 " <h1>Number of false matches: " ^
+			string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+		 " <h1>Number of good matches: " ^
+			string_of_int (List.length uris') ^ "</h1>"
+		in
+		 output_html html' ;
+		 uris'
 ;;