src/Pure/PIDE/document.ML
changeset 59083 88b0b1f28adc
parent 59056 cbe9563c03d1
child 59085 08a6901eb035
equal deleted inserted replaced
59082:25501ba956ac 59083:88b0b1f28adc
   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