X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=d09eacc49773a2a655db35a2d545e47c5a9bb975;hb=30ad9beff172b797049b772e0a710c466c9ed18a;hp=054ad98bd5bd2e779d254179673c7fe58532cb25;hpb=2a825bacd5664c01ae56ed1255390a5972d1e8b9;p=helm.git
diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 054ad98bd..d09eacc49 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -51,52 +51,52 @@ 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' =
- "
^ Exception raised trying to apply " ^
- uri ^ ": " ^ Printexc.to_string e ^ "
" ^ exc
- in
- tl',exc'
- in
- filter_out uris
- in
- let html' =
- " Objects that can actually be applied:
" ^
- String.concat "
" uris' ^ exc ^
- " Number of false matches: " ^
- string_of_int (List.length uris - List.length uris') ^ "
" ^
- " Number of good matches: " ^
- string_of_int (List.length uris') ^ "
"
- in
- output_html html' ;
- uris'
+ 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' =
+ " ^ Exception raised trying to apply " ^
+ uri ^ ": " ^ Printexc.to_string e ^ "
" ^ exc
+ in
+ tl',exc'
+ in
+ filter_out uris
+ in
+ let html' =
+ " Objects that can actually be applied:
" ^
+ String.concat "
" uris' ^ exc ^
+ " Number of false matches: " ^
+ string_of_int (List.length uris - List.length uris') ^ "
" ^
+ " Number of good matches: " ^
+ string_of_int (List.length uris') ^ "
"
+ in
+ output_html html' ;
+ uris'
;;