equal
deleted
inserted
replaced
331 let |
331 let |
332 val id = Document_ID.print command_id; |
332 val id = Document_ID.print command_id; |
333 val span = |
333 val span = |
334 Lazy.lazy (fn () => |
334 Lazy.lazy (fn () => |
335 Position.setmp_thread_data (Position.id_only id) |
335 Position.setmp_thread_data (Position.id_only id) |
336 (fn () => Outer_Syntax.scan (get_keywords ()) (Position.id id) text) ()); |
336 (fn () => Token.explode (get_keywords ()) (Position.id id) text) ()); |
337 val _ = |
337 val _ = |
338 Position.setmp_thread_data (Position.id_only id) |
338 Position.setmp_thread_data (Position.id_only id) |
339 (fn () => Output.status (Markup.markup_only Markup.accepted)) (); |
339 (fn () => Output.status (Markup.markup_only Markup.accepted)) (); |
340 val commands' = |
340 val commands' = |
341 Inttab.update_new (command_id, (name, command_blobs, span)) commands |
341 Inttab.update_new (command_id, (name, command_blobs, span)) commands |