improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
authorwenzelm
Mon Jun 29 20:55:46 2015 +0200 (2015-06-29)
changeset 60610f52b4b0c10c4
parent 60609 15620ae824c0
child 60611 27255d1fbe1a
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
NEWS
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/query_operation.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/print_operation.ML
     1.1 --- a/NEWS	Mon Jun 29 19:27:07 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 29 20:55:46 2015 +0200
     1.3 @@ -7,6 +7,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Prover IDE -- Isabelle/Scala/jEdit ***
     1.8 +
     1.9 +* Improved scheduling for urgent print tasks (e.g. command state output,
    1.10 +interactive queries) wrt. long-running background tasks.
    1.11 +
    1.12 +
    1.13  *** Isar ***
    1.14  
    1.15  * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jun 29 19:27:07 2015 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jun 29 20:55:46 2015 +0200
     2.3 @@ -408,7 +408,7 @@
     2.4  val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
     2.5  
     2.6  val _ =
     2.7 -  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
     2.8 +  Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, output_result} =>
     2.9      (case try Toplevel.proof_of st of
    2.10        SOME state =>
    2.11          let
     3.1 --- a/src/Pure/Concurrent/future.ML	Mon Jun 29 19:27:07 2015 +0200
     3.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jun 29 20:55:46 2015 +0200
     3.3 @@ -159,7 +159,7 @@
     3.4  fun report_status () = (*requires SYNCHRONIZED*)
     3.5    if ! ML_statistics then
     3.6      let
     3.7 -      val {ready, pending, running, passive} = Task_Queue.status (! queue);
     3.8 +      val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
     3.9        val total = length (! workers);
    3.10        val active = count_workers Working;
    3.11        val waiting = count_workers Waiting;
    3.12 @@ -169,6 +169,7 @@
    3.13          ("tasks_pending", Markup.print_int pending),
    3.14          ("tasks_running", Markup.print_int running),
    3.15          ("tasks_passive", Markup.print_int passive),
    3.16 +        ("tasks_urgent", Markup.print_int urgent),
    3.17          ("workers_total", Markup.print_int total),
    3.18          ("workers_active", Markup.print_int active),
    3.19          ("workers_waiting", Markup.print_int waiting)] @
    3.20 @@ -245,12 +246,12 @@
    3.21      (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ()));
    3.22       signal work_available;
    3.23       NONE)
    3.24 -  else if count_workers Working > ! max_active then
    3.25 -    (worker_wait Sleeping work_available; worker_next ())
    3.26    else
    3.27 -    (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
    3.28 -      NONE => (worker_wait Sleeping work_available; worker_next ())
    3.29 -    | some => (signal work_available; some));
    3.30 +    let val urgent_only = count_workers Working > ! max_active in
    3.31 +      (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of
    3.32 +        NONE => (worker_wait Sleeping work_available; worker_next ())
    3.33 +      | some => (signal work_available; some))
    3.34 +    end;
    3.35  
    3.36  fun worker_loop name =
    3.37    (case SYNCHRONIZED name (fn () => worker_next ()) of
     4.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon Jun 29 19:27:07 2015 +0200
     4.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon Jun 29 20:55:46 2015 +0200
     4.3 @@ -15,6 +15,7 @@
     4.4    val group_status: group -> exn list
     4.5    val str_of_group: group -> string
     4.6    val str_of_groups: group -> string
     4.7 +  val urgent_pri: int
     4.8    type task
     4.9    val dummy_task: task
    4.10    val group_of_task: task -> group
    4.11 @@ -31,7 +32,7 @@
    4.12    val group_tasks: queue -> group -> task list
    4.13    val known_task: queue -> task -> bool
    4.14    val all_passive: queue -> bool
    4.15 -  val status: queue -> {ready: int, pending: int, running: int, passive: int}
    4.16 +  val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
    4.17    val cancel: queue -> group -> Thread.thread list
    4.18    val cancel_all: queue -> group list * Thread.thread list
    4.19    val finish: task -> queue -> bool * queue
    4.20 @@ -40,7 +41,7 @@
    4.21    val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
    4.22    val extend: task -> (bool -> bool) -> queue -> queue option
    4.23    val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
    4.24 -  val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue
    4.25 +  val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
    4.26    val dequeue_deps: Thread.thread -> task list -> queue ->
    4.27      (((task * (bool -> bool) list) option * task list) * queue)
    4.28  end;
    4.29 @@ -97,6 +98,8 @@
    4.30  
    4.31  (* tasks *)
    4.32  
    4.33 +val urgent_pri = 1000;
    4.34 +
    4.35  type timing = Time.time * Time.time * string list;  (*run, wait, wait dependencies*)
    4.36  
    4.37  val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
    4.38 @@ -214,10 +217,10 @@
    4.39  
    4.40  (* queue *)
    4.41  
    4.42 -datatype queue = Queue of {groups: groups, jobs: jobs};
    4.43 +datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int};
    4.44  
    4.45 -fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
    4.46 -val empty = make_queue Inttab.empty Task_Graph.empty;
    4.47 +fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
    4.48 +val empty = make_queue Inttab.empty Task_Graph.empty 0;
    4.49  
    4.50  fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
    4.51  fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
    4.52 @@ -233,6 +236,10 @@
    4.53        else NONE
    4.54    | ready_job _ = NONE;
    4.55  
    4.56 +fun ready_job_urgent false = ready_job
    4.57 +  | ready_job_urgent true = (fn entry as (task, _) =>
    4.58 +      if pri_of_task task >= urgent_pri then ready_job entry else NONE);
    4.59 +
    4.60  fun active_job (task, (Running _, _)) = SOME (task, [])
    4.61    | active_job arg = ready_job arg;
    4.62  
    4.63 @@ -241,7 +248,7 @@
    4.64  
    4.65  (* queue status *)
    4.66  
    4.67 -fun status (Queue {jobs, ...}) =
    4.68 +fun status (Queue {jobs, urgent, ...}) =
    4.69    let
    4.70      val (x, y, z, w) =
    4.71        Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
    4.72 @@ -250,7 +257,7 @@
    4.73            | Running _ => (x, y, z + 1, w)
    4.74            | Passive _ => (x, y, z, w + 1)))
    4.75          jobs (0, 0, 0, 0);
    4.76 -  in {ready = x, pending = y, running = z, passive = w} end;
    4.77 +  in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
    4.78  
    4.79  
    4.80  
    4.81 @@ -258,7 +265,7 @@
    4.82  
    4.83  (* cancel -- peers and sub-groups *)
    4.84  
    4.85 -fun cancel (Queue {groups, jobs}) group =
    4.86 +fun cancel (Queue {groups, jobs, ...}) group =
    4.87    let
    4.88      val _ = cancel_group group Exn.Interrupt;
    4.89      val running =
    4.90 @@ -284,70 +291,75 @@
    4.91  
    4.92  (* finish *)
    4.93  
    4.94 -fun finish task (Queue {groups, jobs}) =
    4.95 +fun finish task (Queue {groups, jobs, urgent}) =
    4.96    let
    4.97      val group = group_of_task task;
    4.98      val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
    4.99      val jobs' = Task_Graph.del_node task jobs;
   4.100      val maximal = Task_Graph.is_maximal jobs task;
   4.101 -  in (maximal, make_queue groups' jobs') end;
   4.102 +  in (maximal, make_queue groups' jobs' urgent) end;
   4.103  
   4.104  
   4.105  (* enroll *)
   4.106  
   4.107 -fun enroll thread name group (Queue {groups, jobs}) =
   4.108 +fun enroll thread name group (Queue {groups, jobs, urgent}) =
   4.109    let
   4.110      val task = new_task group name NONE;
   4.111      val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   4.112      val jobs' = jobs |> Task_Graph.new_node (task, Running thread);
   4.113 -  in (task, make_queue groups' jobs') end;
   4.114 +  in (task, make_queue groups' jobs' urgent) end;
   4.115  
   4.116  
   4.117  (* enqueue *)
   4.118  
   4.119 -fun enqueue_passive group abort (Queue {groups, jobs}) =
   4.120 +fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
   4.121    let
   4.122      val task = new_task group "passive" NONE;
   4.123      val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   4.124      val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
   4.125 -  in (task, make_queue groups' jobs') end;
   4.126 +  in (task, make_queue groups' jobs' urgent) end;
   4.127  
   4.128 -fun enqueue name group deps pri job (Queue {groups, jobs}) =
   4.129 +fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =
   4.130    let
   4.131      val task = new_task group name (SOME pri);
   4.132      val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   4.133      val jobs' = jobs
   4.134        |> Task_Graph.new_node (task, Job [job])
   4.135        |> fold (add_job task) deps;
   4.136 -  in (task, make_queue groups' jobs') end;
   4.137 +    val urgent' = if pri >= urgent_pri then urgent + 1 else urgent;
   4.138 +  in (task, make_queue groups' jobs' urgent') end;
   4.139  
   4.140 -fun extend task job (Queue {groups, jobs}) =
   4.141 +fun extend task job (Queue {groups, jobs, urgent}) =
   4.142    (case try (get_job jobs) task of
   4.143 -    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs))
   4.144 +    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent)
   4.145    | _ => NONE);
   4.146  
   4.147  
   4.148  (* dequeue *)
   4.149  
   4.150 -fun dequeue_passive thread task (queue as Queue {groups, jobs}) =
   4.151 +fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent}) =
   4.152    (case try (get_job jobs) task of
   4.153      SOME (Passive _) =>
   4.154        let val jobs' = set_job task (Running thread) jobs
   4.155 -      in (SOME true, make_queue groups jobs') end
   4.156 +      in (SOME true, make_queue groups jobs' urgent) end
   4.157    | SOME _ => (SOME false, queue)
   4.158    | NONE => (NONE, queue));
   4.159  
   4.160 -fun dequeue thread (queue as Queue {groups, jobs}) =
   4.161 -  (case Task_Graph.get_first ready_job jobs of
   4.162 -    SOME (result as (task, _)) =>
   4.163 -      let val jobs' = set_job task (Running thread) jobs
   4.164 -      in (SOME result, make_queue groups jobs') end
   4.165 -  | NONE => (NONE, queue));
   4.166 +fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent}) =
   4.167 +  if not urgent_only orelse urgent > 0 then
   4.168 +    (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of
   4.169 +      SOME (result as (task, _)) =>
   4.170 +        let
   4.171 +          val jobs' = set_job task (Running thread) jobs;
   4.172 +          val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
   4.173 +        in (SOME result, make_queue groups jobs' urgent') end
   4.174 +    | NONE => (NONE, queue))
   4.175 +  else (NONE, queue);
   4.176  
   4.177  
   4.178  (* dequeue wrt. dynamic dependencies *)
   4.179  
   4.180 -fun dequeue_deps thread deps (queue as Queue {groups, jobs}) =
   4.181 +fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent}) =
   4.182    let
   4.183      fun ready [] rest = (NONE, rev rest)
   4.184        | ready (task :: tasks) rest =
   4.185 @@ -369,8 +381,10 @@
   4.186              end;
   4.187  
   4.188      fun result (res as (task, _)) deps' =
   4.189 -      let val jobs' = set_job task (Running thread) jobs
   4.190 -      in ((SOME res, deps'), make_queue groups jobs') end;
   4.191 +      let
   4.192 +        val jobs' = set_job task (Running thread) jobs;
   4.193 +        val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
   4.194 +      in ((SOME res, deps'), make_queue groups jobs' urgent') end;
   4.195    in
   4.196      (case ready deps [] of
   4.197        (SOME res, deps') => result res deps'
     5.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Jun 29 19:27:07 2015 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Jun 29 20:55:46 2015 +0200
     5.3 @@ -62,7 +62,8 @@
     5.4      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
     5.5      then
     5.6        Execution.print
     5.7 -        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
     5.8 +        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
     5.9 +        output
    5.10      else output ()
    5.11    end;
    5.12  
     6.1 --- a/src/Pure/PIDE/command.ML	Mon Jun 29 19:27:07 2015 +0200
     6.2 +++ b/src/Pure/PIDE/command.ML	Mon Jun 29 20:55:46 2015 +0200
     6.3 @@ -350,7 +350,7 @@
     6.4    print_function "Execution.print"
     6.5      (fn {args, exec_id, ...} =>
     6.6        if null args then
     6.7 -        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
     6.8 +        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false,
     6.9            print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
    6.10        else NONE);
    6.11  
    6.12 @@ -358,7 +358,7 @@
    6.13    print_function "print_state"
    6.14      (fn {keywords, command_name, ...} =>
    6.15        if Keyword.is_printed keywords command_name then
    6.16 -        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
    6.17 +        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
    6.18            print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
    6.19        else NONE);
    6.20  
     7.1 --- a/src/Pure/PIDE/protocol.ML	Mon Jun 29 19:27:07 2015 +0200
     7.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Jun 29 20:55:46 2015 +0200
     7.3 @@ -94,7 +94,7 @@
     7.4              (singleton o Future.forks)
     7.5               {name = "Document.update/remove", group = NONE,
     7.6                deps = maps Future.group_snapshot (maps Execution.peek removed),
     7.7 -              pri = 1, interrupts = false}
     7.8 +              pri = Task_Queue.urgent_pri + 2, interrupts = false}
     7.9               (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
    7.10  
    7.11            val _ =
     8.1 --- a/src/Pure/PIDE/query_operation.ML	Mon Jun 29 19:27:07 2015 +0200
     8.2 +++ b/src/Pure/PIDE/query_operation.ML	Mon Jun 29 20:55:46 2015 +0200
     8.3 @@ -7,17 +7,17 @@
     8.4  
     8.5  signature QUERY_OPERATION =
     8.6  sig
     8.7 -  val register: string ->
     8.8 +  val register: {name: string, pri: int} ->
     8.9      ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
    8.10  end;
    8.11  
    8.12  structure Query_Operation: QUERY_OPERATION =
    8.13  struct
    8.14  
    8.15 -fun register name f =
    8.16 +fun register {name, pri} f =
    8.17    Command.print_function name
    8.18      (fn {args = instance :: args, ...} =>
    8.19 -        SOME {delay = NONE, pri = 0, persistent = false, strict = false,
    8.20 +        SOME {delay = NONE, pri = pri, persistent = false, strict = false,
    8.21            print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    8.22              let
    8.23                fun result s = Output.result [(Markup.instanceN, instance)] [s];
     9.1 --- a/src/Pure/Tools/find_consts.ML	Mon Jun 29 19:27:07 2015 +0200
     9.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Jun 29 20:55:46 2015 +0200
     9.3 @@ -163,14 +163,15 @@
     9.4  (* PIDE query operation *)
     9.5  
     9.6  val _ =
     9.7 -  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
     9.8 -    (case try Toplevel.context_of state of
     9.9 -      SOME ctxt =>
    9.10 -        let
    9.11 -          val [query_arg] = args;
    9.12 -          val query = read_query Position.none query_arg;
    9.13 -        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    9.14 -    | NONE => error "Unknown context"));
    9.15 +  Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
    9.16 +    (fn {state, args, output_result} =>
    9.17 +      (case try Toplevel.context_of state of
    9.18 +        SOME ctxt =>
    9.19 +          let
    9.20 +            val [query_arg] = args;
    9.21 +            val query = read_query Position.none query_arg;
    9.22 +          in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    9.23 +      | NONE => error "Unknown context"));
    9.24  
    9.25  end;
    9.26  
    10.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Jun 29 19:27:07 2015 +0200
    10.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Jun 29 20:55:46 2015 +0200
    10.3 @@ -547,16 +547,17 @@
    10.4  (** PIDE query operation **)
    10.5  
    10.6  val _ =
    10.7 -  Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
    10.8 -    if can Toplevel.context_of st then
    10.9 -      let
   10.10 -        val [limit_arg, allow_dups_arg, query_arg] = args;
   10.11 -        val state = proof_state st;
   10.12 -        val opt_limit = Int.fromString limit_arg;
   10.13 -        val rem_dups = allow_dups_arg = "false";
   10.14 -        val criteria = read_query Position.none query_arg;
   10.15 -      in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
   10.16 -    else error "Unknown context");
   10.17 +  Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
   10.18 +    (fn {state = st, args, output_result} =>
   10.19 +      if can Toplevel.context_of st then
   10.20 +        let
   10.21 +          val [limit_arg, allow_dups_arg, query_arg] = args;
   10.22 +          val state = proof_state st;
   10.23 +          val opt_limit = Int.fromString limit_arg;
   10.24 +          val rem_dups = allow_dups_arg = "false";
   10.25 +          val criteria = read_query Position.none query_arg;
   10.26 +        in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
   10.27 +      else error "Unknown context");
   10.28  
   10.29  end;
   10.30  
    11.1 --- a/src/Pure/Tools/ml_statistics.scala	Mon Jun 29 19:27:07 2015 +0200
    11.2 +++ b/src/Pure/Tools/ml_statistics.scala	Mon Jun 29 20:55:46 2015 +0200
    11.3 @@ -34,7 +34,8 @@
    11.4    /* standard fields */
    11.5  
    11.6    val tasks_fields =
    11.7 -    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
    11.8 +    ("Future tasks",
    11.9 +      List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))
   11.10  
   11.11    val workers_fields =
   11.12      ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    12.1 --- a/src/Pure/Tools/print_operation.ML	Mon Jun 29 19:27:07 2015 +0200
    12.2 +++ b/src/Pure/Tools/print_operation.ML	Mon Jun 29 20:55:46 2015 +0200
    12.3 @@ -45,15 +45,16 @@
    12.4    report ());
    12.5  
    12.6  val _ =
    12.7 -  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
    12.8 -    let
    12.9 -      val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
   12.10 -      fun err s = Pretty.mark_str (Markup.bad, s);
   12.11 -      fun print name =
   12.12 -        (case AList.lookup (op =) (Synchronized.value print_operations) name of
   12.13 -          SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
   12.14 -        | NONE => [err ("Unknown print operation: " ^ quote name)]);
   12.15 -    in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
   12.16 +  Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
   12.17 +    (fn {state, args, output_result} =>
   12.18 +      let
   12.19 +        val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
   12.20 +        fun err s = Pretty.mark_str (Markup.bad, s);
   12.21 +        fun print name =
   12.22 +          (case AList.lookup (op =) (Synchronized.value print_operations) name of
   12.23 +            SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
   12.24 +          | NONE => [err ("Unknown print operation: " ^ quote name)]);
   12.25 +      in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
   12.26  
   12.27  end;
   12.28