X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fregtest.ml;h=c6b598151b2127babf3df6f449274fe41c857caa;hb=9af598ece6749c1854799f5aa83133b9e3da052c;hp=4e72bdd544616a50078e82e26910c2b2d84755e4;hpb=9b0237f419714f67bfe4ae0cdee2c59986588e50;p=helm.git diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 4e72bdd54..c6b598151 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -275,8 +275,8 @@ let restore_environment filename = else CicEnvironment.empty () -let main mqi_handle generate dump fnames tryvars varsprefix = - let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in +let main mqi_handle generate dump fnames tryvars prefix varsprefix = + let uri_pred = BatchParser.uri_pred_of_conf tryvars ~prefix ~varsprefix in if generate then begin (* gen mode *) @@ -339,7 +339,8 @@ let _ = (if append_NL then prerr_endline else prerr_string) (HelmLogger.string_of_html_msg msg)); - let mqi_debug_fun = ignore in + let mqi_debug_fun s = + HelmLogger.log ~append_NL:true (`Msg (`T s)) in let mqi_handle = MQIConn.init ~log:mqi_debug_fun () in let fnames = ref [] in @@ -347,7 +348,8 @@ let _ = let tryvars = ref false in let dump = ref false in let nodump = ref false in - let varsprefix = ref "" in + let prefix = ref "" in + let varsprefix = ref "###" in let usage = "regtest [OPTION] ... test1 ..." in let spec = ["-gen", Arg.Set gen, @@ -360,14 +362,19 @@ let _ = "--nodump", Arg.Set nodump, "do not dump the final environment" ; "-vars", Arg.Set tryvars, "try also variables" ; "-novars", Arg.Clear tryvars, "do not try variables (default)" ; + "-prefix", Arg.Set_string prefix, + "limit object choices to URIs beginning with prefix" ; + "--prefix", Arg.Set_string prefix, + "limit object choices to URIs beginning with prefix" ; "-varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "limit variable choices to URIs beginning with prefix; overrides -prefix" ; "--varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "limit variable choices to URIs beginning with prefix; overrides -prefix" ] in Arg.parse spec (fun filename -> fnames := filename::!fnames ) usage ; if !fnames = [] then Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ; - main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix; + if !varsprefix = "###" then varsprefix := !prefix ; + main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix; MQIConn.close mqi_handle