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
27 Scanf.sscanf s "%u %u" A.mk_exists
30 Scanf.sscanf s "%u" A.mk_or
33 Scanf.sscanf s "%u" A.mk_and
35 let process_centralized conf =
36 let preamble = L.get_preamble conf in
37 if R.has "xoa.objects" && R.has "xoa.notations" then begin
38 let ooch = L.open_out preamble (R.get_string "xoa.objects") in
39 let noch = L.open_out preamble (R.get_string "xoa.notations") in
40 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
41 L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");
42 List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
43 List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
44 List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
45 close_out noch; close_out ooch
48 let generate (p, o, n) d =
49 let oname, nname = match d with
51 let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
52 let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
55 let oname = Printf.sprintf "%s/or_%u" o c in
56 let nname = Printf.sprintf "%s/or_%u" n c in
59 let oname = Printf.sprintf "%s/and_%u" o c in
60 let nname = Printf.sprintf "%s/and_%u" n c in
63 if !incremental && L.exists_out oname && L.exists_out nname then () else
65 let ooch = L.open_out p oname in
66 let noch = L.open_out p nname in
67 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
68 L.out_include ooch (nname ^ ".ma");
69 E.generate ooch noch d;
70 close_out noch; close_out ooch
73 let process_distributed conf =
74 let preamble = L.get_preamble conf in
75 if R.has "xoa.objects" && R.has "xoa.notations" then begin
76 let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
77 List.iter (generate st) (R.get_list unm_ex "xoa.ex");
78 List.iter (generate st) (R.get_list unm_or "xoa.or");
79 List.iter (generate st) (R.get_list unm_and "xoa.and");
83 if !separate then process_distributed conf else process_centralized conf
86 let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
87 let help_X = " Clear configuration" in
88 let help_s = " Generate separate objects" in
89 let help_u = " Update existing separate files" in
91 "-X", Arg.Unit clear, help_X;
92 "-s", Arg.Set separate, help_s;
93 "-u", Arg.Clear incremental, help_u;