/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/ |
H A D | commonUnifScript.sml | 12 `!subst source z. 13 (((FINITE (source z)) /\ 15 (!n. DISJOINT (FDOM (subst n)) (source n)) /\ 16 (!n. z < n ==> (FDOM (subst n) UNION (source n) = FDOM (subst z) UNION (source z)))) 20 `!m. z <= m ==> ?n.m < n /\ CARD(source n) < CARD(source m)` 25 by (Q.EXISTS_TAC `\n.CARD(source(FUNPOW f n z))` THEN 35 `(FDOM (subst n) UNION source n = FDOM (subst m) UNION source [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | PEGParse.sig | 20 datatype ('source,'tok,'nt,'value)kont = 21 ksym of ('tok,'nt,'value)pegsym * ('source,'tok,'nt,'value)kont * 22 ('source,'tok,'nt,'value)kont 23 | appf1 of ('value -> 'value) * ('source,'tok,'nt,'value)kont 24 | appf2 of ('value -> 'value -> 'value) * ('source,'tok,'nt,'value)kont 25 | returnTo of 'source * 'value option list * 26 ('source,'tok,'nt,'value)kont 27 | poplist of ('value list -> 'value) * ('source,'tok,'nt,'value)kont 29 ('source,'tok,'nt,'value)kont 35 ('source [all...] |
/seL4-l4v-10.1.1/l4v/tools/c-parser/ |
H A D | StrictC.lex | 38 source : SourceFile.t, 59 val eof = (fn {source,in_comment,in_attr,commentStart,...} : lexstate => 60 let val pos = SourceFile.lineStart source 93 fun resolve_id (b, arg as {source=src,tokidseen,...}:lexstate, l, s) = 110 source = SourceFile.new fname, 125 %arg ({source, in_comment, commentStart, stringlitContent, stringlitStart, charlitContent, charlitStart, tokpdepth, tokbdepth, tokidseen, return,...}:UserDeclarations.lexstate); 147 <INITIAL,TSI>";" => (tok(Tokens.YSEMI,source,yypos,yypos)); 148 <TDEF,TSS,TS>";" => (YYBEGIN INITIAL; tok(Tokens.YSEMI,source,yypos,yypos)); 151 <INITIAL,TSI>"," => (tok(Tokens.YCOMMA,source,yypos,yypos+size yytext-1)); 153 tok(Tokens.YCOMMA,source,yypo [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | nested_struct11.c | 28 static C C_fn (int x, int y, int z, C source, int i, int j, int k) argument 31 result.a.a_x = source.a.a_x; 32 result.a.a_y = source.a.a_y; 33 result.b.b_x = source.b.b_x; 34 result.b.b_y = source.b.b_y; 40 source.a.a_x, source.a.a_y, 41 source.b.b_x, source.b.b_y, 64 struct C source local [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | antiquote.scala | 12 sealed abstract class Antiquote { def source: String } 13 case class Text(source: String) extends Antiquote 14 case class Control(source: String) extends Antiquote 15 case class Antiq(source: String) extends Antiquote 53 error("Malformed quotation/antiquotation source" + 61 case List(Antiq(source)) => Some(source.substring(2, source.length - 1))
|
H A D | scan.scala | 59 val end = in.source.length 60 val matcher = new Symbol.Matcher(in.source) 67 val sym = in.source.subSequence(i, i + n).toString 72 else Success(in.source.subSequence(start, i).toString, in.drop(i - start)) 108 def quoted_content(quote: Symbol.Symbol, source: String): String = 110 require(parseAll(quoted(quote), source).successful) 111 val body = source.substring(1, source.length - 1) 150 def verbatim_content(source: String): String = 152 require(parseAll(verbatim, source) [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | antiquote.scala | 12 sealed abstract class Antiquote { def source: String } 13 case class Text(source: String) extends Antiquote 14 case class Control(source: String) extends Antiquote 15 case class Antiq(source: String) extends Antiquote 53 error("Malformed quotation/antiquotation source" + 61 case List(Antiq(source)) => Some(source.substring(2, source.length - 1))
|
H A D | scan.scala | 59 val end = in.source.length 60 val matcher = new Symbol.Matcher(in.source) 67 val sym = in.source.subSequence(i, i + n).toString 72 else Success(in.source.subSequence(start, i).toString, in.drop(i - start)) 108 def quoted_content(quote: Symbol.Symbol, source: String): String = 110 require(parseAll(quoted(quote), source).successful) 111 val body = source.substring(1, source.length - 1) 150 def verbatim_content(source: String): String = 152 require(parseAll(verbatim, source) [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | yxml.scala | 62 private def parse_attrib(source: CharSequence) = { 63 val s = source.toString 70 def parse_body(source: CharSequence): XML.Body = 101 for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) { 117 def parse(source: CharSequence): XML.Tree = 118 parse_body(source) match { 124 def parse_elem(source: CharSequence): XML.Tree = 125 parse_body(source) match { 133 private def markup_broken(source: CharSequence) = 134 XML.Elem(Markup.Broken, List(XML.Text(source [all...] |
H A D | command_span.scala | 45 def length: Int = (0 /: content)(_ + _.source.length) 49 val source = Token.implode(content) 54 val s1 = source.substring(i, i + n) 58 (source, Span(kind, content1.toList)) 64 def unparsed(source: String): Span = 65 Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | yxml.scala | 62 private def parse_attrib(source: CharSequence) = { 63 val s = source.toString 70 def parse_body(source: CharSequence): XML.Body = 101 for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) { 117 def parse(source: CharSequence): XML.Tree = 118 parse_body(source) match { 124 def parse_elem(source: CharSequence): XML.Tree = 125 parse_body(source) match { 133 private def markup_broken(source: CharSequence) = 134 XML.Elem(Markup.Broken, List(XML.Text(source [all...] |
H A D | command_span.scala | 45 def length: Int = (0 /: content)(_ + _.source.length) 49 val source = Token.implode(content) 54 val s1 = source.substring(i, i + n) 58 (source, Span(kind, content1.toList)) 64 def unparsed(source: String): Span = 65 Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | parse.sml | 37 val source = Header.newSource(file,in_str,TextIO.stdOut) value 39 Header.error source i s 41 source 44 Parser.parse(15,stream,error,source)) 45 in (TextIO.closeIn in_str; (result,source))
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
H A D | update_comments.scala | 24 if tok.source == "--" || tok.source == Symbol.comment => 28 case _ => update(rest, tok.source :: result) 30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) => 32 case tok :: rest => update(rest, tok.source :: result)
|
H A D | update_header.scala | 17 yield { if (tok.source == "header") section else tok.source }).mkString
|
H A D | update_cartouches.scala | 32 if (ants == ants1) content else ants1.map(_.source).mkString 49 case s => tok.source 52 else tok.source 65 if (content == content1) tok.source 69 else tok.source
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | update_comments.scala | 24 if tok.source == "--" || tok.source == Symbol.comment => 28 case _ => update(rest, tok.source :: result) 30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) => 32 case tok :: rest => update(rest, tok.source :: result)
|
H A D | update_header.scala | 17 yield { if (tok.source == "header") section else tok.source }).mkString
|
H A D | update_cartouches.scala | 32 if (ants == ants1) content else ants1.map(_.source).mkString 49 case s => tok.source 52 else tok.source 65 if (content == content1) tok.source 69 else tok.source
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/32/mode/machine/ |
H A D | debug.h | 106 *@param source The memory block from which to load the register values. 109 loadBreakpointState(tcb_t *source) 135 : "r" (source->tcbArch.tcbContext.breakpointState.dr)
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/machine/ |
H A D | debug.h | 106 *@param source The memory block from which to load the register values. 109 loadBreakpointState(tcb_t *source) 135 : "r" (source->tcbArch.tcbContext.breakpointState.dr)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src-base/ |
H A D | isabelle_encoding.scala | 27 val source = (new BufferedSource(in)(codec)).mkString 29 if (strict && Codepoint.iterator(source).exists(Symbol.is_code)) 32 new CharArrayReader(Symbol.decode(source).toArray)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src-base/ |
H A D | isabelle_encoding.scala | 27 val source = (new BufferedSource(in)(codec)).mkString 29 if (strict && Codepoint.iterator(source).exists(Symbol.is_code)) 32 new CharArrayReader(Symbol.decode(source).toArray)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 70 if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 73 case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3 74 case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4 128 yield (token_style(chunk.kind, tok), tok.source) 165 private class Asset(label: String, label_html: String, range: Text.Range, source: String) 168 override def getLongString: String = source 180 val source = chunk.source 186 val range = Text.Range(offset, offset + source.length) 187 val asset = new Asset(label, label_html, range, source) [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 70 if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 73 case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3 74 case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4 128 yield (token_style(chunk.kind, tok), tok.source) 165 private class Asset(label: String, label_html: String, range: Text.Range, source: String) 168 override def getLongString: String = source 180 val source = chunk.source 186 val range = Text.Range(offset, offset + source.length) 187 val asset = new Asset(label, label_html, range, source) [all...] |