src/Pure/General/graph.scala
changeset 48507 1182677e4728
parent 48350 09bf3b73e446
child 48648 f13eeeea1a69
equal deleted inserted replaced
48506:af1dabad14c0 48507:1182677e4728
    37 
    37 
    38 
    38 
    39   /* graphs */
    39   /* graphs */
    40 
    40 
    41   def is_empty: Boolean = rep.isEmpty
    41   def is_empty: Boolean = rep.isEmpty
       
    42   def defined(x: Key): Boolean = rep.isDefinedAt(x)
    42 
    43 
    43   def entries: Iterator[(Key, Entry)] = rep.iterator
    44   def entries: Iterator[(Key, Entry)] = rep.iterator
    44   def keys: Iterator[Key] = entries.map(_._1)
    45   def keys: Iterator[Key] = entries.map(_._1)
    45 
    46 
    46   def dest: List[(Key, List[Key])] =
    47   def dest: List[(Key, List[Key])] =
   153 
   154 
   154 
   155 
   155   /* edge operations */
   156   /* edge operations */
   156 
   157 
   157   def is_edge(x: Key, y: Key): Boolean =
   158   def is_edge(x: Key, y: Key): Boolean =
   158     try { imm_succs(x)(y) }
   159     defined(x) && defined(y) && imm_succs(x)(y)
   159     catch { case _: Graph.Undefined[_] => false }
       
   160 
   160 
   161   def add_edge(x: Key, y: Key): Graph[Key, A] =
   161   def add_edge(x: Key, y: Key): Graph[Key, A] =
   162     if (is_edge(x, y)) this
   162     if (is_edge(x, y)) this
   163     else
   163     else
   164       map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
   164       map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).