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_______________________________________________________________ *)
16 module R = Helm_registry
25 let help_O = "<dir> Set this output directory"
26 let help_X = " Clear configuration and options"
27 let help_a = " Log alpha-unconverted identifiers (default: no)"
28 let help_g = " Global alpha-conversion (default: no)"
29 let help_l = "<file> Output the list of generated files in this file"
30 let help_m = " Log missing notational macros (default: no)"
31 let help_p = " Omit types (default: no)"
32 let help_t = " Test term transformations (default: no)"
36 (* internal functions *******************************************************)
38 let alpha_decode = R.triple R.string R.string R.string
40 let const_decode = R.pair R.string R.string
42 let macro_decode = R.triple R.string R.string R.int
46 if !G.no_init then begin
50 G.alpha_type := R.get_list alpha_decode "matex.alpha.type";
51 G.alpha_sort := R.get_list alpha_decode "matex.alpha.sort";
52 G.alpha_gref := R.get_list const_decode "matex.alpha.gref";
53 G.macro_gref := R.get_list macro_decode "matex.notation.const"
56 F.check_suffix s ".conf.xml"
59 failwith "MaTeX: main: registry not initialized"
62 failwith ("MaTeX: main: malformed argument: " ^ s)
65 let file = F.concat !G.out_dir fname in
66 G.close_list (); G.list_och := Some (open_out file)
69 if is_registry s then init s
70 else if !G.no_init then no_init ()
71 else if L.is_uri s then E.process (U.uri_of_string s)
77 "-O", A.String ((:=) G.out_dir), help_O;
78 "-X", A.Unit G.clear, help_X;
79 "-a", A.Set G.log_alpha, help_a;
80 "-g", A.Set G.global_alpha, help_g;
81 "-l", A.String set_list, help_l;
82 "-m", A.Set G.log_missing, help_m;
83 "-p", A.Set G.no_types, help_p;
84 "-t", A.Set G.test, help_t;
87 | X.Error s -> X.log s