X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Ftest_parser.ml;h=3b30e59001dd35aba70508c6ecdf4ce2b5adebe3;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=31bcdad054e19763f646e09527a5455c63ee80f5;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 31bcdad05..3b30e5900 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -27,16 +27,17 @@ open Printf let pp_tactical = TacticAst2Box.tacticalPp +let modes = ("term",`Term) :: ("statement",`Statement) :: [] + let mode = try - match Sys.argv.(1) with - | "term" -> prerr_endline "Term"; `Term - | "statement" -> prerr_endline "Statement"; `Statement -(* | "script" -> prerr_endline "Script"; `Script *) - | _ -> - prerr_endline "What???????"; - exit 1 - with Invalid_argument _ -> prerr_endline "Term"; `Term + List.assoc (Sys.argv.(1)) modes + with + | _ -> + prerr_endline + (sprintf "What? Supported modes are: %s\n" + (String.concat " " (List.map fst modes))); + exit 1 let _ = (* @@ -63,10 +64,11 @@ let _ = print_endline (BoxPp.pp_term term) | `Statement -> (match CicTextualParser2.parse_statement istream with - | TacticAst.Command (_, cmd) -> - print_endline (TacticAstPp.pp_command cmd) - | TacticAst.Tactical (_, tac) -> - print_endline (TacticAstPp.pp_tactical tac)) + | TacticAst.Executable (_, exe) + | TacticAst.Comment (_,TacticAst.Code (_, exe)) -> + print_endline (TacticAstPp.pp_executable exe) + | TacticAst.Comment (_,TacticAst.Note (_, note)) -> + print_endline note) (* | `Tactical -> let tac = CicTextualParser2.parse_tactical istream in