/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | HM_Core_Cline.sml | 12 no_prereqs opentheory quiet 23 quiet = quiet, quit_on_failure = quit_on_failure, 28 quiet opentheory 42 quiet = quiet, quit_on_failure = quit_on_failure, 50 quiet, quit_on_failure, rebuild_deps, recursive_build, 55 no_prereqs opentheory quiet 84 quiet : bool, 110 quiet [all...] |
H A D | HM_Core_Cline.sig | 20 quiet : bool,
|
H A D | HM_GraphBuildJ1.sig | 35 quiet : bool,
|
H A D | Systeml.sig | 43 (and it won't be quiet). *)
|
H A D | HM_GraphBuildJ1.sml | 40 quiet, hmenv, system} = static_info 108 if not noecho andalso not quiet then
|
H A D | Holmake_tools.sig | 74 (* 0 : quiet, 1 : normal, 2 : chatty, 3 : everything + debug info *)
|
/seL4-l4v-master/l4v/tools/haskell-translator/ |
H A D | pars_skl.py | 29 quiet = True variable 32 quiet = False variable 118 if not quiet: 132 if bad_type_assignment and not quiet:
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | selftest.sml | 16 val quiet = true; value 24 val quiet = true 29 val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) []));
|
/seL4-l4v-master/HOL4/tools/trailing-wspace/ |
H A D | trailingwspace.sml | 156 datatype cline_record = CR of { quiet : bool, action : action, help : bool} 157 val init = CR {quiet = false, action = Fix, help = false} 159 CR {action = action, quiet = b, help = help} 160 fun act_upd a (CR {quiet, help, ...}) = 161 CR {action = a, quiet = quiet, help = help} 162 fun help_upd b (CR{quiet, action, ...}) = 163 CR {action = action, quiet = quiet, help = b} 169 {short = "q", long = ["quiet"], des [all...] |
/seL4-l4v-master/isabelle/src/HOL/Mirabelle/lib/scripts/ |
H A D | mirabelle.pl | 153 my $quiet = ""; 156 $quiet = " > /dev/null 2>&1"; 166 "-l $mirabelle_logic" . $quiet;
|
/seL4-l4v-master/l4v/isabelle/src/HOL/Mirabelle/lib/scripts/ |
H A D | mirabelle.pl | 153 my $quiet = ""; 156 $quiet = " > /dev/null 2>&1"; 166 "-l $mirabelle_logic" . $quiet;
|
/seL4-l4v-master/l4v/spec/ |
H A D | Makefile | 54 git diff --no-ext-diff --quiet || echo "*" >> $@ 55 git diff --no-ext-diff --quiet --cached || echo "+" >> $@
|
/seL4-l4v-master/HOL4/src/q/ |
H A D | selftest.sml | 371 val _ = tprint "(Interactive) PAT_ASSUM quiet about tyvar guesses(1)" 384 val _ = tprint "(Interactive) PAT_ASSUM quiet about tyvar guesses(2)" 390 val _ = tprint "(Interactive) PAT_ASSUM quiet about tyvar guesses(3)" 396 val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(1)" 401 val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(2)" 405 val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(3)" 409 val _ = tprint "(Interactive) RENAME_TAC quiet about tyvar guesses(4)"
|
/seL4-l4v-master/HOL4/tools/set_mtime/ |
H A D | set_mtime.sml | 13 \ -q Make output quiet\n\n\
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/poly/ |
H A D | holfoot_command_line.sml | 18 val s = " -q quiet mode, verify specifications automatically and\n\ 246 val (quiet, args) = (true, Lib.snd (Lib.pluck (fn x => x = "-q") args)) value 291 (not quiet) (not quiet) file (SOME [generate_vcs]) []; 294 if quiet then () else print "\n\n\n"
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/ |
H A D | selftest.sml | 26 val quiet = false; value
|
/seL4-l4v-master/HOL4/src/quantHeuristics/ |
H A D | selftest.sml | 9 val quiet = false; 31 val quiet = false; value
|
/seL4-l4v-master/HOL4/tools/Holmake/mosml/ |
H A D | BuildCommand.sml | 44 val quiet_flag = #quiet (#core optv) 194 quiet = quiet_flag,
|
/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | BuildCommand.sml | 228 val quiet_flag = #quiet (#core optv) 468 quiet = quiet_flag, 482 quiet = quiet_flag, hmenv = hmenv,
|
H A D | multibuild.sml | 28 keep_going, quiet, hmenv, jobs, info, time_limit,
|
/seL4-l4v-master/HOL4/developers/ |
H A D | poly-prehol.sml | 106 Switch in and out of quiet mode
|
/seL4-l4v-master/graph-refine/ |
H A D | stack_logic.py | 1185 def compute_stack_bounds (quiet = False): 1187 if quiet: 1200 if quiet: 1204 if quiet: 1224 quiet = True): 1248 stack_bounds = compute_stack_bounds (quiet = quiet)
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | selftest.sml | 10 val quiet = false; value 18 val quiet = false; 28 val _ = print (if quiet then "" else "Testing "^s^" "); 40 val quiet = quiet andalso ok value 48 val _ = if quiet then () else print ("\n "); 50 val _ = if quiet then () else
|
H A D | patternMatchesSyntax.sig | 215 (* Like [prove], but quiet in case it fails. This is useful,
|
/seL4-l4v-master/HOL4/tools/unicode-grep/ |
H A D | ugrep.sml | 263 {help = "be less chatty", long = ["quiet"], short = "q",
|