]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/options.ml
- revision of ground_2 and basic_2
[helm.git] / helm / software / helena / src / common / options.ml
index 3a394c5b7803191f47cddbafbdf98ac597b4147e..b8ea00387746fa8506e78102036b866b42ecc636 100644 (file)
@@ -17,9 +17,13 @@ type uri_generator = string -> string
 
 type kernel = V4 | V3 | V0
 
+type manager = Quiet
+             | Matita
+             | Coq
+
 (* interface functions ******************************************************)
 
-let version_string = "Helena 0.8.2 M - December 2014"
+let version_string = "Helena 0.8.2 M (February 2015)"
 
 let stage = ref 3            (* stage *)
 
@@ -49,16 +53,22 @@ let debug_parser = ref false (* output parser debug information *)
 
 let debug_lexer = ref false  (* output lexer debug information *)
 
-let ma_dir = ref ""          (* directory for grafite output *)
+let manager_dir = ref ""     (* output directory for manager *)
+
+let manager = ref Quiet      (* manager *)
 
-let ma_preamble = ref ""     (* location of grafite preamble file *)
+let preamble = ref ""        (* preamble file for manager *)
 
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
-let kernel_id () = match !kernel with
-   | V4 -> ""
-   | V3 -> "V3"
-   | V0 -> "V0"
+let kernel_id () = 
+   let id = match !kernel with
+      | V4 -> "Environment"
+      | V3 -> "Environment_V3"
+      | V0 -> "Environment_V0"
+   in
+   let si = if !si then "_si" else "" in
+   id ^ si
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
@@ -72,4 +82,4 @@ let clear () =
    xdir := ""; kernel := V3; si := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false;
    debug_parser := false; debug_lexer := false;
-   ma_dir := ""; ma_preamble := ""
+   manager_dir := ""; manager := Quiet