equal
deleted
inserted
replaced
64 val tidT: typ |
64 val tidT: typ |
65 val tvarT: typ |
65 val tvarT: typ |
66 val terminals: string list |
66 val terminals: string list |
67 val is_terminal: string -> bool |
67 val is_terminal: string -> bool |
68 val report_token: Proof.context -> token -> unit |
68 val report_token: Proof.context -> token -> unit |
|
69 val report_token_range: Proof.context -> token -> unit |
69 val matching_tokens: token * token -> bool |
70 val matching_tokens: token * token -> bool |
70 val valued_token: token -> bool |
71 val valued_token: token -> bool |
71 val predef_term: string -> token option |
72 val predef_term: string -> token option |
72 val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list |
73 val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list |
73 end; |
74 end; |
186 | EOF => Markup.empty; |
187 | EOF => Markup.empty; |
187 |
188 |
188 fun report_token ctxt (Token (kind, _, (pos, _))) = |
189 fun report_token ctxt (Token (kind, _, (pos, _))) = |
189 Context_Position.report ctxt (token_kind_markup kind) pos; |
190 Context_Position.report ctxt (token_kind_markup kind) pos; |
190 |
191 |
|
192 fun report_token_range ctxt tok = |
|
193 if is_proper tok |
|
194 then Context_Position.report ctxt Markup.token_range (pos_of_token tok) |
|
195 else (); |
|
196 |
191 |
197 |
192 (* matching_tokens *) |
198 (* matching_tokens *) |
193 |
199 |
194 fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y |
200 fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y |
195 | matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k'; |
201 | matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k'; |