# HG changeset patch
# User wenzelm
# Date 1435604146 -7200
# Node ID f52b4b0c10c4b0ba105dcc78c315f086cbae909c
# Parent  15620ae824c085b2e812a0447acdca5179c893fc
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);

diff -r 15620ae824c0 -r f52b4b0c10c4 NEWS
--- a/NEWS	Mon Jun 29 19:27:07 2015 +0200
+++ b/NEWS	Mon Jun 29 20:55:46 2015 +0200
@@ -7,6 +7,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Improved scheduling for urgent print tasks (e.g. command state output,
+interactive queries) wrt. long-running background tasks.
+
+
 *** Isar ***
 
 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
diff -r 15620ae824c0 -r f52b4b0c10c4 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -408,7 +408,7 @@
 val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
 
 val _ =
-  Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
+  Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, output_result} =>
     (case try Toplevel.proof_of st of
       SOME state =>
         let
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -159,7 +159,7 @@
 fun report_status () = (*requires SYNCHRONIZED*)
   if ! ML_statistics then
     let
-      val {ready, pending, running, passive} = Task_Queue.status (! queue);
+      val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
       val total = length (! workers);
       val active = count_workers Working;
       val waiting = count_workers Waiting;
@@ -169,6 +169,7 @@
         ("tasks_pending", Markup.print_int pending),
         ("tasks_running", Markup.print_int running),
         ("tasks_passive", Markup.print_int passive),
+        ("tasks_urgent", Markup.print_int urgent),
         ("workers_total", Markup.print_int total),
         ("workers_active", Markup.print_int active),
         ("workers_waiting", Markup.print_int waiting)] @
@@ -245,12 +246,12 @@
     (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ()));
      signal work_available;
      NONE)
-  else if count_workers Working > ! max_active then
-    (worker_wait Sleeping work_available; worker_next ())
   else
-    (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of
-      NONE => (worker_wait Sleeping work_available; worker_next ())
-    | some => (signal work_available; some));
+    let val urgent_only = count_workers Working > ! max_active in
+      (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of
+        NONE => (worker_wait Sleeping work_available; worker_next ())
+      | some => (signal work_available; some))
+    end;
 
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next ()) of
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -15,6 +15,7 @@
   val group_status: group -> exn list
   val str_of_group: group -> string
   val str_of_groups: group -> string
+  val urgent_pri: int
   type task
   val dummy_task: task
   val group_of_task: task -> group
@@ -31,7 +32,7 @@
   val group_tasks: queue -> group -> task list
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
-  val status: queue -> {ready: int, pending: int, running: int, passive: int}
+  val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
   val cancel: queue -> group -> Thread.thread list
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
@@ -40,7 +41,7 @@
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
-  val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue
+  val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
   val dequeue_deps: Thread.thread -> task list -> queue ->
     (((task * (bool -> bool) list) option * task list) * queue)
 end;
@@ -97,6 +98,8 @@
 
 (* tasks *)
 
+val urgent_pri = 1000;
+
 type timing = Time.time * Time.time * string list;  (*run, wait, wait dependencies*)
 
 val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
@@ -214,10 +217,10 @@
 
 (* queue *)
 
-datatype queue = Queue of {groups: groups, jobs: jobs};
+datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int};
 
-fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
-val empty = make_queue Inttab.empty Task_Graph.empty;
+fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
+val empty = make_queue Inttab.empty Task_Graph.empty 0;
 
 fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
@@ -233,6 +236,10 @@
       else NONE
   | ready_job _ = NONE;
 
+fun ready_job_urgent false = ready_job
+  | ready_job_urgent true = (fn entry as (task, _) =>
+      if pri_of_task task >= urgent_pri then ready_job entry else NONE);
+
 fun active_job (task, (Running _, _)) = SOME (task, [])
   | active_job arg = ready_job arg;
 
@@ -241,7 +248,7 @@
 
 (* queue status *)
 
-fun status (Queue {jobs, ...}) =
+fun status (Queue {jobs, urgent, ...}) =
   let
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
@@ -250,7 +257,7 @@
           | Running _ => (x, y, z + 1, w)
           | Passive _ => (x, y, z, w + 1)))
         jobs (0, 0, 0, 0);
