updated probe and matitadep

[helm.git] / matita / components / binaries / probe / options.ml

diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml
index 4c3c51d12028db93d7378371a375a59eaa970d10..981483e29b196ce8fbbae3a593f7f004913bfb12 100644 (file)
--- a/matita/components/binaries/probe/options.ml
+++ b/matita/components/binaries/probe/options.ml
@@ -9,8 +9,18 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
+module A = Array
+module P = Printf
+
+module C  = NCic
 module R  = Helm_registry
+module U  = NUri
 module US = NUri.UriSet
+module UH = NUri.UriHash
+
+type def_xflavour = [ C.def_flavour
+                    | `Inductive
+                    ]
 
 let default_objs = US.empty
 
@@ -22,10 +32,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 +54,49 @@ 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 deps = UH.create 11
+
+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 add_dep c u =
+  UH.add deps c u
+
+let out_deps file =
+  let och = open_out file in
+  let map a b =
+    P.fprintf och "\"%s\": \"%s\"\n" (U.string_of_uri a) (U.string_of_uri b)
+  in
+  UH.iter map deps;
+  close_out och
+
 let clear () =
-   R.clear ();
-   objs := default_objs; srcs := default_srcs; remove := default_remove;
-   exclude := default_exclude; net := default_net;
-   no_devel := default_no_devel; no_init := default_no_init
+  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;
+  UH.reset deps