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) = function
49 | A.Exists (c, v) as d ->
50 let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
51 let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
52 if !incremental && L.exists_out oname && L.exists_out nname then () else
54 let ooch = L.open_out p oname in
55 let noch = L.open_out p nname in
56 List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
57 L.out_include ooch (nname ^ ".ma");
58 E.generate ooch noch d;
59 close_out noch; close_out ooch
64 let process_distributed conf =
65 let preamble = L.get_preamble conf in
66 if R.has "xoa.objects" && R.has "xoa.notations" then begin
67 let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
68 List.iter (generate st) (R.get_list unm_ex "xoa.ex");
69 List.iter (generate st) (R.get_list unm_or "xoa.or");
70 List.iter (generate st) (R.get_list unm_and "xoa.and");
74 if !separate then process_distributed conf else process_centralized conf
77 let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
78 let help_X = " Clear configuration" in
79 let help_s = " Generate separate objects" in
80 let help_u = " Update existing separate files" in
82 "-X", Arg.Unit clear, help_X;
83 "-s", Arg.Set separate, help_s;
84 "-u", Arg.Clear incremental, help_u;