X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2Foptions.ml;h=0b9487d6bf68d6d15ed8f4faba317b4ae76fa54c;hb=076439def28e649ec384fae038ed021dadd5f75c;hp=23f208d538ba7b72a8094d9ba94d7cbc6fd8a5bf;hpb=603c8b3cdab901c26f63b5fed2c65e49693cc9a3;p=helm.git

diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml
index 23f208d53..0b9487d6b 100644
--- a/matita/components/binaries/probe/options.ml
+++ b/matita/components/binaries/probe/options.ml
@@ -1,43 +1,124 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   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 UriPair = struct
+
+  type t = U.uri * U.uri
+
+  let equal (u1l,u1r) (u2l,u2r) =
+     U.eq u1l u2l && U.eq u1r u2r
+
+  let compare (u1l,u1r) (u2l,u2r) =
+    match U.compare u1l u2l with
+    | 0 -> U.compare u1r u2r
+    | c -> c
+
+  let hash (ul,ur) =
+    Hashtbl.hash (U.hash ul, U.hash ur)
+
+end
+
+module UPS = Set.Make(UriPair)
+
+type def_xflavour = [ C.def_flavour
+                    | `Inductive
+                    ]
+
 let default_objs = US.empty
 
 let default_srcs = US.empty
 
+let default_names = US.empty
+
+let default_remove = []
+
 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
 
+let names = ref default_names
+
+let remove = ref default_remove
+
 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 = ref UPS.empty
+
+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 =
+  deps := UPS.add (c,u) !deps
+
+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
+  UPS.iter map !deps;
+  close_out och
+
 let clear () =
-   R.clear ();
-   objs := default_objs; srcs := default_srcs;
-   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; names := default_names;
+  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;
+  deps := UPS.empty