- bug fix in the static disambiguation of unified binders

[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 d91ba1724180ce2a448b3d5db5d0d9aaf0839730..55fdab3ca918502ccf416acc92f9b359f9191d5c 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -11,14 +11,15 @@
 
 module F  = Filename
 module P  = Printf
+
 module U  = NUri
 module C  = Cps
 module L  = Log
 module Y  = Time
 module G  = Options
 module H  = Hierarchy
-module O  = Output
 module E  = Entity
+module O  = Output
 module S  = Status
 module DO = CrgOutput
 module TD = TxtCrg
@@ -305,6 +306,7 @@ let main =
       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 () =
@@ -342,12 +344,13 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -O <dir> | -m <file> | -hkr <string> ]* [ <file> ]*\n\n" ^
+      "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" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
    in
    let help_L = " show lexer debug information" in 
+   let help_M = "<dir>  set location of output directory (Grafite) to <dir> (default: current directory)" in
    let help_O = "<dir>  set location of output directory (XML) to <dir> (default: current directory)" in
    let help_P = " show parser debug information" in 
    let help_T = "<number>  set trace level (see above)" in
@@ -360,7 +363,7 @@ let main =
    let help_i = " show local references by index" in
    let help_k = "<string>  set kernel version (default: \"brg\")" in
    let help_l = " disambiguate binders level (Automath)" in
-   let help_m = "<file>  set location of Matita preamble to <file> (default: empty)" in   
+   let help_m = "<file>  export kernel entities (Grafite) setting location of preamble to <file> (default: empty)" 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
@@ -372,7 +375,8 @@ let main =
    let help_1 = " parse files with streaming policy" in
    at_exit exit;
    Arg.parse [
-      ("-L", Arg.Set G.debug_lexer, help_L); 
+      ("-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); 
       ("-T", Arg.Int set_trace, help_T);