Searched refs:source (Results 1 - 25 of 202) sorted by relevance

123456789

/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/
H A DcommonUnifScript.sml12 `!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 DPEGParse.sig20 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 DStrictC.lex38 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 Dnested_struct11.c28 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 Dantiquote.scala12 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 Dscan.scala59 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 Dantiquote.scala12 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 Dscan.scala59 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 Dyxml.scala62 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 Dcommand_span.scala45 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 Dyxml.scala62 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 Dcommand_span.scala45 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 Dparse.sml37 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 Dupdate_comments.scala24 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 Dupdate_header.scala17 yield { if (tok.source == "header") section else tok.source }).mkString
H A Dupdate_cartouches.scala32 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 Dupdate_comments.scala24 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 Dupdate_header.scala17 yield { if (tok.source == "header") section else tok.source }).mkString
H A Dupdate_cartouches.scala32 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 Ddebug.h106 *@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 Ddebug.h106 *@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 Disabelle_encoding.scala27 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 Disabelle_encoding.scala27 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 Djedit_bibtex.scala70 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 Djedit_bibtex.scala70 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...]

Completed in 221 milliseconds

123456789