/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | join.sml | 27 type result = ParserData.result type 72 type result = ParserData.result type
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | active.scala | 83 case Protocol.Dialog(id, serial, result) => 84 model.session.dialog_result(id, serial, result)
|
H A D | jedit_spell_checker.scala | 39 val result = 48 result match {
|
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | join.sml | 27 type result = ParserData.result type 72 type result = ParserData.result type
|
/seL4-l4v-master/HOL4/src/datatype/record/ |
H A D | RecordType.sig | 20 which modifies a tyinfo in the same way as the result has just been
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | selftest.sml | 110 val result = value 113 if null (hyp result) andalso aconv (rhs (concl result)) boolSyntax.F then 123 val result = SIMP_CONV ss [] t value 125 if aconv (rhs (concl result)) ``(1 + 4 * y) MOD 6`` then OK() 132 val result = SIMP_CONV ss [ASSUME ``0 < n``] t value 134 if aconv (rhs (concl result)) ``5 MOD n`` then OK() 141 val result = SIMP_CONV ss [] t value 143 if aconv (rhs (concl result)) ``(SUC x + 1) MOD 3`` then OK()
|
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_spell_checker.scala | 34 val result = 41 result match {
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_spell_checker.scala | 34 val result = 41 result match {
|
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | export.scala | 123 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = 125 case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) 126 case '*' :: rest => make("[^:/]*" :: result, depth, rest) 127 case '?' :: rest => make("[^:/]" :: result, depth, rest) 128 case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) 129 case '{' :: rest => make("(" :: result, depth + 1, rest) 130 case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) 131 case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) 132 case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) 133 case c :: rest => make(c.toString :: result, dept [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | export.scala | 123 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = 125 case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) 126 case '*' :: rest => make("[^:/]*" :: result, depth, rest) 127 case '?' :: rest => make("[^:/]" :: result, depth, rest) 128 case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) 129 case '{' :: rest => make("(" :: result, depth + 1, rest) 130 case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) 131 case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) 132 case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) 133 case c :: rest => make(c.toString :: result, dept [all...] |
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | winbasicio.cpp | 334 waitUntilOutputPossible(taskData); // canOutput will test the result and may update currentInBuffer. 390 // We've had EOF - That result is available 553 // Even if it actually succeeded we still pick up the result in canOutput. 587 // These tests may result in a GC if another thread is running. 617 // These tests may result in a GC if another thread is running. 630 Handle result = SAVE(C_string_to_Poly(taskData, (char*)buff, haveRead)); local 632 return result; 680 Handle result = 0; local 715 /* Copy the results to a result vector. */ 716 result 766 Handle result = NULL; local 1344 Handle result = 0; local 1366 bool result = false; local 1389 bool result = false; local [all...] |
H A D | basicio.cpp | 287 // These tests may result in a GC if another thread is running. 289 // These tests may result in a GC if another thread is running. 324 // These tests may result in a GC if another thread is running. 338 Handle result = SAVE(C_string_to_Poly(taskData, (char*)buff, haveRead)); local 340 return result; 490 Handle result = 0; local 521 // Construct the result vectors. 522 result = alloc_and_save(taskData, nDesc); 529 DEREFWORDHANDLE(result)->Set(i, TAGGED(res)); 539 if (result 1075 Handle result = 0; local 1098 Handle result = 0; local [all...] |
H A D | interpret.cpp | 179 // Put a real result in a "box" 489 case INSTR_deleteHandler: /* Delete handler retaining the result. */ 495 *sp = u; // Put back the result 576 stackItem result = *sp++; /* Result */ local 582 *(--sp) = result; /* Result */ 823 POLYUNSIGNED result = doCall(); local 827 *(--sp) = PolyWord::FromUnsigned(result); 837 POLYUNSIGNED result = doCall(rtsArg1); local 841 *(--sp) = PolyWord::FromUnsigned(result); 852 POLYUNSIGNED result local 868 POLYUNSIGNED result = doCall(rtsArg1, rtsArg2, rtsArg3); local 885 POLYUNSIGNED result = doCall(rtsArg1, rtsArg2, rtsArg3, rtsArg4); local 903 POLYUNSIGNED result = doCall(rtsArg1, rtsArg2, rtsArg3, rtsArg4, rtsArg5); local 916 POLYUNSIGNED result = doCall(this->threadObject); local 930 POLYUNSIGNED result = doCall(this->threadObject, rtsArg1); local 945 POLYUNSIGNED result = doCall(this->threadObject, rtsArg1, rtsArg2); local 961 POLYUNSIGNED result = doCall(this->threadObject, rtsArg1, rtsArg2, rtsArg3); local 1474 int result = memcmp(arg1Ptr+arg1Offset, arg2Ptr+arg2Offset, length); local [all...] |
H A D | osmemunix.cpp | 413 void *result = mmap(0, space, PROT_READ|PROT_WRITE, flags, fd, 0); local 415 if (result == MAP_FAILED) 417 return result; 443 void *result = mmap(0, space, prot, MAP_PRIVATE|MAP_ANON, fd, 0); local 445 if (result == MAP_FAILED) 447 shadowArea = result; 448 return result;
|
/seL4-l4v-master/HOL4/src/portableML/monads/ |
H A D | seqmonad.sml | 4 fun return x env = seq.result (env, x) 5 fun ok env = seq.result (env, ())
|
H A D | errormonad.sml | 68 | Some((s0',s'), result) => Some(s0',(s',result))
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | SHA1_ML.sml | 154 val result = Word8Array.array (20, 0wx0) value 156 (PackWord32Big.update(result, 0, Word32.toLarge h0) 157 ; PackWord32Big.update(result, 1, Word32.toLarge h1) 158 ; PackWord32Big.update(result, 2, Word32.toLarge h2) 159 ; PackWord32Big.update(result, 3, Word32.toLarge h3) 160 ; PackWord32Big.update(result, 4, Word32.toLarge h4) 161 ; Word8Array.vector result) 229 (* The initial values of the hash result state. These are defined
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Mosml.sml | 30 val result = if OS.Process.isSuccess status then value 38 result
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/tools/ |
H A D | tuerk_tacticsLib.sml | 19 val result = mk_eq(newLBody, newRBody) value 20 in ([(asl, result)], 34 val result = mk_eq(newLBody, newRBody) value 35 in ([(asl, result)], 185 val result = DISCH (concl thm) thm_t; value 186 val result = MP result thm value 188 result
|
/seL4-l4v-master/HOL4/src/compute/src/ |
H A D | selftest.sml | 9 val result = Lib.with_flag (Feedback.MESG_outstream, out) f x value 11 (result, String.concat (List.rev (!captured)))
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | KnuthBendixOrder.sml | 188 val result = compare kbo (tm1,tm2) 190 case result of 191 NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n" 193 Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x 195 result
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | cond_cleanLib.sml | 106 fun aux [] result = result 107 | aux (th::rest) result = let 108 val th = append_nop_to_if th result 109 in aux rest (th::result) end
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | KnuthBendixOrder.sml | 188 val result = compare kbo (tm1,tm2) 190 case result of 191 NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n" 193 Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x 195 result
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_tools.sig | 39 datatype 'a result = Res of 'a | Exn of exn 40 val get_res : 'a result -> 'a option 41 val get_exn : 'a result -> exn option 42 val capture : ('a -> 'b) -> 'a -> 'b result 43 val release : 'a result -> 'a
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | scan.scala | 300 val result = lexicon.scan(in) 301 if (result.isEmpty) Failure("keyword expected", in) 302 else Success(result, in.drop(result.length)) 326 private def dest(tree: Lexicon.Tree, result: List[String]): List[String] = 327 (result /: tree.branches.toList) ((res, entry) => 415 @tailrec def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String = 419 case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1) 420 case None => result 423 else result [all...] |