Searched refs:token (Results 26 - 50 of 114) sorted by relevance

12345

/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A DformParseScript.sml42 (token p [] = p []) ���
43 (token p (h::t) = if isSpace h then token p t else p (h::t))
48 ���EVERY isSpace s1 ��� token p (s1 ++ s2) = token p s2���,
86 ���(token p s = NONE) ���
102 ���(token p s = SOME (v, s')) ���
130 token (literal "F") ;
135 token (literal "G") ;
140 token (litera
[all...]
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dyacc.lex13 type ('a,'b) token = ('a,'b) Tokens.token
14 type lexresult = (svalue,pos) token
/seL4-l4v-10.1.1/l4v/tools/c-parser/
H A DStrictC.lex16 type ('a,'b) token = ('a,'b) Tokens.token
17 type lexresult= (svalue,pos) token
/seL4-l4v-10.1.1/l4v/tools/c-parser/tools/mlyacc/src/
H A Dyacc.lex16 type ('a,'b) token = ('a,'b) Tokens.token
17 type lexresult = (svalue,pos) token
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/mlyacclib/
H A DMLY_join.sml36 sharing type Lex.UserDeclarations.token = ParserData.Token.token)
70 yielding a value of type unit -> (svalue,pos) token
80 sharing type Lex.UserDeclarations.token = ParserData.Token.token)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DPrint.sig154 type token = string type
163 {token : token,
173 ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
H A DTerm.sml371 {token = "/", precedence = 7, assoc = Print.LeftAssoc},
372 {token = "div", precedence = 7, assoc = Print.LeftAssoc},
373 {token = "mod", precedence = 7, assoc = Print.LeftAssoc},
374 {token = "*", precedence = 7, assoc = Print.LeftAssoc},
375 {token = "+", precedence = 6, assoc = Print.LeftAssoc},
376 {token = "-", precedence = 6, assoc = Print.LeftAssoc},
377 {token = "^", precedence = 6, assoc = Print.LeftAssoc},
378 {token = "@", precedence = 5, assoc = Print.RightAssoc},
379 {token = "::", precedence = 5, assoc = Print.RightAssoc},
380 {token
[all...]
H A DParse.sig103 (Print.token * 'a * 'a -> 'a) -> ('b,Print.token) parser ->
/seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Djoin.sml17 sharing type Lex.UserDeclarations.token = ParserData.Token.token)
51 yielding a value of type unit -> (svalue,pos) token
61 sharing type Lex.UserDeclarations.token = ParserData.Token.token)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DPrint.sig154 type token = string type
163 {token : token,
173 ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
H A DTerm.sml371 {token = "/", precedence = 7, assoc = Print.LeftAssoc},
372 {token = "div", precedence = 7, assoc = Print.LeftAssoc},
373 {token = "mod", precedence = 7, assoc = Print.LeftAssoc},
374 {token = "*", precedence = 7, assoc = Print.LeftAssoc},
375 {token = "+", precedence = 6, assoc = Print.LeftAssoc},
376 {token = "-", precedence = 6, assoc = Print.LeftAssoc},
377 {token = "^", precedence = 6, assoc = Print.LeftAssoc},
378 {token = "@", precedence = 5, assoc = Print.RightAssoc},
379 {token = "::", precedence = 5, assoc = Print.RightAssoc},
380 {token
[all...]
H A DParse.sig103 (Print.token * 'a * 'a -> 'a) -> ('b,Print.token) parser ->
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Djoin.sml17 sharing type Lex.UserDeclarations.token = ParserData.Token.token)
51 yielding a value of type unit -> (svalue,pos) token
61 sharing type Lex.UserDeclarations.token = ParserData.Token.token)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dio_internal.h68 PolyWord token; // Either a pointer or a tagged int for stdIn etc. member in struct:basic_io_struct
108 extern PIOSTRUCT get_stream(PolyWord token);
H A Dwindows_specific.cpp100 is a token which is an ML object. The token is simply a word
101 containing the index in the table. It is the token itself which
102 represents the entry within the ML world. The token is checked
106 also allows us to garbage-collect entries since if the token becomes
111 PolyObject *token; /* pointer into ML heap */ member in struct:__anon84
154 pTab->token = 0;
158 static PHANDLETAB get_handle(PolyWord token, HANDENTRYTYPE heType) argument
160 StreamToken *handle_token = (StreamToken*)token.AsObjPtr();
164 handleTable[handle_no].token !
1337 PolyObject *token = str->readToken.AsObjPtr(); local
1343 PolyObject *token = str->writeToken.AsObjPtr(); local
[all...]
H A Dbasicio.cpp174 For each stream a single word token is made containing the file
178 address of the token. This also prevents streams other than stdin
304 str->token = TAGGED(0);
323 if (basic_io_vector[stream_no].token != stream_token)
337 // Find a free entry in the stream vector and return a token for it.
344 stream_no < max_streams && basic_io_vector[stream_no].token != ClosedToken;
359 basic_io_vector[i].token = ClosedToken;
362 // Create the token. This must be mutable not because it will be updated but
371 /* Clear the entry then set the token. */
373 basic_io_vector[stream_no].token
[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Djedit_rendering.scala33 /* Isabelle/Isar token markup */
69 def token_markup(syntax: Outer_Syntax, token: Token): Byte =
70 if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
71 else if (token.is_delimiter) JEditToken.OPERATOR
72 else token_style(token.kind)
75 /* Isabelle/ML token markup */
104 def ml_token_markup(token: ML_Lex.Token): Byte =
105 if (!token.is_keyword) ml_token_style(token
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_rendering.scala33 /* Isabelle/Isar token markup */
69 def token_markup(syntax: Outer_Syntax, token: Token): Byte =
70 if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
71 else if (token.is_delimiter) JEditToken.OPERATOR
72 else token_style(token.kind)
75 /* Isabelle/ML token markup */
104 def ml_token_markup(token: ML_Lex.Token): Byte =
105 if (!token.is_keyword) ml_token_style(token
[all...]
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A Dlocn.sig30 (* when a token is put back, eg with qbuf.replace_current, we
31 claim the new token is near where the old one was *)
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHolmake_types.sig12 datatype token = HM_defn of string * quotation type
22 val to_token : pretoken -> token
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A DAssembleHolindexParser.sml33 val s = "lex error - ill formed token \""^tok^"\"";
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DAssembleHolfootParser.sml41 val s = "lex error - ill formed token \""^tok^"\"";
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DLibrary.sml124 val token = case !buffer of value
125 SOME token => (buffer := NONE; token)
129 Feedback.HOL_MESG ("HolSmtLib: next token is '" ^ token ^ "'")
131 token
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/
H A Dtoken.scala1 /* Title: Pure/Isar/token.scala
4 Outer token syntax for Isabelle/Isar.
110 def token(keywords: Keyword.Keywords): Parser[Token] =
135 Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match {
191 /* token reader */
212 def advance(token: Token): Pos = advance(token.source)
233 def position(token: Token): Position.T = position(advance(token).offset)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/
H A Dtoken.scala1 /* Title: Pure/Isar/token.scala
4 Outer token syntax for Isabelle/Isar.
110 def token(keywords: Keyword.Keywords): Parser[Token] =
135 Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match {
191 /* token reader */
212 def advance(token: Token): Pos = advance(token.source)
233 def position(token: Token): Position.T = position(advance(token).offset)

Completed in 296 milliseconds

12345