# HG changeset patch
# User wenzelm
# Date 1704797676 -3600
# Node ID ec7a1603129a38473a756e89ee291fab5904d959
# Parent  a7241e5db6019f85b8e261365c98d03f6665a75a
clarified signature;

diff -r a7241e5db601 -r ec7a1603129a src/Pure/Concurrent/task_queue.ML
--- 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 *)
diff -r a7241e5db601 -r ec7a1603129a src/Pure/General/graph.ML
--- 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