Searched refs:token (Results 76 - 100 of 114) sorted by relevance

12345

/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Dtoken_markup.scala4 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 DPrint.sml470 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 DPrint.sml470 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 Dtype_tokens.sml153 | dest_aq _ = raise Fail "dest_aq of non antiquote token"
H A Dparse_term.sml33 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 Dparse_type.sml54 push back the unwanted token *)
55 (* can't use item for these, because this would require the token type
H A DParseDatatype.sml278 "Unexpected token in constructor's argument"
H A Dterm_pp.sml195 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 Dyacc.sml180 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 Dbuild-jars86 Isar/token.scala
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/
H A Dbuild-jars86 Isar/token.scala
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A Dmisc.tex1138 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 DOldPP.sml110 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 Djson.scala122 /* token */
124 def token: Parser[Token] =
/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Doptions.scala86 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 Dtptp.yacc598 instead of subtype_sign use token SUBTYPE
621 use token GENTZEN_ARROW
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Djson.scala122 /* token */
124 def token: Parser[Token] =
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Doptions.scala86 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 Dtptp.yacc598 instead of subtype_sign use token SUBTYPE
621 use token GENTZEN_ARROW
/seL4-l4v-10.1.1/HOL4/tools/mllex/
H A Dmllex.sml163 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 Dmisc.tex1044 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 Dsystem.tex102 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 DHolmake_types.sml16 datatype token = HM_defn of string * quotation type
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DString.sml334 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 Dtexinfo.tex177 % 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...]

Completed in 331 milliseconds

12345