-  in {ready = x, pending = y, running = z, passive = w} end;
+  in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
 
 
 
@@ -258,7 +265,7 @@
 
 (* cancel -- peers and sub-groups *)
 
-fun cancel (Queue {groups, jobs}) group =
+fun cancel (Queue {groups, jobs, ...}) group =
   let
     val _ = cancel_group group Exn.Interrupt;
     val running =
@@ -284,70 +291,75 @@
 
 (* finish *)
 
-fun finish task (Queue {groups, jobs}) =
+fun finish task (Queue {groups, jobs, urgent}) =
   let
     val group = group_of_task task;
     val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
     val jobs' = Task_Graph.del_node task jobs;
     val maximal = Task_Graph.is_maximal jobs task;
-  in (maximal, make_queue groups' jobs') end;
+  in (maximal, make_queue groups' jobs' urgent) end;
 
 
 (* enroll *)
 
-fun enroll thread name group (Queue {groups, jobs}) =
+fun enroll thread name group (Queue {groups, jobs, urgent}) =
   let
     val task = new_task group name NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Running thread);
-  in (task, make_queue groups' jobs') end;
+  in (task, make_queue groups' jobs' urgent) end;
 
 
 (* enqueue *)
 
-fun enqueue_passive group abort (Queue {groups, jobs}) =
+fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
   let
     val task = new_task group "passive" NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
-  in (task, make_queue groups' jobs') end;
+  in (task, make_queue groups' jobs' urgent) end;
 
-fun enqueue name group deps pri job (Queue {groups, jobs}) =
+fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =
   let
     val task = new_task group name (SOME pri);
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs
       |> Task_Graph.new_node (task, Job [job])
       |> fold (add_job task) deps;
-  in (task, make_queue groups' jobs') end;
+    val urgent' = if pri >= urgent_pri then urgent + 1 else urgent;
+  in (task, make_queue groups' jobs' urgent') end;
 
-fun extend task job (Queue {groups, jobs}) =
+fun extend task job (Queue {groups, jobs, urgent}) =
   (case try (get_job jobs) task of
-    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs))
+    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent)
   | _ => NONE);
 
 
 (* dequeue *)
 
-fun dequeue_passive thread task (queue as Queue {groups, jobs}) =
+fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent}) =
   (case try (get_job jobs) task of
     SOME (Passive _) =>
       let val jobs' = set_job task (Running thread) jobs
-      in (SOME true, make_queue groups jobs') end
+      in (SOME true, make_queue groups jobs' urgent) end
   | SOME _ => (SOME false, queue)
   | NONE => (NONE, queue));
 
-fun dequeue thread (queue as Queue {groups, jobs}) =
-  (case Task_Graph.get_first ready_job jobs of
-    SOME (result as (task, _)) =>
-      let val jobs' = set_job task (Running thread) jobs
-      in (SOME result, make_queue groups jobs') end
-  | NONE => (NONE, queue));
+fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent}) =
+  if not urgent_only orelse urgent > 0 then
+    (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of
+      SOME (result as (task, _)) =>
+        let
+          val jobs' = set_job task (Running thread) jobs;
+          val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
+        in (SOME result, make_queue groups jobs' urgent') end
+    | NONE => (NONE, queue))
+  else (NONE, queue);
 
 
 (* dequeue wrt. dynamic dependencies *)
 
-fun dequeue_deps thread deps (queue as Queue {groups, jobs}) =
+fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent}) =
   let
     fun ready [] rest = (NONE, rev rest)
       | ready (task :: tasks) rest =
@@ -369,8 +381,10 @@
             end;
 
     fun result (res as (task, _)) deps' =
