some renaming and some interfaces improved

[helm.git] / helm / software / lambda-delta / toplevel / top.ml

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 3fa3c908ce66ccee70ca5c3756167af76323b775..13887c6ef28e508258220d9e90687e974b6a590b 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -25,10 +25,11 @@ module MBrg = MetaBrg
 module G    = Library
 module BrgO = BrgOutput
 module BrgR = BrgReduction
+module BrgT = BrgType
 module BrgU = BrgUntrusted
 module MBag = MetaBag
 module BagO = BagOutput
-module BagR = BagReduction
+module BagT = BagType
 module BagU = BagUntrusted
 
 type status = {
@@ -58,7 +59,7 @@ let bag_error s msg =
    L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush () 
 
 let brg_error s msg =
-   L.error BrgO.specs (L.Warn s :: L.Loc :: msg); flush () 
+   L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush () 
 
 let process_item f st =
    let f ast = f {st with ast = ast} in
@@ -106,7 +107,7 @@ let type_check f st si g k =
 
 let main =
 try 
-   let version_string = "Helena 0.8.0 M - August 2009" in
+   let version_string = "Helena 0.8.0 M - September 2009" in
    let stage = ref 3 in
    let moch = ref None in
    let meta = ref false in
@@ -203,7 +204,7 @@ try
       flush ()
    in
    let help = 
-      "Usage: helena [ -Vacimpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+      "Usage: helena [ -Vcijmpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
       "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
        3 data information, 4 typing information, 5 reduction information\n\n" ^
        "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
@@ -211,13 +212,13 @@ try
    let help_S = "<number>  set summary level (see above)" in
    let help_V = " show version information" in   
 
-   let help_a = " analyze source files" in
    let help_c = " disable initial segment of URI hierarchy" in
    let help_h = "<string>  set type hierarchy (default: Z2)" in
    let help_i = " show local references by index" in
+   let help_j = " show URI of processed kernel objects" in
    let help_k = "<string>  set kernel version (default: brg)" in
    let help_m = " output intermediate representation (HAL)" in
-   let help_p = " activate progress indicator" in
+   let help_p = " preprocess Automath source" in
    let help_u = " activate sort inclusion" in
    let help_s = "<number>  set translation stage (see above)" in
    let help_x = " export kernel objects (XML)" in
@@ -227,16 +228,16 @@ try
    Arg.parse [
       ("-S", Arg.Int set_summary, help_S);
       ("-V", Arg.Unit print_version, help_V);
-      ("-a", Arg.Set process, help_a);      
       ("-c", Arg.Clear use_cover, help_c);
       ("-h", Arg.String set_hierarchy, help_h);
       ("-i", Arg.Set O.indexes, help_i);
+      ("-j", Arg.Set progress, help_j);      
       ("-k", Arg.String set_kernel, help_k);
       ("-m", Arg.Set meta, help_m); 
-      ("-p", Arg.Set progress, help_p);
+      ("-p", Arg.Set process, help_p);      
       ("-u", Arg.Set si, help_u);
       ("-s", Arg.Int set_stage, help_s);
       ("-x", Arg.Set export, help_x)
    ] read_file help;
-with BagR.TypeError msg -> bag_error "Type Error" msg
-   | BrgR.TypeError msg -> brg_error "Type Error" msg
+with BagT.TypeError msg -> bag_error "Type Error" msg
+   | BrgT.TypeError msg -> brg_error "Type Error" msg