src/Pure/PIDE/query_operation.ML

       SOME {delay = NONE, pri = pri, persistent = false, strict = false,
         print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
           let
             fun result s = Output.result [(Markup.instanceN, instance)] [s];
             fun status m = result (Markup.markup_only m);
-            fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
-            fun toplevel_error exn =
-              result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
+            fun output_result s = result (Markup.markup Markup.writeln s);
+            fun toplevel_error exn = result (Markup.markup Markup.error (Runtime.exn_message exn));
 
             val _ = status Markup.running;
             fun run () = f {state = state, args = args, output_result = output_result};
             val _ =
               (case Exn.capture (*sic!*) (restore_attributes run) () of

 
 val _ =
   register {name = "print_state", pri = Task_Queue.urgent_pri + 2}
     (fn {state = st, output_result, ...} =>
       if Toplevel.is_proof st
-      then output_result (Markup.markup (Markup.stateN, []) (Toplevel.string_of_state st))
+      then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
       else ());
 
 end;