--- a/src/Pure/General/graph.ML Fri Feb 21 21:08:03 2014 +0100
+++ b/src/Pure/General/graph.ML Fri Feb 21 21:27:55 2014 +0100
@@ -35,6 +35,7 @@
val all_preds: 'a T -> key list -> key list
val all_succs: 'a T -> key list -> key list
val strong_conn: 'a T -> key list list
+ val map_strong_conn: ((key * 'a) list -> 'b list) -> 'a T -> 'b T
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val is_minimal: 'a T -> key -> bool
@@ -159,6 +160,15 @@
fun strong_conn G =
rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
+fun map_strong_conn f G =
+ let
+ val xss = strong_conn G;
+ fun map' xs =
+ fold2 (curry Table.update) xs (f (AList.make (get_node G) xs));
+ val tab' = Table.empty
+ |> fold map' xss;
+ in map_nodes (fn x => fn _ => the (Table.lookup tab' x)) G end;
+
(* minimal and maximal elements *)
--- a/src/Tools/Code/code_ml.ML Fri Feb 21 21:08:03 2014 +0100
+++ b/src/Tools/Code/code_ml.ML Fri Feb 21 21:27:55 2014 +0100
@@ -55,7 +55,6 @@
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
val deresolve_const = deresolve o Constant;
- val deresolve_tyco = deresolve o Type_Constructor;
val deresolve_class = deresolve o Type_Class;
val deresolve_classrel = deresolve o Class_Relation;
val deresolve_inst = deresolve o Class_Instance;
@@ -361,7 +360,6 @@
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
val deresolve_const = deresolve o Constant;
- val deresolve_tyco = deresolve o Type_Constructor;
val deresolve_class = deresolve o Type_Class;
val deresolve_classrel = deresolve o Class_Relation;
val deresolve_inst = deresolve o Class_Instance;