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