# HG changeset patch
# User wenzelm
# Date 1420058730 -3600
# Node ID ecf64bc6977813369d0e1dfee297b3e10c3ac10d
# Parent  7b74e84087117c7568b82f0146d2fed799c48e13
converse graph according to Graph_Display;

diff -r 7b74e8408711 -r ecf64bc69778 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Wed Dec 31 20:55:11 2014 +0100
+++ b/src/Pure/General/graph.scala	Wed Dec 31 21:45:30 2014 +0100
@@ -21,13 +21,15 @@
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
-  def make[Key, A](entries: List[((Key, A), List[Key])])(implicit ord: Ordering[Key])
-    : Graph[Key, A] =
+  def make[Key, A](entries: List[((Key, A), List[Key])], converse: Boolean = false)(
+    implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
     val graph2 =
-      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
+      (graph1 /: entries) { case (graph, ((x, _), ys)) =>
+        if (converse) (graph /: ys)(_.add_edge(_, x)) else (graph /: ys)(_.add_edge(x, _))
+      }
     graph2
   }
 
@@ -44,11 +46,11 @@
       list(pair(pair(key, info), list(key)))(graph.dest)
     })
 
-  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(implicit ord: Ordering[Key])
-      : XML.Decode.T[Graph[Key, A]] =
+  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A], converse: Boolean = false)(
+    implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
     ((body: XML.Body) => {
       import XML.Decode._
-      make(list(pair(pair(key, info), list(key)))(body))(ord)
+      make(list(pair(pair(key, info), list(key)))(body), converse)(ord)
     })
 }
 
diff -r 7b74e8408711 -r ecf64bc69778 src/Tools/Graphview/model.scala
--- a/src/Tools/Graphview/model.scala	Wed Dec 31 20:55:11 2014 +0100
+++ b/src/Tools/Graphview/model.scala	Wed Dec 31 21:45:30 2014 +0100
@@ -56,7 +56,7 @@
   type Graph = isabelle.Graph[String, Info]
 
   val decode_graph: XML.Decode.T[Graph] =
-    isabelle.Graph.decode(XML.Decode.string, decode_info)
+    isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
 }
 
 class Model(private val graph: Model.Graph) {