/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | token_markup.scala | 4 Outer syntax token markup. 215 /* token marker */ 272 for ((style, token) <- styled_tokens) { 273 val length = token.length
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 470 type token = string; type 479 {token : token, 486 val {token = _, precedence = p1, assoc = _} = io1 value 487 and {token = _, precedence = p2, assoc = _} = io2 value 507 fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) = 517 | {token = t, precedence = p, assoc = a} :: ios =>
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 470 type token = string; type 479 {token : token, 486 val {token = _, precedence = p1, assoc = _} = io1 value 487 and {token = _, precedence = p2, assoc = _} = io2 value 507 fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) = 517 | {token = t, precedence = p, assoc = a} :: ios =>
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | type_tokens.sml | 153 | dest_aq _ = raise Fail "dest_aq of non antiquote token"
|
H A D | parse_term.sml | 33 type 'a token = 'a term_tokens.term_token 221 val msg = "Grammar ambiguous on token pair "^ 355 x > rule's left hand token 359 rule's right hand token < x 514 (* string is name of term; list of pairs, is list of token-pairs between 621 (* dummy lookahead token *) 778 (* transform takes an input token (of the sort that comes out of the 779 lexer), and turns it into a token of the sort used internally by the 937 nonterminal) or a TOK (=token, i.e., terminal). *) 1409 be a special token b [all...] |
H A D | parse_type.sml | 54 push back the unwanted token *) 55 (* can't use item for these, because this would require the token type
|
H A D | ParseDatatype.sml | 278 "Unexpected token in constructor's argument"
|
H A D | term_pp.sml | 195 the base token technology (see base_lexer) to separate the 802 endbinding token. If this happens, then the restriction needs 804 "." as the endbinding token and as the infix record selection 810 or not the restrictor might print an endbinding token. *) 905 [] => raise PP_ERR "pr_abs" "No token for lambda abstraction"
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | yacc.sml | 180 sayln "type ('a,'b) token = ('a,'b) Token.token"; 210 "type ('a,'b) token\ntype svalue\n" ^ 216 " 'a * 'a -> (svalue,'a) token\n", r]) "" term) ^ 221 ".Token.token = Tokens.token\nsharing type " ^
|
/seL4-l4v-10.1.1/isabelle/src/Pure/ |
H A D | build-jars | 86 Isar/token.scala
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ |
H A D | build-jars | 86 Isar/token.scala
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | misc.tex | 1138 By default, the HOL pretty-printer is paranoid about token-merging, and will insert spaces between the tokens it emits to try to ensure that what is output can be read in again without error. 1146 (In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.) 1319 \item[$s\mathtt{//}t$] (For use with \holtm{}, \holthm, and \holty) Causes \LaTeX{} string $s$ to be substituted for token $t$. 1323 The width of the \LaTeX{} string is taken to be the width of the original token $t$. 1412 token-to-\LaTeX{} replacements of what is pretty-printed. 1422 where \texttt{tok} is a \HOL{} token, \texttt{width} is a number 1446 By overriding the special token \texttt{\$Turnstile\$}, one can control the printing of the turnstile produced by \holthm{}. 1463 \paragraph{Preventing Merge Analysis} As mentioned above in the description of the \texttt{merge} and \texttt{nomerge} options to the \holtm{} and \holthm{} commands, the munger can be configured to not do token-merging avoidance by passing the \texttt{--nomergeanalysis} option to the munger. 1681 token-to-\LaTeX{} replacements of what is pretty-printed. 1699 Though one might specify all one's desired token [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | OldPP.sml | 110 a stack of indices into the token buffer. The indices only point to 155 (* The initial values in the token buffer *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | json.scala | 122 /* token */ 124 def token: Parser[Token] =
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | options.scala | 86 opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
|
/seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ |
H A D | tptp.yacc | 598 instead of subtype_sign use token SUBTYPE 621 use token GENTZEN_ARROW
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | json.scala | 122 /* token */ 124 def token: Parser[Token] =
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | options.scala | 86 opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ |
H A D | tptp.yacc | 598 instead of subtype_sign use token SUBTYPE 621 use token GENTZEN_ARROW
|
/seL4-l4v-10.1.1/HOL4/tools/mllex/ |
H A D | mllex.sml | 163 as our token, when we should have "a" as our token. 251 datatype token = CHARS of bool array | QMARK | STAR | PLUS | BAR type 681 fun GetTok (_:unit) : token =
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 1044 By default, the HOL pretty-printer is paranoid about token-merging, and will insert spaces between the tokens it emits to try to ensure that what is output can be read in again without error. 1052 (In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.) 1242 token-to-\LaTeX{} replacements of what is pretty-printed. 1252 where \texttt{tok} is a \HOL{} token, \texttt{width} is a number 1288 \paragraph{Preventing Merge Analysis} As mentioned above in the description of the \texttt{merge} and \texttt{nomerge} options to the \holtm{} and \holthm{} commands, the munger can be configured to not do token-merging avoidance by passing the \texttt{--nomergeanalysis} option to the munger. 1497 token-to-\LaTeX{} replacements of what is pretty-printed. 1515 Though one might specify all one's desired token-replacements in an \texttt{overrides} file, there is also support for specifying token replacements in the theory where tokens are first ``defined''. 1519 A token's printing form is given in a script-file with the \ml{TeX\_notation} command (from the \ml{TexTokenMap} module). 1525 The \ml{hol} field specifies the string of the token a [all...] |
H A D | system.tex | 102 A meno che il token desiderato non sia gi� presente nella grammatica, questi 105 token, cos� come lo sono \holtxt{"+;"} e \holtxt{"-+"}. 107 \index{token!Caratteri unicode} 161 In generale, un utente \HOL{} ha una grande quantit� di libert� di creare la sua propria sintassi, richiedendo token speciali a prescindere dalle variabili e dai nomi per le costanti. 164 ha token speciali (l'``if'', il ``then'' e l'``else'') che non sono nomi per le variabili, n� per le costanti (la costante sottostante � di fatto chiamata \holtxt{COND}). 165 Per essere sicuro che le operazioni di stampa e parsing dei token siano appropriatamente l'una l'inverso dell'altra, gli utenti non dovrebbero creare token che includono spazi vuoti o le stringhe di commento (\ml{(*} and \ml{*)}). 166 \index{token|)} 708 token non � mai dato un trattamento speciale dal parser della sintassi
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holmake_types.sml | 16 datatype token = HM_defn of string * quotation type
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | String.sml | 334 fun tok' i l = (* i is the character to examine. l is the start of a token *) 356 fun field' i l = (* i is the character to examine. l is the start of a token *) 1508 fun tok' i l = (* i is the character to examine. l is the start of a token *) 1530 fun field' i l = (* i is the character to examine. l is the start of a token *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | texinfo.tex | 177 % Ignore a token. 433 \parseargline\empty% Insert the \empty token, see \finishparsearg below. 451 % This space token undergoes the same procedure and is eventually removed 464 % Put the space token in: 470 % We prepended an \empty token at the very beginning and we expand it now, 476 % But first, we have to remove the trailing space token. 3678 % \splitoff TOKENS\endmark defines \first to be the first token in 3693 % Detect if the argument is a single token. If so, it might be a 3695 % (We will always have one token, because of the test we just made. 3700 % Only one token i [all...] |