]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/testlibrary.ml
Big bug fixed: batchParser applied the varsprefix prefix also to
[helm.git] / helm / gTopLevel / testlibrary.ml
index ea6e4c6c037db42b62fb335e94a6776bc9d7546a..af459000a0c18e44de8f41e20b1f14e16e4dc5e6 100644 (file)
@@ -12,7 +12,7 @@ let verbose = false
 exception Failure of string
 let fail msg = raise (Failure msg)
 
-let uri_predicate = ref BatchParser.constants_only
+let uri_predicate = ref (BatchParser.constants_only ~prefix:"")
 
 module DisambiguateCallbacks =
  struct
@@ -147,18 +147,23 @@ let _ =
        (HelmLogger.string_of_html_msg msg));
   let names = ref [] in
   let tryvars = ref false in
-  let varsprefix = ref "" in
+  let prefix = ref "" in
+  let varsprefix = ref "####" in
   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
   let spec =
     [ "-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" ; 
       "-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 name -> names := name :: !names) usage;
   let names = List.rev !names in
-  uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix;
+  if !varsprefix = "####" then varsprefix := !prefix ;
+  uri_predicate :=
+   BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix;
   let status = (ref [], ref [], ref []) in  (* <ok, nok, maybe> URIs *)
   List.iter
     (fun name ->