Removed several try .... with _ -> (which make thread killing impossible ;-((

[helm.git] / helm / ocaml / tactics / tacticChaser.ml

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 054ad98bd5bd2e779d254179673c7fe58532cb25..d09eacc49773a2a655db35a2d545e47c5a9bb975 100644 (file)
--- 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' =
-                   "<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'
+        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'
 ;;