src/Pure/General/graph_display.scala

Using the "constant_on" operator

/*  Title:      Pure/General/graph_display.scala
    Author:     Makarius

Support for graph display.
*/

package isabelle

object Graph_Display
{
  /* graph entries */

  type Entry = ((String, (String, XML.Body)), List[String])  // ident, name, content, parents


  /* graph structure */

  object Node
  {
    val dummy: Node = Node("", "")

    object Ordering extends scala.math.Ordering[Node]
    {
      def compare(node1: Node, node2: Node): Int =
        node1.name compare node2.name match {
          case 0 => node1.ident compare node2.ident
          case ord => ord
        }
    }
  }
  sealed case class Node(name: String, ident: String)
  {
    def is_dummy: Boolean = this == Node.dummy
    override def toString: String = name
  }

  type Edge = (Node, Node)

  type Graph = isabelle.Graph[Node, XML.Body]

  val empty_graph: Graph = isabelle.Graph.empty(Node.Ordering)

  def build_graph(entries: List[Entry]): Graph =
  {
    val node =
      (Map.empty[String, Node] /: entries) {
        case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
      }
    (((empty_graph /: entries) {
        case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
      }) /: entries) {
        case (g1, ((ident, _), parents)) =>
          (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
      }
  }

  def decode_graph(body: XML.Body): Graph =
    build_graph(
      {
        import XML.Decode._
        list(pair(pair(string, pair(string, x => x)), list(string)))(body)
      })
}