]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/toplevel/top.ml
level disambiguation cmpleted! the Grafite file is succesfully generated.
[helm.git] / helm / software / helena / src / toplevel / top.ml
index 55fdab3ca918502ccf416acc92f9b359f9191d5c..2db38afb88f75591d42e9654857156c3ae915762 100644 (file)
@@ -305,10 +305,6 @@ let main =
    let set_preprocess () = 
       if !G.trace >= 2 then begin preprocess := true; G.summary := true end 
    in 
-   let set_stage i = G.stage := i in
-   let set_madir s = G.ma_dir := s in
-   let set_xdir s = G.xdir := s in
-   let set_root s = root := s in
    let clear_options () =
       export := false; preprocess := false;
       root := "";
@@ -317,7 +313,6 @@ let main =
       streaming := false;
       version := true
    in
-   let set_ma_preamble fname = G.ma_preamble := fname in
    let process_file name =
       if !G.trace >= 2 then L.warn 1 (P.sprintf "Processing file: %s" name);
       if !G.trace >= 2 then Y.utime_stamp "started";
@@ -344,9 +339,9 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -m <file> | -hkr <string> ]* [ <file> ]*\n\n" ^
-      "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, \
-       3 typing information, 4 reduction information\n\n" ^
+      "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -m <file> | -ahkr <string> ]* [ <file> ]*\n\n" ^
+      "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 typing information,\n" ^
+      "              4 conversion information, 5 reduction information, 6 level disambiguation\n\n" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
    in
    let help_L = " show lexer debug information" in 
@@ -357,6 +352,7 @@ let main =
    let help_V = " show version information" in
    let help_X = " clear options" in
    
+   let help_a = "<string>  set prefix of numeric identifiers (default: empty)" in
    let help_d = " show summary information (requires trace >= 2)" in
    let help_g = " always expand global definitions" in
    let help_h = "<string>  set type hierarchy (default: \"Z1\")" in
@@ -376,24 +372,25 @@ let main =
    at_exit exit;
    Arg.parse [
       ("-L", Arg.Set G.debug_lexer, help_L);
-      ("-M", Arg.String set_madir, help_M);
-      ("-O", Arg.String set_xdir, help_O);       
-      ("-P", Arg.Set G.debug_parser, help_P); 
+      ("-M", Arg.String ((:=) G.ma_dir), help_M);
+      ("-O", Arg.String ((:=) G.xdir), help_O);
+      ("-P", Arg.Set G.debug_parser, help_P);
       ("-T", Arg.Int set_trace, help_T);
       ("-V", Arg.Unit print_version, help_V);
       ("-X", Arg.Unit clear_options, help_X);
+      ("-a", Arg.String ((:=) G.alpha), help_a);
       ("-d", Arg.Unit set_summary, help_d);
       ("-g", Arg.Set G.expand, help_g);
       ("-h", Arg.String set_hierarchy, help_h);
       ("-i", Arg.Set G.indexes, help_i);
       ("-k", Arg.String set_kernel, help_k);
       ("-l", Arg.Set G.cc, help_l);
-      ("-m", Arg.String set_ma_preamble, help_m);      
+      ("-m", Arg.String ((:=) G.ma_preamble), help_m);      
       ("-o", Arg.Set G.si, help_o);
       ("-p", Arg.Unit set_preprocess, help_p);
       ("-q", Arg.Set G.unquote, help_q);      
-      ("-r", Arg.String set_root, help_r);
-      ("-s", Arg.Int set_stage, help_s);
+      ("-r", Arg.String ((:=) root), help_r);
+      ("-s", Arg.Int ((:=) G.stage), help_s);
       ("-t", Arg.Clear version, help_t);      
       ("-x", Arg.Set export, help_x);
       ("-1", Arg.Set streaming, help_1);