Searched refs:quiet (Results 1 - 25 of 40) sorted by relevance

12

/seL4-l4v-master/HOL4/tools/Holmake/
H A DHM_Core_Cline.sml12 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 DHM_Core_Cline.sig20 quiet : bool,
H A DHM_GraphBuildJ1.sig35 quiet : bool,
H A DSysteml.sig43 (and it won't be quiet). *)
H A DHM_GraphBuildJ1.sml40 quiet, hmenv, system} = static_info
108 if not noecho andalso not quiet then
H A DHolmake_tools.sig74 (* 0 : quiet, 1 : normal, 2 : chatty, 3 : everything + debug info *)
/seL4-l4v-master/l4v/tools/haskell-translator/
H A Dpars_skl.py29 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 Dselftest.sml16 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 Dtrailingwspace.sml156 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 Dmirabelle.pl153 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 Dmirabelle.pl153 my $quiet = "";
156 $quiet = " > /dev/null 2>&1";
166 "-l $mirabelle_logic" . $quiet;
/seL4-l4v-master/l4v/spec/
H A DMakefile54 git diff --no-ext-diff --quiet || echo "*" >> $@
55 git diff --no-ext-diff --quiet --cached || echo "+" >> $@
/seL4-l4v-master/HOL4/src/q/
H A Dselftest.sml371 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 Dset_mtime.sml13 \ -q Make output quiet\n\n\
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/poly/
H A Dholfoot_command_line.sml18 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 Dselftest.sml26 val quiet = false; value
/seL4-l4v-master/HOL4/src/quantHeuristics/
H A Dselftest.sml9 val quiet = false;
31 val quiet = false; value
/seL4-l4v-master/HOL4/tools/Holmake/mosml/
H A DBuildCommand.sml44 val quiet_flag = #quiet (#core optv)
194 quiet = quiet_flag,
/seL4-l4v-master/HOL4/tools/Holmake/poly/
H A DBuildCommand.sml228 val quiet_flag = #quiet (#core optv)
468 quiet = quiet_flag,
482 quiet = quiet_flag, hmenv = hmenv,
H A Dmultibuild.sml28 keep_going, quiet, hmenv, jobs, info, time_limit,
/seL4-l4v-master/HOL4/developers/
H A Dpoly-prehol.sml106 Switch in and out of quiet mode
/seL4-l4v-master/graph-refine/
H A Dstack_logic.py1185 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 Dselftest.sml10 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 DpatternMatchesSyntax.sig215 (* Like [prove], but quiet in case it fails. This is useful,
/seL4-l4v-master/HOL4/tools/unicode-grep/
H A Dugrep.sml263 {help = "be less chatty", long = ["quiet"], short = "q",

Completed in 228 milliseconds

12