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.
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_______________________________________________________________ *)
12 module R = Helm_registry
18 let incremental = ref true
19 let separate = ref false
30 Scanf.sscanf s "%u %u" A.mk_exists
33 Scanf.sscanf s "%u" A.mk_or
36 Scanf.sscanf s "%u" A.mk_and
38 let process_centralized conf =
40 if R.has "xoa.objects" && R.has "xoa.notations" then begin
41 let ooch = L.open_out true preamble (R.get_string "xoa.objects") in
42 let noch = L.open_out false preamble (R.get_string "xoa.notations") in
43 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
44 L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");
45 List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
46 List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
47 List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
48 close_out noch; close_out ooch
51 let generate (p, o, n) d =
52 let oname, nname = match d with
54 let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
55 let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
58 let oname = Printf.sprintf "%s/or_%u" o c in
59 let nname = Printf.sprintf "%s/or_%u" n c in
62 let oname = Printf.sprintf "%s/and_%u" o c in
63 let nname = Printf.sprintf "%s/and_%u" n c in
66 if !incremental && L.exists_out oname && L.exists_out nname then () else
68 let ooch = L.open_out true p oname in
69 let noch = L.open_out false p nname in
70 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
71 L.out_include ooch (nname ^ ".ma");
72 E.generate ooch noch d;
73 close_out noch; close_out ooch
76 let process_distributed conf =
78 if R.has "xoa.objects" && R.has "xoa.notations" then begin
79 let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
80 List.iter (generate st) (R.get_list unm_ex "xoa.ex");
81 List.iter (generate st) (R.get_list unm_or "xoa.or");
82 List.iter (generate st) (R.get_list unm_and "xoa.and");
86 if !separate then process_distributed conf else process_centralized conf
89 let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
90 let help_X = " Clear configuration" in
91 let help_s = " Generate separate objects" in
92 let help_u = " Update existing separate files" in
94 "-X", Arg.Unit clear, help_X;
95 "-s", Arg.Set separate, help_s;
96 "-u", Arg.Clear incremental, help_u;