equal
deleted
inserted
replaced
309 | _ => false); |
309 | _ => false); |
310 |
310 |
311 fun ident_or_symbolic "begin" = false |
311 fun ident_or_symbolic "begin" = false |
312 | ident_or_symbolic ":" = true |
312 | ident_or_symbolic ":" = true |
313 | ident_or_symbolic "::" = true |
313 | ident_or_symbolic "::" = true |
314 | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s; |
314 | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; |
315 |
315 |
316 |
316 |
317 (* scan verbatim text *) |
317 (* scan verbatim text *) |
318 |
318 |
319 val scan_verb = |
319 val scan_verb = |