1structure HM_Cline :> HM_Cline =
2struct
3
4type t = {
5  core : HM_Core_Cline.t,
6  mosmldir : string option,
7  no_basis2002 : bool
8}
9
10local
11  open FunctionalRecordUpdate
12  fun makeUpdateT z = makeUpdate3 z
13in
14fun updateT z = let
15  fun from  core mosmldir no_basis2002 =
16    {
17      no_basis2002 = no_basis2002, mosmldir = mosmldir, core = core
18    }
19  fun from' no_basis2002 mosmldir core =
20    {
21      no_basis2002 = no_basis2002, mosmldir = mosmldir, core = core
22    }
23  fun to f {core, mosmldir, no_basis2002} =
24    f core mosmldir no_basis2002
25in
26  makeUpdateT (from, from', to)
27end z
28val U = U
29val $$ = $$
30end (* local *)
31
32
33val default_options = {
34  no_basis2002 = false,
35  mosmldir = NONE,
36  core = HM_Core_Cline.fupd_jobs (fn _ => 1) HM_Core_Cline.default_core_options
37}
38fun fupd_core f t = updateT t (U #core (f (#core t))) $$
39
40(* this fupdcore function is used internally to build command-line options *)
41fun fupdcore f x =
42  let
43    val {update = u, hmakefile, no_hmf} = f x
44  in
45    {update = fn (wn, t : t) => updateT t (U #core (u (wn, #core t))) $$,
46     hmakefile = hmakefile, no_hmf = no_hmf}
47  end
48
49open GetOpt
50type core_t = HM_Core_Cline.t
51type 'a cline_result = 'a HM_Core_Cline.cline_result
52type 'a arg_descr = 'a GetOpt.arg_descr
53
54fun resfn f : t cline_result = {update = f, hmakefile = NONE, no_hmf = false}
55
56fun set_mosmldir s =
57  resfn (fn (wn, t : t) =>
58            (if isSome (#mosmldir t) then
59               wn ("Moscow ML dir already set; ignoring earlier spec")
60             else ();
61             updateT t (U #mosmldir (SOME s)) $$))
62val mosml_option_descriptions = [
63  {help = "don't use HOL's provided basis 2002", long = ["no_basis2002"],
64   short = "",
65   desc = NoArg (fn () =>
66                    resfn (fn (wn,t) => updateT t (U #no_basis2002 true) $$))},
67  {help = "specify Moscow ML's base directory", long = ["mosmldir"],
68   short = "",
69   desc = ReqArg (set_mosmldir, "directory")}
70]
71
72type core_t = HM_Core_Cline.t
73
74fun mapd (d : core_t cline_result arg_descr) : t cline_result arg_descr =
75  case d of
76      NoArg f => NoArg(fupdcore f)
77    | ReqArg (f, s) => ReqArg (fupdcore f, s)
78    | OptArg (f, s) => OptArg (fupdcore f, s)
79
80
81val option_descriptions =
82    HM_Core_Cline.sort_descriptions
83      (map (fn {desc,help,short,long} =>
84               {desc = mapd desc, help = help, long = long, short = short})
85           HM_Core_Cline.core_option_descriptions @
86       mosml_option_descriptions)
87
88end
89