new options activated

[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 77a7e2c25682610faec295684a2e33c2cb606e5d..ffef0796ee9292150124e438027f16fe467a00ac 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -20,7 +20,8 @@ type kernel = V4 | V3 | V0
 type manager = Quiet
              | Coq
              | Matita
-             | ELPI
+             | ELPI1
+             | ELPI2
 
 (* interface functions ******************************************************)
 
@@ -30,6 +31,8 @@ let stage = ref 3            (* stage *)
 
 let trace = ref 0            (* trace level *)
 
+let ct = ref 0               (* current trace level *)
+
 let summary = ref false      (* log summary information *)
 
 let xdir = ref ""            (* directory for XML output *)
@@ -62,6 +65,15 @@ let preamble = ref ""        (* preamble file for manager *)
 
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
+let first = ref 0            (* begin trace here *)
+
+let last = ref max_int       (* end trace here *) 
+
+let extended = ref false     (* extended applications *) 
+
+let set_current_trace n =
+   ct := if !first <= n && n <= !last then !trace else 0
+
 let kernel_id () = 
    let id = match !kernel with
       | V4 -> "Environment"
@@ -69,7 +81,8 @@ let kernel_id () =
       | V0 -> "Environment_V0"
    in
    let si = if !si then "_si" else "" in
-   id ^ si
+   let ext = if !extended then "_x" else "" in
+   id ^ si ^ ext
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
@@ -79,8 +92,8 @@ let get_mk_uri () =
    fun s -> KF.concat bu (s ^ ".ld")
 
 let clear () =
-   stage := 3; trace := 0; summary := false; 
-   xdir := ""; kernel := V3; si := false; cover := ""; 
+   stage := 3; trace := 0; summary := false; first := 0; last := max_int;
+   xdir := ""; kernel := V3; si := false; extended := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false;
    debug_parser := false; debug_lexer := false;
    manager_dir := ""; manager := Quiet