/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | formParseScript.sml | 42 (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 D | yacc.lex | 13 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 D | StrictC.lex | 16 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 D | yacc.lex | 16 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 D | MLY_join.sml | 36 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 D | Print.sig | 154 type token = string type 163 {token : token, 173 ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
|
H A D | Term.sml | 371 {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 D | Parse.sig | 103 (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 D | join.sml | 17 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 D | Print.sig | 154 type token = string type 163 {token : token, 173 ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
|
H A D | Term.sml | 371 {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 D | Parse.sig | 103 (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 D | join.sml | 17 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 D | io_internal.h | 68 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 D | windows_specific.cpp | 100 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 D | basicio.cpp | 174 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 D | jedit_rendering.scala | 33 /* 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 D | jedit_rendering.scala | 33 /* 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 D | locn.sig | 30 (* 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 D | Holmake_types.sig | 12 datatype token = HM_defn of string * quotation type 22 val to_token : pretoken -> token
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | AssembleHolindexParser.sml | 33 val s = "lex error - ill formed token \""^tok^"\"";
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | AssembleHolfootParser.sml | 41 val s = "lex error - ill formed token \""^tok^"\"";
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Library.sml | 124 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 D | token.scala | 1 /* 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 D | token.scala | 1 /* 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)
|