-      let val jobs' = set_job task (Running thread) jobs
-      in ((SOME res, deps'), make_queue groups jobs') end;
+      let
+        val jobs' = set_job task (Running thread) jobs;
+        val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
+      in ((SOME res, deps'), make_queue groups jobs' urgent') end;
   in
     (case ready deps [] of
       (SOME res, deps') => result res deps'
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -62,7 +62,8 @@
     if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
     then
       Execution.print
-        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
+        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
+        output
     else output ()
   end;
 
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -350,7 +350,7 @@
   print_function "Execution.print"
     (fn {args, exec_id, ...} =>
       if null args then
-        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
+        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false,
           print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
       else NONE);
 
@@ -358,7 +358,7 @@
   print_function "print_state"
     (fn {keywords, command_name, ...} =>
       if Keyword.is_printed keywords command_name then
-        SOME {delay = NONE, pri = 1, persistent = false, strict = false,
+        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
       else NONE);
 
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -94,7 +94,7 @@
             (singleton o Future.forks)
              {name = "Document.update/remove", group = NONE,
               deps = maps Future.group_snapshot (maps Execution.peek removed),
-              pri = 1, interrupts = false}
+              pri = Task_Queue.urgent_pri + 2, interrupts = false}
              (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
 
           val _ =
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -7,17 +7,17 @@
 
 signature QUERY_OPERATION =
 sig
-  val register: string ->
+  val register: {name: string, pri: int} ->
     ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
 end;
 
 structure Query_Operation: QUERY_OPERATION =
 struct
 
-fun register name f =
+fun register {name, pri} f =
   Command.print_function name
     (fn {args = instance :: args, ...} =>
-        SOME {delay = NONE, pri = 0, persistent = false, strict = false,
+        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];
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -163,14 +163,15 @@
 (* PIDE query operation *)
 
 val _ =
-  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
-    (case try Toplevel.context_of state of
-      SOME ctxt =>
-        let
-          val [query_arg] = args;
-          val query = read_query Position.none query_arg;
-        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
-    | NONE => error "Unknown context"));
+  Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
+    (fn {state, args, output_result} =>
+      (case try Toplevel.context_of state of
+        SOME ctxt =>
+          let
+            val [query_arg] = args;
+            val query = read_query Position.none query_arg;
+          in output_result (Pretty.string_of (pretty_consts ctxt query)) end
+      | NONE => error "Unknown context"));
 
 end;
 
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -547,16 +547,17 @@
 (** PIDE query operation **)
 
 val _ =
-  Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
-    if can Toplevel.context_of st then
-      let
-        val [limit_arg, allow_dups_arg, query_arg] = args;
-        val state = proof_state st;
-        val opt_limit = Int.fromString limit_arg;
-        val rem_dups = allow_dups_arg = "false";
-        val criteria = read_query Position.none query_arg;
-      in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
-    else error "Unknown context");
+  Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
+    (fn {state = st, args, output_result} =>
+      if can Toplevel.context_of st then
+        let
+          val [limit_arg, allow_dups_arg, query_arg] = args;
+          val state = proof_state st;
+          val opt_limit = Int.fromString limit_arg;
+          val rem_dups = allow_dups_arg = "false";
+          val criteria = read_query Position.none query_arg;
+        in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+      else error "Unknown context");
 
 end;
 
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/Tools/ml_statistics.scala
--- a/src/Pure/Tools/ml_statistics.scala	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/ml_statistics.scala	Mon Jun 29 20:55:46 2015 +0200
@@ -34,7 +34,8 @@
   /* standard fields */
 
   val tasks_fields =
-    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+    ("Future tasks",
+      List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))
 
   val workers_fields =
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
diff -r 15620ae824c0 -r f52b4b0c10c4 src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Mon Jun 29 19:27:07 2015 +0200
+++ b/src/Pure/Tools/print_operation.ML	Mon Jun 29 20:55:46 2015 +0200
@@ -45,15 +45,16 @@
   report ());
 
 val _ =
-  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
-    let
-      val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
-      fun err s = Pretty.mark_str (Markup.bad, s);
-      fun print name =
-        (case AList.lookup (op =) (Synchronized.value print_operations) name of
-          SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
-        | NONE => [err ("Unknown print operation: " ^ quote name)]);
-    in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
+  Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
+    (fn {state, args, output_result} =>
+      let
+        val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
+        fun err s = Pretty.mark_str (Markup.bad, s);
+        fun print name =
+          (case AList.lookup (op =) (Synchronized.value print_operations) name of
+            SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
+          | NONE => [err ("Unknown print operation: " ^ quote name)]);
+      in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
 
 end;