src/Pure/General/graph.ML
changeset 15927 db77bed00211
parent 15759 144c9f9a8ade
child 16003 48ae07a95c70
equal deleted inserted replaced
15926:09fad9a8bc47 15927:db77bed00211
    25   val all_preds: 'a T -> key list -> key list
    25   val all_preds: 'a T -> key list -> key list
    26   val all_succs: 'a T -> key list -> key list
    26   val all_succs: 'a T -> key list -> key list
    27   val strong_conn: 'a T -> key list list
    27   val strong_conn: 'a T -> key list list
    28   val find_paths: 'a T -> key * key -> key list list
    28   val find_paths: 'a T -> key * key -> key list list
    29   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    29   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
       
    30   val update_node : key * 'a -> 'a T -> 'a T
    30   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    31   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    31   val is_edge: 'a T -> key * key -> bool
    32   val is_edge: 'a T -> key * key -> bool
    32   val add_edge: key * key -> 'a T -> 'a T
    33   val add_edge: key * key -> 'a T -> 'a T
    33   val del_edge: key * key -> 'a T -> 'a T
    34   val del_edge: key * key -> 'a T -> 'a T
    34   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
    35   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
   143 (* nodes *)
   144 (* nodes *)
   144 
   145 
   145 fun new_node (x, info) (Graph tab) =
   146 fun new_node (x, info) (Graph tab) =
   146   Graph (Table.update_new ((x, (info, ([], []))), tab));
   147   Graph (Table.update_new ((x, (info, ([], []))), tab));
   147 
   148 
       
   149 fun update_node (x, info) (G as Graph tab) =
       
   150     let val (_, (preds, succs)) = get_entry G x in
       
   151       Graph (Table.update ((x, (info, (preds, succs))), tab))
       
   152     end;
       
   153 
   148 fun del_nodes xs (Graph tab) =
   154 fun del_nodes xs (Graph tab) =
   149   Graph (tab
   155   Graph (tab
   150     |> fold Table.delete xs
   156     |> fold Table.delete xs
   151     |> Table.map (fn (i, (preds, succs)) =>
   157     |> Table.map (fn (i, (preds, succs)) =>
   152       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   158       (i, (fold remove_key xs preds, fold remove_key xs succs))));