new options activated

[helm.git] / helm / software / helena / src / toplevel / top.ml

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 3ce7bbc7026252f29724ea52559cafa3288d3218..984933290764364f3ecd8d71f088efcbeead5f00 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -236,7 +236,7 @@ let process_2 st entity =
      | Some (export_entity, _) -> manager st export_entity entity
 
 let process_1 st entity = 
-   if !G.trace >= 3 then pp_progress entity;
+   if !G.ct >= 3 then pp_progress entity;
    let st = if !G.summary then count_entity st entity else st in
    if !export && !G.stage = 1 then export_entity st entity;
    if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st 
@@ -313,10 +313,11 @@ let main =
       if !G.trace >= 2 then begin preprocess := true; G.summary := true end 
    in
    let set_manager s = match KS.lowercase s with
-      | "v8"   -> G.manager := G.Coq
-      | "ma2"  -> G.manager := G.Matita
-      | "elpi" -> G.manager := G.ELPI
-      | s      -> L.warn level (KP.sprintf "Unknown manager: %s" s) 
+      | "v8"    -> G.manager := G.Coq
+      | "ma2"   -> G.manager := G.Matita
+      | "elpi1" -> G.manager := G.ELPI1
+      | "elpi2" -> G.manager := G.ELPI2
+      | s       -> L.warn level (KP.sprintf "Unknown manager: %s" s) 
    in
    let clear_options () =
       export := false; preprocess := false;
@@ -335,7 +336,8 @@ let main =
       begin match !G.manager with
          | G.Coq    -> st := {!st with mst = Some (BA.open_out base_name)}
          | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)}
-         | G.ELPI   -> st := {!st with mst = Some (BP.open_out base_name)}
+         | G.ELPI1  -> st := {!st with mst = Some (BP.open_out_1 base_name)}
+         | G.ELPI2  -> st := {!st with mst = Some (BP.open_out_2 base_name)}
          | G.Quiet  -> ()
       end;
       P.clear_marks ();
@@ -357,12 +359,12 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -c <file> | -ahkmr <string> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXdgilnopqtx1 | -Ts <number> | -MO <dir> | -c <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
       "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
       "              7 level disambiguation\n\n" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
-      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi\" (lambda-Prolog)\n" 
+      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi1\" \"elpi2\" (lambda-Prolog)\n" 
    in
    let help_L = " show lexer debug information" in 
    let help_M = "<dir>  set location of output directory (manager) to <dir> (default: current directory)" in
@@ -373,20 +375,23 @@ let main =
    let help_X = " clear options" in
    
    let help_a = "<string>  set prefix of numeric identifiers (default: empty)" in
+   let help_b = "<age>  begin trace at this global constant (default: first)" in
    let help_c = "<file>  set preamble to this file (default: empty)" in
    let help_d = " show summary information (requires trace >= 2)" in
+   let help_e = "<age>  end trace at this global constant (default: last)" in
    let help_g = " always expand global definitions" in
    let help_h = "<string>  set type hierarchy (default: \"Z1\")" in
    let help_i = " show local references by index" in
    let help_k = "<string>  set kernel version (default: \"V3\")" in
-   let help_l = " disambiguate binders level (Automath)" in
+   let help_l = " disambiguate binders layer (Automath)" in
    let help_m = "<string>  export kernel entities for this manager (see above, default: no manager)" in
+   let help_n = " use extended (i.e. native) applications (Automath)" in
    let help_o = " activate sort inclusion (default: false)" in
    let help_p = " preprocess source (Automath)" in
    let help_q = " disable quotation of identifiers" in
    let help_r = "<string>  set initial segment of URI hierarchy (default: empty)" in
    let help_s = "<number>  set translation stage (see above)" in
-   let help_t = " type check [version 1]" in
+   let help_t = " type check (version 1)" in
    let help_x = " export kernel entities (XML)" in
    
    let help_1 = " parse files with streaming policy" in
@@ -400,14 +405,17 @@ let main =
       ("-V", Arg.Unit print_version, help_V);
       ("-X", Arg.Unit clear_options, help_X);
       ("-a", Arg.String ((:=) G.alpha), help_a);
+      ("-b", Arg.Int ((:=) G.first), help_b);
       ("-c", Arg.String ((:=) G.preamble), help_c);
       ("-d", Arg.Unit set_summary, help_d);
+      ("-e", Arg.Int ((:=) G.last), help_e);
       ("-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_manager, help_m);      
+      ("-n", Arg.Set G.extended, help_n);
       ("-o", Arg.Set G.si, help_o);
       ("-p", Arg.Unit set_preprocess, help_p);
       ("-q", Arg.Set G.unquote, help_q);