]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/test_parser.ml
Partial porting to V8 URIs.
[helm.git] / helm / ocaml / cic_disambiguation / test_parser.ml
index ff4ae9726e41bac09d7dad80d831d92d54e1d6bd..d6afddc670607b1099de6e7384f3bb9f28744458 100644 (file)
@@ -27,6 +27,11 @@ let default_mode = `Term
 
 let mode = ref default_mode
 
+(* let pp_tactical = TacticAstPp.pp_tactical *)
+
+let pp_tactical = TacticAst2Box.tacticalPp
+
+
 let _ =
   try
     match Sys.argv.(1) with
@@ -55,15 +60,18 @@ let _ =
             print_endline (TacticAstPp.pp_tactic term)
         | `Tactical ->
             let term = CicTextualParser2.parse_tactical istream in
-            print_endline (TacticAstPp.pp_tactical term)
+            print_endline (pp_tactical term)
         | `Alias ->
             let env = CicTextualParser2.EnvironmentP3.of_string line in
             print_endline (CicTextualParser2.EnvironmentP3.to_string env));
         flush stdout
       with
+      | CicTextualParser2.Parse_error msg -> prerr_endline msg
+(*
       | Stdpp.Exc_located ((p_start, p_end), exn) ->
         prerr_endline (Printf.sprintf "Exception at character %d-%d: %s"
           p_start p_end (Printexc.to_string exn))
+*)
     done
   with End_of_file ->
     close_in ic