--- a/src/Pure/Concurrent/task_queue.ML Mon Jan 08 23:44:02 2024 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Tue Jan 09 11:54:36 2024 +0100
@@ -250,7 +250,7 @@
gs Tasks.empty
|> Tasks.dest;
-fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
+fun known_task (Queue {jobs, ...}) task = Task_Graph.defined jobs task;
(* job status *)
--- a/src/Pure/General/graph.ML Mon Jan 08 23:44:02 2024 +0100
+++ b/src/Pure/General/graph.ML Tue Jan 09 11:54:36 2024 +0100
@@ -25,6 +25,7 @@
val keys: 'a T -> key list
val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
+ val defined: 'a T -> key -> bool
val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*)
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
@@ -120,6 +121,8 @@
fun get_first f (Graph tab) = Table.get_first f tab;
fun fold_graph f (Graph tab) = Table.fold f tab;
+fun defined (Graph tab) = Table.defined tab;
+
fun get_entry (Graph tab) x =
(case Table.lookup_key tab x of
SOME entry => entry