equal
deleted
inserted
replaced
338 val syn = Proof_Context.syn_of ctxt; |
338 val syn = Proof_Context.syn_of ctxt; |
339 val ast_tr = Syntax.parse_ast_translation syn; |
339 val ast_tr = Syntax.parse_ast_translation syn; |
340 |
340 |
341 val toks = Syntax.tokenize syn raw syms; |
341 val toks = Syntax.tokenize syn raw syms; |
342 val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks); |
342 val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks); |
|
343 val _ = toks |> List.app (fn tok => |
|
344 (case Lexicon.kind_of_token tok of |
|
345 Lexicon.Comment NONE => |
|
346 legacy_feature ("Old-style inner comment: use \"\<comment> \<open>...\<close>\" or \"\<^cancel>\<open>...\<close>\" instead" ^ |
|
347 Position.here (Lexicon.pos_of_token tok)) |
|
348 | _ => ())); |
343 |
349 |
344 val pts = Syntax.parse syn root (filter Lexicon.is_proper toks) |
350 val pts = Syntax.parse syn root (filter Lexicon.is_proper toks) |
345 handle ERROR msg => |
351 handle ERROR msg => |
346 error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks))); |
352 error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks))); |
347 val len = length pts; |
353 val len = length pts; |