X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Foptions.ml;h=d84d2b3e11c9343dbddb76b0e15af2609bb29f74;hb=2f20aaf586f7cb4fd2933d765f4d09fcf077e4c5;hp=4c3c51d12028db93d7378371a375a59eaa970d10;hpb=8ff4315142253a1a0478b67c07dddf70c36f50cd;p=helm.git

diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml
index 4c3c51d12..d84d2b3e1 100644
--- a/matita/components/binaries/probe/options.ml
+++ b/matita/components/binaries/probe/options.ml
@@ -9,9 +9,17 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
+module A = Array
+module P = Printf
+
+module C = NCic
 module R  = Helm_registry
 module US = NUri.UriSet
 
+type def_xflavour = [ C.def_flavour
+                    | `Inductive
+                    ]
+
 let default_objs = US.empty
 
 let default_srcs = US.empty
@@ -22,10 +30,18 @@ let default_exclude = []
 
 let default_net = 0
 
+let default_chars = 0
+
+let default_debug_lexer = false
+
 let default_no_devel = true
 
 let default_no_init = true
 
+let xflavours = 8
+
+let slot = A.make xflavours 0
+
 let objs = ref default_objs
 
 let srcs = ref default_srcs
@@ -36,12 +52,35 @@ let exclude = ref default_exclude
 
 let net = ref default_net
 
+let chars = ref default_chars
+
+let debug_lexer = ref default_debug_lexer
+
 let no_devel = ref default_no_devel
 
 let no_init = ref default_no_init
 
+let index_of_xflavour = function 
+   | `Inductive  -> 0
+   | `Axiom      -> 1 
+   | `Definition -> 2
+   | `Fact       -> 3
+   | `Lemma      -> 4
+   | `Theorem    -> 5
+   | `Corollary  -> 6
+   | `Example    -> 7
+
+let add_xflavour n xf =
+   let i = index_of_xflavour xf in
+   slot.(i) <- slot.(i) + n
+
+let clear_slot i _ = slot.(i) <- 0
+
+let iter_xflavours map = A.iteri (fun _ -> map) slot
+
 let clear () =
-   R.clear ();
+   R.clear (); A.iteri clear_slot slot;
    objs := default_objs; srcs := default_srcs; remove := default_remove;
    exclude := default_exclude; net := default_net;
+   chars := default_chars; debug_lexer := default_debug_lexer;
    no_devel := default_no_devel; no_init := default_no_init