]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/top.ml
transcript: we now check for non-existing objects
[helm.git] / helm / software / components / binaries / transcript / top.ml
index 5b3b234730fff1c8d61a06764aa22125ed10ffbb..c92b71512e05ffdb47432702cae54e31887011e2 100644 (file)
  *)
 
 let main =
-   let cwd = ref Filename.current_dir_name in
-   let help = "Usage: transcript [ -C <dir> ] [ <package> | <conf_file> ]*" in
+   let help = "Usage: transcript [ -glmpx | -C <dir> ] [ <package> | <conf_file> ]*" in
    let help_C = " set working directory to <dir>" in
-   let help_vp = " verbose parsing" in
-   let help_vl = " verbose lexing" in
-   let help_vx = " verbose character escaping" in
-   let set_cwd dir = cwd := dir in
-   let process_package package = Engine.produce (Engine.make !cwd package) in
-   Engine.init ();
+   let help_g = " check for non existing objects" in
+   let help_l = " verbose lexing" in
+   let help_m = " minimal output generation" in
+   let help_p = " verbose parsing" in
+   let help_x = " verbose character escaping" in
+   let set_cwd dir = Options.cwd := dir; Engine.init () in
+   let process_package package = Engine.produce (Engine.make package) in
    Arg.parse [
       ("-C", Arg.String set_cwd, help_C);
-      ("-vp", Arg.Set Options.verbose_parser, help_vp);
-      ("-vl", Arg.Set Options.verbose_lexer, help_vl);
-      ("-vx", Arg.Set Options.verbose_escape, help_vx);
+      ("-g", Arg.Set Options.getter, help_g);
+      ("-l", Arg.Set Options.verbose_lexer, help_l);
+      ("-m", Arg.Clear Options.comments, help_m);
+      ("-p", Arg.Set Options.verbose_parser, help_p);
+      ("-x", Arg.Set Options.verbose_escape, help_x);
    ] process_package help