- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / common / options.ml

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 8cc200ad92b025b9063e171f6a6fe4782aecfbad..0c32d1138e775bb51c17ed21b47fc2b90e73741b 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -9,6 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module F = Filename
 module C = Cps
 
 type uri_generator = string -> string
@@ -17,9 +18,17 @@ type kernel = Crg | Brg | Bag
 
 (* interface functions ******************************************************)
 
-let xdir = ref ""
+let version_string = "Helena 0.8.2 M - November 2014"
 
-let kernel = ref Brg
+let stage = ref 3            (* stage *)
+
+let trace = ref 0            (* trace level *)
+
+let summary = ref false      (* log summary information *)
+
+let xdir = ref ""            (* directory for XML output *)
+
+let kernel = ref Brg         (* kernel type *)
 
 let si = ref false           (* use sort inclusion *)
 
@@ -39,6 +48,8 @@ let debug_parser = ref false (* output parser debug information *)
 
 let debug_lexer = ref false  (* output lexer debug information *)
 
+let ma_preamble = ref ""     (* location of Matita preamble file *)
+
 let kernel_id () = 
    let id = match !kernel with
       | Crg -> "crg"
@@ -49,13 +60,15 @@ let kernel_id () =
    id ^ si
 
 let get_baseuri () =
-   String.concat "/" ["ld:"; kernel_id (); !cover ]
+   String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
 
 let get_mk_uri () =
    let bu = get_baseuri () in
-   fun s -> bu ^ "/" ^ s ^ ".ld"
+   fun s -> F.concat bu (s ^ ".ld")
 
 let clear () =
+   stage := 3; trace := 0; summary := false; 
    xdir := ""; kernel := Brg; si := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false;
-   debug_parser := false; debug_lexer := false
+   debug_parser := false; debug_lexer := false;
+   ma_preamble := ""