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 separate = ref false
25 Scanf.sscanf s "%u %u" A.mk_exists
28 Scanf.sscanf s "%u" A.mk_or
31 Scanf.sscanf s "%u" A.mk_and
33 let process_centralized conf =
34 let preamble = L.get_preamble conf in
35 if R.has "xoa.objects" && R.has "xoa.notations" then begin
36 let ooch = L.open_out preamble (R.get_string "xoa.objects") in
37 let noch = L.open_out preamble (R.get_string "xoa.notations") in
38 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
39 L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");
40 List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
41 List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
42 List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
43 close_out noch; close_out ooch
46 let generate (p, o, n) = function
47 | A.Exists (c, v) as d ->
48 let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
49 let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
50 let ooch = L.open_out p oname in
51 let noch = L.open_out p nname in
52 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
53 L.out_include ooch (nname ^ ".ma");
54 E.generate ooch noch d;
55 close_out noch; close_out ooch
59 let process_distributed conf =
60 let preamble = L.get_preamble conf in
61 if R.has "xoa.objects" && R.has "xoa.notations" then begin
62 let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
63 List.iter (generate st) (R.get_list unm_ex "xoa.ex");
64 List.iter (generate st) (R.get_list unm_or "xoa.or");
65 List.iter (generate st) (R.get_list unm_and "xoa.and");
69 if !separate then process_distributed conf else process_centralized conf
72 let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
73 let help_X = " Clear configuration" in
74 let help_s = " Generate separate objects" in
76 "-X", Arg.Unit clear, help_X;
77 "-s", Arg.Set separate, help_s;