snapshot

[helm.git] / helm / ocaml / cic_notation / test_parser.ml

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index 522baacccfc4c8dee80ada2fb192c92dc3663e88..1673db6f474a2ef1e7961bcc14ca4f6f39c99a45 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -25,9 +25,7 @@
 
 open Printf
 
-let _ =
-  Helm_registry.load_from "test_parser.conf.xml"
-(*   Http_getter.init () *)
+let _ = Helm_registry.load_from "test_parser.conf.xml"
 
 let xml_stream_of_markup =
   let rec print_box (t: CicNotationPres.boxml_markup) =
@@ -52,6 +50,7 @@ let _ =
     try
       let istream = Stream.of_channel stdin in
        while Stream.peek istream <> None do
+          try
          match CicNotationParser.parse_phrase istream with
            | P.Print t -> 
                 prerr_endline "====";
@@ -63,16 +62,16 @@ let _ =
            | P.Notation (l1, associativity, precedence, l2) ->
                 prerr_endline "Extending parser ..."; flush stdout;
                prerr_endline (CicNotationPp.pp_term l1) ;
+                prerr_endline (sprintf "Found keywords: %s"
+                  (String.concat " " (CicNotationUtil.keywords_of_term l1)));
                 let time1 = Unix.gettimeofday () in
-                  ignore
-                   (CicNotationParser.extend l1 ?precedence ?associativity
-                      (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
+                  ignore (CicNotationParser.extend l1 ?precedence ?associativity
+                     (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
                   let time2 = Unix.gettimeofday () in
                    prerr_endline "Extending pretty printer ..."; flush stdout;
                    let time3 = Unix.gettimeofday () in
-                     ignore
-                       (CicNotationRew.add_pretty_printer ?precedence ?associativity
-                          l2 l1);
+                    ignore (CicNotationRew.add_pretty_printer
+                      ?precedence ?associativity l2 l1);
                      let time4 = Unix.gettimeofday () in
                        printf "done (extending parser took %f, extending pretty printer took %f)\n"
                          (time2 -. time1) (time4 -. time3);
@@ -85,6 +84,7 @@ let _ =
                    printf "done (patterns compilation took %f seconds)\n"
                      (time2 -. time1);
                    flush stdout
+            | P.Dump -> CicNotationParser.print_l2_pattern (); print_newline ()
            | P.Render uri ->
                 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                 let annobj, _, _, id_to_sort, _, _, _ =
@@ -111,13 +111,17 @@ let _ =
                    prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3));
                    prerr_endline (CicNotationPp.pp_term t');
                    dump_xml t' id_to_uri "out.xml"
-(*                     CicNotationParser.print_l2_pattern () *)
                      (*    let (x, y) = P.loc_of_floc floc in *)
                      (*    let before = String.sub line 0 x in *)
                      (*    let error = String.sub line x (y - x) in *)
                      (*    let after = String.sub line y (String.length line - y) in *)
                      (*      eprintf "%s\e[01;31m%s\e[00m%s\n" before error after; *)
                      (*      prerr_endline (sprintf "at character %d-%d: %s" x y msg) *)
+        with
+        | End_of_file -> raise End_of_file
+        | exn ->
+            prerr_endline
+              (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
        done
     with End_of_file ->
       ()