/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holdep.sml | 21 fun errMsg str = TextIO.output(TextIO.stdErr, str ^ "\n\n") 111 else str c 168 handle e as OS.SysErr (str, _) => (errMsg str; raise e)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCode.sml | 438 val str : string = value 441 PrettyString str 446 val str : string = value 449 PrettyString str 454 val str : string = value 457 PrettyString str 462 val str : string = value 465 PrettyString str 470 val str = "INDIRECT(" ^ Int.toString offset ^ ", "; value 473 [ PrettyString str, prett 630 val str = "INDIRECTCONTAINER(" ^ Int.toString offset ^ ", "; value [all...] |
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | scan.scala | 331 private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = 333 val len = str.length 337 tree.branches.get(str.charAt(i)) match { 347 def completions(str: CharSequence): List[String] = 348 lookup(str) match { 349 case Some((true, tree)) => dest(tree, List(str.toString))
|
H A D | bytes.scala | 24 val str = s.toString 25 if (str.isEmpty) empty 27 val b = UTF8.bytes(str)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | scan.scala | 331 private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = 333 val len = str.length 337 tree.branches.get(str.charAt(i)) match { 347 def completions(str: CharSequence): List[String] = 348 lookup(str) match { 349 case Some((true, tree)) => dest(tree, List(str.toString))
|
H A D | bytes.scala | 24 val str = s.toString 25 if (str.isEmpty) empty 27 val b = UTF8.bytes(str)
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Help.sml | 57 dir ^ str slash ^ file 111 fun instr s str = 115 String.sub (s, j) = Char.toLower (String.sub (str, k)) andalso eq (j+1) (k+1) 116 val stop = String.size str - len 119 fun occurshere str = 122 | SOME s => instr s str
|
/seL4-l4v-master/HOL4/examples/acl2/lisp/ |
H A D | a2ml.lisp | 155 (defun set-cbd-fn-state (str state) 157 (set-cbd-fn str state) 162 str))
|
/seL4-l4v-master/l4v/misc/regression/ |
H A D | testspec.py | 61 parse_attr("cwd", "cwd", str) 142 + str(dtd.error_log)) 334 parser.add_argument("file", metavar="FILE", type=str, nargs="*",
|
/seL4-l4v-master/seL4/src/machine/ |
H A D | io.c | 600 word_t ksnprintf(char *str, word_t size, const char *format, ...) argument 605 out_wrap_t out = { buf_out_fn, str, 0, size }; 615 str[i] = 0;
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | IRSyntax.sml | 476 format_exp (hd sList) ^ itlist (curry (fn (exp,str) => "," ^ format_exp exp ^ str)) (tl sList) "" ^ 480 format_exp (hd dList) ^ itlist (curry (fn (exp,str) => "," ^ format_exp exp ^ str)) (tl dList) "" ^ 484 itlist (curry (fn (exp,str) => format_exp exp ^ str)) dList "" ^ " " ^ 487 itlist (curry (fn (exp,str) => " " ^ format_exp exp ^ str)) (tl sList) "");
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | IRSyntax.sml | 468 format_exp (hd sList) ^ itlist (curry (fn (exp,str) => "," ^ format_exp exp ^ str)) (tl sList) "" ^ 472 format_exp (hd dList) ^ itlist (curry (fn (exp,str) => "," ^ format_exp exp ^ str)) (tl dList) "" ^ 476 itlist (curry (fn (exp,str) => format_exp exp ^ str)) dList "" ^ " " ^ 479 itlist (curry (fn (exp,str) => " " ^ format_exp exp ^ str)) (tl sList) "");
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | IRSyntax.sml | 468 format_exp (hd sList) ^ itlist (curry (fn (exp,str) => "," ^ format_exp exp ^ str)) (tl sList) "" ^ 472 format_exp (hd dList) ^ itlist (curry (fn (exp,str) => "," ^ format_exp exp ^ str)) (tl dList) "" ^ 476 itlist (curry (fn (exp,str) => format_exp exp ^ str)) dList "" ^ " " ^ 479 itlist (curry (fn (exp,str) => " " ^ format_exp exp ^ str)) (tl sList) "");
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/examples/ |
H A D | fc_examples.sml | 90 1: str r0, [sp] 100 11: str r0, [sp]
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | sexpScript.sml | 96 val _ = declare_names ("ACL2_STRING", "str"); 159 `(stringp(str x) = t) /\ (stringp _ = nil)`; 680 (sexp_size (str a) = 1) /\ 728 `(coerce (str s) y = 731 else str "") 736 else str(coerce_list_to_string(make_character_list(cons a x)))) 738 (coerce _ y = if y = sym "COMMON-LISP" "LIST" then nil else str "")`; 1152 `(symbol_name (sym p n) = ite (symbolp (sym p n)) (str n) (str "")) 1154 (symbol_name _ = (str ""))`; [all...] |
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | elfexport.h | 115 unsigned long makeStringTableEntry(const char *str, ExportStringTable *stab);
|
H A D | run_time.cpp | 233 void raiseExceptionStringWithLocation(TaskData *taskData, int id, const char *str, const char *file, int line) argument 236 raise_exception(taskData, id, SAVE(C_string_to_Poly(taskData, str)), file, line); 267 void raiseExceptionFailWithLocation(TaskData *taskData, const char *str, const char *file, int line) argument 269 raiseExceptionStringWithLocation(taskData, EXC_Fail, str, file, line);
|
/seL4-l4v-master/isabelle/src/Pure/ML/ |
H A D | ml_lex.scala | 96 private val str = 106 "#\"" ~ str ~ "\"" ^^ { case x ~ y ~ z => Token(Kind.CHAR, x + y + z) } 109 "#\"" ~ opt(str) ^^ { case x ~ Some(y) => x + y case x ~ None => x } 115 rep(gap | str) ^^ (_.mkString)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | export_codeLib.sml | 67 val str = if ty = ``:word8`` then "\t.byte\t" else value 72 in str ^ foo tms end
|
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/ |
H A D | export_codeLib.sml | 56 val str = if ty = ``:word8`` then "\t.byte\t" else value 61 in str ^ foo tms end
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | export_codeLib.sml | 55 val str = if ty = ``:word8`` then "\t.byte\t" else value 60 in str ^ foo tms end
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfoot.lex | 28 List.foldl (fn ((str, tok), t) => Binarymap.insert (t, str, tok))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/ |
H A D | ml_lex.scala | 96 private val str = 106 "#\"" ~ str ~ "\"" ^^ { case x ~ y ~ z => Token(Kind.CHAR, x + y + z) } 109 "#\"" ~ opt(str) ^^ { case x ~ Some(y) => x + y case x ~ None => x } 115 rep(gap | str) ^^ (_.mkString)
|
/seL4-l4v-master/graph-refine/ |
H A D | target_objects.py | 77 tracer[0](str (s), push)
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | rich_text_area.scala | 399 val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str 425 val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset) 432 val s1 = str.substring(0, i) 433 val s2 = str.substring(i, j) 434 val s3 = str.substring(j) 445 gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y) 448 gfx.drawString(Word.bidi_override(str), x1, y) 450 x1 += string_width(str)
|