/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | getopts.scala | 36 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 D | options.scala | 86 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 D | getopts.scala | 36 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 D | options.scala | 86 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 D | pprint-file.csh | 5 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 D | jedit_options.scala | 56 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 D | isabelle_options.scala | 50 (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 D | jedit_spell_checker.scala | 88 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 D | jedit_options.scala | 56 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 D | isabelle_options.scala | 50 (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 D | jedit_spell_checker.scala | 88 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 D | spec_databaseLib.sml | 10 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 D | spec_databaseLib.sig | 3 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 D | get_tool_prefix.sh | 3 TC=$(find ../.. /opt -maxdepth 2 -name 'toolchain*' 2> /dev/null )
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/ |
H A D | cmdline.c | 36 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 D | arm_evalScript.sml | 595 `(!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 D | arm8_decompLib.sml | 40 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 D | ObsCongrLib.sml | 61 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 D | WeakEQLib.sml | 60 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 D | Options.sig | 21 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 D | Options.sig | 21 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 D | armLib.sml | 82 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 D | regexTest.sml | 26 (* /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 D | selftest.sml | 3 (* /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 D | arm_decompLib.sml | 49 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
|