Searched refs:opt (Results 1 - 25 of 109) sorted by relevance

12345

/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Dgetopts.scala36 private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
37 private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
38 private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
39 private def print_option(opt: Char): String = quote("-" + opt
[all...]
H A Doptions.scala86 opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
100 opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
206 private def print_opt(opt: Options.Opt): String =
207 if (opt.public) "public " + opt.print else opt.print
218 case Some(opt) if !opt.unknown => opt
224 val opt
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Dgetopts.scala36 private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
37 private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
38 private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
39 private def print_option(opt: Char): String = quote("-" + opt
[all...]
H A Doptions.scala86 opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
100 opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
206 private def print_opt(opt: Options.Opt): String =
207 if (opt.public) "public " + opt.print else opt.print
218 case Some(opt) if !opt.unknown => opt
224 val opt
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/obsolete/
H A Dpprint-file.csh5 set opt = ""
8 set opt = nil
22 if ($opt != "") then
28 echo '(pprint-file' '"'$infile'"' '"'$outfile'"' $opt ')' >> $tmpfile
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Djedit_options.scala56 def make_color_component(opt: Options.Opt): Option_Component =
60 val opt_name = opt.name
61 val opt_title = opt.title("jedit")
63 val button = new ColorWellButton(Color_Value(opt.value))
71 component.tooltip = GUI.tooltip_lines(opt.print_default)
75 def make_component(opt: Options.Opt): Option_Component =
79 val opt_name = opt.name
80 val opt_title = opt.title("jedit")
83 if (opt.typ == Options.Bool)
119 component.tooltip = GUI.tooltip_lines(opt
[all...]
H A Disabelle_options.scala50 (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
58 (name, opt) <- PIDE.options.value.options.toList
59 if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
60 } yield PIDE.options.make_color_component(opt))
H A Djedit_spell_checker.scala88 val opt = PIDE.options.value.check_name(option_name)
93 val title = opt.title()
106 component.tooltip = GUI.tooltip_lines(opt.print_default)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_options.scala56 def make_color_component(opt: Options.Opt): Option_Component =
60 val opt_name = opt.name
61 val opt_title = opt.title("jedit")
63 val button = new ColorWellButton(Color_Value(opt.value))
71 component.tooltip = GUI.tooltip_lines(opt.print_default)
75 def make_component(opt: Options.Opt): Option_Component =
79 val opt_name = opt.name
80 val opt_title = opt.title("jedit")
83 if (opt.typ == Options.Bool)
119 component.tooltip = GUI.tooltip_lines(opt
[all...]
H A Disabelle_options.scala50 (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
58 (name, opt) <- PIDE.options.value.options.toList
59 if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
60 } yield PIDE.options.make_color_component(opt))
H A Djedit_spell_checker.scala88 val opt = PIDE.options.value.check_name(option_name)
93 val title = opt.title()
106 component.tooltip = GUI.tooltip_lines(opt.print_default)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A Dspec_databaseLib.sml10 datatype ''opt entry = Pending of thm * term | Built of (''opt list * thm) list
19 The type ''opt represents configuration options.
21 - basic_opt : unit -> ''opt
35 - closeness : ''opt -> ''opt -> int
55 fun mk_spec_database basic_opt (default_opt: ''opt) proj_opt closeness
59 fun set_current_opt opt = current_opt := opt
61 val db = ref (LVTermNet.empty: (''opt entr
106 val opt = !current_opt value
120 val opt = !current_opt value
[all...]
H A Dspec_databaseLib.sig3 datatype ''opt entry = Pending of Thm.thm * Term.term
4 | Built of (''opt list * Thm.thm) list
/seL4-l4v-10.1.1/graph-refine/seL4-example/
H A Dget_tool_prefix.sh3 TC=$(find ../.. /opt -maxdepth 2 -name 'toolchain*' 2> /dev/null )
/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/
H A Dcmdline.c36 static int UNUSED parse_opt(const char *cmdline, const char *opt, char *value, int bufsize) argument
47 for (optptr = opt; *optptr && *cmdline && (*cmdline != '=') && !is_space(*cmdline) && (*optptr == *cmdline); optptr++, cmdline++);
65 static int parse_bool(const char *cmdline, const char *opt) argument
75 for (optptr = opt; *optptr && *cmdline && !is_space(*cmdline) && (*optptr == *cmdline); optptr++, cmdline++);
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A Darm_evalScript.sml595 `(!cond b opt rd rn offset.
596 DECODE_ARM (enc (instruction$LDR cond b opt rd rn offset)) = ldr_str) /\
597 (!cond b opt rd rn offset.
598 DECODE_ARM (enc (instruction$STR cond b opt rd rn offset)) = ldr_str)`,
604 `(!cond s h opt rd rn offset.
605 DECODE_ARM (enc (instruction$LDRH cond s h opt rd rn offset)) =
607 (!cond opt rd rn offset.
608 DECODE_ARM (enc (instruction$STRH cond opt rd rn offset)) = ldrh_strh)`,
615 `(!cond s opt rn list.
616 DECODE_ARM (enc (instruction$LDM cond s opt r
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/decompiler/
H A Darm8_decompLib.sml40 fun arm8_tools_opt opt = gen_arm8_tools (arm8_spec_opt opt)
51 fun gen_arm8_decompile iscode tools opt name (qcode: string quotation) =
57 arm8_progLib.arm8_config ("no-newline," ^ opt)
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DObsCongrLib.sml61 val (opt, t1, t2) = args_equiv w value
63 if (opt = ``OBS_CONGR``) then
79 val (opt, t1, t2) = args_equiv w value
81 if (opt = ``OBS_CONGR``) then
H A DWeakEQLib.sml60 val (opt, t1, t2) = args_equiv w value
62 if (opt = ``WEAK_EQUIV``) then
78 val (opt, t1, t2) = args_equiv w value
80 if (opt = ``WEAK_EQUIV``) then
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DOptions.sig21 type opt = type
55 val basicOptions : opt list
63 footer : string, options : opt list}
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DOptions.sig21 type opt = type
55 val basicOptions : opt list
63 footer : string, options : opt list}
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A DarmLib.sml82 fun print_progress x c opt opc =
84 of NONE => arm_step opt opc
92 Lib.real_time (arm_step opt) opc
94 arm_step opt opc
156 fun arm_steps_from f opt qs =
157 arm_steps_from_parse opt (Lib.mk_set (List.map snd (fst (f qs))));
170 fun decode_opcode opt opc =
171 case opt
192 fun decode_from_string opt s =
193 let val tm = decode_opcode opt (Arbnu
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/test/
H A DregexTest.sml26 (* /opt/hol_bir/examples/PSL/regexp/test *)
27 (* /opt/hol_bir/src/tfl/examples/regexp.{naive/deriv} - in the end *)
28 (* /opt/hol_bir/examples/formal-languages/regular/test.{ml/hol} *)
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/
H A Dselftest.sml3 (* /opt/hol_bir/examples/formal-languages/context-free/selftest.sml *)
4 (* /opt/hol_bir/examples/separationLogic/src/holfoot/selftest.sml *)
6 (* also look at: /opt/hol_bir/src/list/src/selftest.sml *)
8 (* /opt/hol_bir/src/pattern_matches *)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_decompLib.sml49 fun arm_tools_opt opt = arm_tools (l3_arm_spec_opt opt)
61 fun arm_decompile iscode tools opt name (qcode: string quotation) =
67 set_opt opt

Completed in 121 milliseconds

12345