1structure HM_Core_Cline :> HM_Core_Cline =
2struct
3
4local
5  open FunctionalRecordUpdate
6  fun makeUpdateT z = makeUpdate22 z
7in
8fun updateT z = let
9  fun from debug do_logging dontmakes fast help hmakefile holdir includes
10           interactive jobs keep_going no_action no_hmakefile no_lastmaker_check
11           no_overlay
12           no_prereqs opentheory quiet
13           quit_on_failure rebuild_deps recursive verbose =
14    {
15      debug = debug, do_logging = do_logging, dontmakes = dontmakes,
16      fast = fast, help = help, hmakefile = hmakefile, holdir = holdir,
17      includes = includes, interactive = interactive, jobs = jobs,
18      keep_going = keep_going,
19      no_action = no_action, no_hmakefile = no_hmakefile,
20      no_lastmaker_check = no_lastmaker_check, no_overlay = no_overlay,
21      no_prereqs = no_prereqs, opentheory = opentheory,
22      quiet = quiet, quit_on_failure = quit_on_failure,
23      rebuild_deps = rebuild_deps, recursive = recursive, verbose = verbose
24    }
25  fun from' verbose recursive rebuild_deps quit_on_failure quiet opentheory
26            no_prereqs
27            no_overlay no_lastmaker_check no_hmakefile no_action keep_going
28            jobs interactive
29            includes holdir
30            hmakefile help fast dontmakes do_logging debug =
31    {
32      debug = debug, do_logging = do_logging, dontmakes = dontmakes,
33      fast = fast, help = help, hmakefile = hmakefile, holdir = holdir,
34      includes = includes, interactive = interactive, jobs = jobs,
35      keep_going = keep_going,
36      no_action = no_action, no_hmakefile = no_hmakefile,
37      no_lastmaker_check = no_lastmaker_check, no_overlay = no_overlay,
38      no_prereqs = no_prereqs, opentheory = opentheory,
39      quiet = quiet, quit_on_failure = quit_on_failure,
40      rebuild_deps = rebuild_deps, recursive = recursive, verbose = verbose
41    }
42  fun to f {debug, do_logging, dontmakes, fast, help, hmakefile, holdir,
43            includes, interactive, jobs, keep_going, no_action, no_hmakefile,
44            no_lastmaker_check,
45            no_overlay, no_prereqs, opentheory,
46            quiet, quit_on_failure, rebuild_deps, recursive, verbose} =
47    f debug do_logging dontmakes fast help hmakefile holdir includes
48      interactive jobs keep_going no_action no_hmakefile no_lastmaker_check
49      no_overlay
50      no_prereqs opentheory quiet
51      quit_on_failure rebuild_deps recursive verbose
52in
53  makeUpdateT (from, from', to)
54end z
55val U = U
56val $$ = $$
57end (* local *)
58
59fun fupd_jobs f t = updateT t (U #jobs (f (#jobs t))) $$
60fun fupd_includes f t = updateT t (U #includes (f (#includes t))) $$
61
62type t = {
63  debug : bool,
64  do_logging : bool,
65  dontmakes : string list,
66  fast : bool,
67  help : bool,
68  hmakefile : string option,
69  holdir : string option,
70  includes : string list,
71  interactive : bool,
72  jobs : int,
73  keep_going : bool,
74  no_action : bool,
75  no_hmakefile : bool,
76  no_lastmaker_check : bool,
77  no_overlay : bool,
78  no_prereqs : bool,
79  opentheory : string option,
80  quiet : bool,
81  quit_on_failure : bool,
82  rebuild_deps : bool,
83  recursive : bool,
84  verbose : bool
85}
86
87val default_core_options : t =
88{
89  debug = false,
90  do_logging = false,
91  dontmakes = [],
92  fast = false,
93  help = false,
94  hmakefile = NONE,
95  holdir = NONE,
96  includes = [],
97  interactive = false,
98  jobs = 4,
99  keep_going = false,
100  no_action = false,
101  no_hmakefile = false,
102  no_lastmaker_check = false,
103  no_overlay = false,
104  no_prereqs = false,
105  opentheory = NONE,
106  quiet = false,
107  quit_on_failure = true,
108  rebuild_deps = false,
109  recursive = false,
110  verbose = false
111}
112
113type 'a cline_result =
114     { update: (string -> unit) * 'a -> 'a,
115       hmakefile : string option,
116       no_hmf : bool }
117
118fun resfn f : t cline_result = {update = f, hmakefile = NONE, no_hmf = false}
119
120open GetOpt
121val setNOHMF =
122    NoArg (fn () => {update = fn (wn,t) => updateT t (U #no_hmakefile true) $$,
123                     hmakefile = NONE, no_hmf = true})
124fun mkBoolT sel =
125  NoArg (fn () => resfn (fn (wn,t) => updateT t (U sel true) $$))
126fun mkBoolF sel =
127  NoArg (fn () => resfn (fn (wn,t) => updateT t (U sel false) $$))
128fun cons_dontmakes x =
129  resfn (fn (wn,t) => updateT t (U #dontmakes (x :: #dontmakes t)) $$)
130fun cons_includes x =
131  resfn (fn (wn,t) => updateT t (U #includes (x :: #includes t)) $$)
132fun change_jobs nstr =
133  resfn (fn (wn,t) =>
134            case Int.fromString nstr of
135                NONE => (wn ("Couldn't parse "^nstr^
136                             " as a number; ignoring it"); t)
137              | SOME n => if n < 1 then
138                            (wn "Ignoring non-positive job count"; t)
139                          else updateT t (U #jobs n) $$)
140
141fun set_hmakefile s =
142  { update = fn (wn,t) =>
143                (if isSome (#hmakefile t) then
144                   wn "Multiple Holmakefile specs; ignoring earlier spec"
145                 else ();
146                 updateT t (U #hmakefile (SOME s)) $$),
147    hmakefile = SOME s, no_hmf = false }
148fun set_holdir s =
149  resfn (fn (wn, t) =>
150            (if isSome (#holdir t) then
151               wn "Multiple holdir specs; ignoring earlier spec"
152             else ();
153             updateT t (U #holdir (SOME s)) $$))
154fun set_openthy s =
155  resfn (fn (wn, t) =>
156            (if isSome (#opentheory t) then
157               wn "Multiple opentheory specs; ignoring earlier spec"
158             else ();
159             updateT t (U #opentheory (SOME s)) $$))
160val core_option_descriptions = [
161  { help = "turn on diagnostic messages", long = ["dbg", "d"], short = "",
162    desc = mkBoolT #debug},
163  { help = "don't make this target", long = [], short = "d",
164    desc = ReqArg (cons_dontmakes, "target") },
165  { help = "fast build (replace tactics w/cheat)", long = ["fast"], short = "",
166    desc = mkBoolT #fast },
167  { help = "show this message", long = ["help"], short = "h",
168    desc = mkBoolT #help },
169  { help = "use different HOLDIR", long = ["holdir"], short = "",
170    desc = ReqArg (set_holdir, "directory") },
171  { help = "use different holmakefile", long = ["holmakefile"], short = "",
172    desc = ReqArg (set_hmakefile, "file") },
173  { help = "make session 'interactive'", long = ["interactive"], short = "i",
174    desc = mkBoolT #interactive },
175  { help = "include directory", long = [], short = "I",
176    desc = ReqArg (cons_includes, "directory") },
177  { help = "max number of parallel jobs", long = ["jobs"], short = "j",
178    desc = ReqArg (change_jobs, "n") },
179  { help = "try to build all targets", long = ["keep-going"], short = "k",
180    desc = mkBoolT #keep_going },
181  { help = "enable time logging", long = ["logging"], short = "",
182    desc = mkBoolT #do_logging },
183  { help = "print what would be executed", long = ["no_action"], short = "n",
184    desc = mkBoolT #no_action },
185  { help = "don't use a Holmakefile", long = ["no_hmakefile"], short = "",
186    desc = setNOHMF },
187  { help = "don't check which Holmake was last used", long = ["nolmbc"],
188    short = "", desc = mkBoolT #no_lastmaker_check },
189  { help = "don't use Overlay.sml file", long = ["no_overlay"],
190    short = "", desc = mkBoolT #no_overlay },
191  { help = "don't build recursively in INCLUDES",
192    long = ["no_prereqs"], short = "", desc = mkBoolT #no_prereqs },
193  { help = "don't quit on failure", long = ["noqof"], short = "",
194    desc = mkBoolF #quit_on_failure },
195  { help = "use file as opentheory logging .uo",
196    long = ["ot"], short = "", desc = ReqArg (set_openthy, "file")},
197  { help = "be quieter with output", short = "q", long = ["quiet"],
198    desc = NoArg
199             (fn () =>
200                 resfn (fn (wn,t) =>
201                           (if #verbose t then
202                              wn "Quiet and verbose incompatible; \
203                                 \taking verbose"
204                            else () ;
205                            updateT t (U #quiet true) $$))) },
206  { help = "quit on failure", short = "", long = ["qof"],
207    desc = mkBoolT #quit_on_failure },
208  { help = "rebuild cached dependency files", short = "",
209    long = ["rebuild_deps"], desc = mkBoolT #rebuild_deps },
210  { help = "clean recursively", short = "r", long = [],
211    desc = mkBoolT #recursive },
212  { help = "verbose output", short = "v", long = ["verbose"],
213    desc = NoArg
214             (fn () =>
215                 resfn (fn (wn,t) =>
216                           (if #quiet t then
217                              wn "Quiet and verbose incompatible; \
218                                 \taking verbose"
219                            else ();
220                            updateT t (U #verbose true) $$))) }
221]
222
223fun descr_key (d:'a GetOpt.opt_descr) =
224  str (String.sub(#short d, 0))
225  handle Subscript => hd (#long d) handle Empty => ""
226
227fun descr_compare (d1, d2) = String.compare(descr_key d1, descr_key d2)
228
229fun sort_descriptions dl = Listsort.sort descr_compare dl
230
231
232end
233