# HG changeset patch
# User wenzelm
# Date 1667571325 -3600
# Node ID bb96846e27f8e28864045c9d0e36c5231aec56d3
# Parent  bd919b794b38a33f817c3cbeaf7b8f068da112e8
tuned signature;

diff -r bd919b794b38 -r bb96846e27f8 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Nov 04 15:09:44 2022 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Nov 04 15:15:25 2022 +0100
@@ -26,7 +26,7 @@
   type print
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   val print0: {pri: int, print_fn: print_fn} -> eval -> print
-  val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
+  val print: Keyword.keywords -> bool -> (string * string list) list -> string ->
     eval -> print list -> print list option
   val parallel_print: print -> bool
   type print_function =
@@ -362,7 +362,7 @@
   make_print ("", [serial_string ()])
     {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
 
-fun print visible overlays keywords command_name eval old_prints =
+fun print keywords visible overlays command_name eval old_prints =
   let
     val print_functions = Synchronized.value print_functions;
 
diff -r bd919b794b38 -r bb96846e27f8 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 04 15:09:44 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 15:15:25 2022 +0100
@@ -679,7 +679,7 @@
                   val overlays = command_overlays node command_id;
                   val command_name = the_command_name command_id;
                 in
-                  (case Command.print visible overlays keywords command_name eval prints of
+                  (case Command.print keywords visible overlays command_name eval prints of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
@@ -710,7 +710,7 @@
       val eval' =
         Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
           (blobs, blobs_index) command_id' span (#1 (#2 command_exec));
-      val prints' = perhaps (Command.print visible overlays keywords command_name eval') [];
+      val prints' = perhaps (Command.print keywords visible overlays command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;