]> matita.cs.unibo.it Git - helm.git/blob - matita/components/binaries/probe/options.ml
commit in ground_2, static_2, basic_2, apps_2
[helm.git] / matita / components / binaries / probe / options.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 module A = Array
13 module P = Printf
14
15 module C = NCic
16 module R  = Helm_registry
17 module US = NUri.UriSet
18
19 type def_xflavour = [ C.def_flavour
20                     | `Inductive
21                     ]
22
23 let default_objs = US.empty
24
25 let default_srcs = US.empty
26
27 let default_remove = []
28
29 let default_exclude = []
30
31 let default_net = 0
32
33 let default_chars = 0
34
35 let default_debug_lexer = false
36
37 let default_no_devel = true
38
39 let default_no_init = true
40
41 let xflavours = 8
42
43 let slot = A.make xflavours 0
44
45 let objs = ref default_objs
46
47 let srcs = ref default_srcs
48
49 let remove = ref default_remove
50
51 let exclude = ref default_exclude
52
53 let net = ref default_net
54
55 let chars = ref default_chars
56
57 let debug_lexer = ref default_debug_lexer
58
59 let no_devel = ref default_no_devel
60
61 let no_init = ref default_no_init
62
63 let index_of_xflavour = function 
64    | `Inductive  -> 0
65    | `Axiom      -> 1 
66    | `Definition -> 2
67    | `Fact       -> 3
68    | `Lemma      -> 4
69    | `Theorem    -> 5
70    | `Corollary  -> 6
71    | `Example    -> 7
72
73 let add_xflavour n xf =
74    let i = index_of_xflavour xf in
75    slot.(i) <- slot.(i) + n
76
77 let clear_slot i _ = slot.(i) <- 0
78
79 let iter_xflavours map = A.iteri (fun _ -> map) slot
80
81 let clear () =
82    R.clear (); A.iteri clear_slot slot;
83    objs := default_objs; srcs := default_srcs; remove := default_remove;
84    exclude := default_exclude; net := default_net;
85    chars := default_chars; debug_lexer := default_debug_lexer;
86    no_devel := default_no_devel; no_init := default_no_init