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