# HG changeset patch
# User wenzelm
# Date 1310568134 -7200
# Node ID d5803c3d537a90d1dbbf83664252155193119d53
# Parent  5e9a1d71f94d6f33f13a73bebe78908f26f33a3f
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
Sorts.certify_class: prefer the persistent name;

diff -r 5e9a1d71f94d -r d5803c3d537a src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Jul 13 16:42:14 2011 +0200
@@ -318,7 +318,7 @@
       | ready (task :: tasks) rest =
           (case try (Task_Graph.get_entry jobs) task of
             NONE => ready tasks rest
-          | SOME entry =>
+          | SOME (_, entry) =>
               (case ready_job task entry of
                 NONE => ready tasks (task :: rest)
               | some => (some, List.revAppend (rest, tasks))));
@@ -327,7 +327,7 @@
       | ready_dep seen (task :: tasks) =
           if Tasks.defined seen task then ready_dep seen tasks
           else
-            let val entry as (_, (ds, _)) = Task_Graph.get_entry jobs task in
+            let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
               (case ready_job task entry of
                 NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
               | some => some)
diff -r 5e9a1d71f94d -r d5803c3d537a src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/General/graph.ML	Wed Jul 13 16:42:14 2011 +0200
@@ -20,7 +20,7 @@
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
   val subgraph: (key -> bool) -> 'a T -> 'a T
-  val get_entry: 'a T -> key -> 'a * (key list * key list)            (*exception UNDEF*)
+  val get_entry: 'a T -> key -> key * ('a * (key list * key list))    (*exception UNDEF*)
   val map: (key -> 'a -> 'b) -> 'a T -> 'b T
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
@@ -101,14 +101,14 @@
   in Graph (fold_graph subg G Table.empty) end;
 
 fun get_entry (Graph tab) x =
-  (case Table.lookup tab x of
+  (case Table.lookup_key tab x of
     SOME entry => entry
   | NONE => raise UNDEF x);
 
-fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
+fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
 
 fun map_entry_yield x f (G as Graph tab) =
-  let val (a, node') = f (get_entry G x)
+  let val (a, node') = f (#2 (get_entry G x))
   in (a, Graph (Table.update (x, node') tab)) end;
 
 
@@ -116,7 +116,7 @@
 
 fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
 
-fun get_node G = #1 o get_entry G;
+fun get_node G = #1 o #2 o get_entry G;
 
 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
 
@@ -137,8 +137,8 @@
   in fold reachs xs ([], empty_keys) end;
 
 (*immediate*)
-fun imm_preds G = #1 o #2 o get_entry G;
-fun imm_succs G = #2 o #2 o get_entry G;
+fun imm_preds G = #1 o #2 o #2 o get_entry G;
+fun imm_succs G = #2 o #2 o #2 o get_entry G;
 
 (*transitive*)
 fun all_preds G = flat o #1 o reachable (imm_preds G);
@@ -167,7 +167,7 @@
 fun del_node x (G as Graph tab) =
   let
     fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
-    val (preds, succs) = #2 (get_entry G x);
+    val (preds, succs) = #2 (#2 (get_entry G x));
   in
     Graph (tab
       |> Table.delete x
diff -r 5e9a1d71f94d -r d5803c3d537a src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/General/table.ML	Wed Jul 13 16:42:14 2011 +0200
@@ -30,6 +30,7 @@
   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
+  val lookup_key: 'a table -> key -> (key * 'a) option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
   val update: key * 'a -> 'a table -> 'a table
@@ -161,25 +162,27 @@
 
 (* lookup *)
 
-fun lookup tab key =
+fun lookup_key tab key =
   let
     fun look Empty = NONE
       | look (Branch2 (left, (k, x), right)) =
           (case Key.ord (key, k) of
             LESS => look left
-          | EQUAL => SOME x
+          | EQUAL => SOME (k, x)
           | GREATER => look right)
       | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
           (case Key.ord (key, k1) of
             LESS => look left
-          | EQUAL => SOME x1
+          | EQUAL => SOME (k1, x1)
           | GREATER =>
               (case Key.ord (key, k2) of
                 LESS => look mid
-              | EQUAL => SOME x2
+              | EQUAL => SOME (k2, x2)
               | GREATER => look right));
   in look tab end;
 
+fun lookup tab key = Option.map #2 (lookup_key tab key);
+
 fun defined tab key =
   let
     fun def Empty = false
diff -r 5e9a1d71f94d -r d5803c3d537a src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/sorts.ML	Wed Jul 13 16:42:14 2011 +0200
@@ -185,8 +185,8 @@
 (* certify *)
 
 fun certify_class algebra c =
-  if can (Graph.get_node (classes_of algebra)) c then c
-  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
+  #1 (Graph.get_entry (classes_of algebra) c)
+    handle Graph.UNDEF _ => raise TYPE ("Undeclared class: " ^ quote c, [], []);
 
 fun certify_sort classes = map (certify_class classes);