src/Tools/Graphview/model.scala

tuned headers;

/*  Title:      Tools/Graphview/model.scala
    Author:     Markus Kaiser, TU Muenchen
    Author:     Makarius

Internal graph representation.
*/

package isabelle.graphview


import isabelle._

import java.awt.Color


class Mutator_Container(val available: List[Mutator])
{
  val events = new Mutator_Event.Bus

  private var _mutators : List[Mutator.Info] = Nil
  def apply() = _mutators
  def apply(mutators: List[Mutator.Info])
  {
    _mutators = mutators
    events.event(Mutator_Event.New_List(mutators))
  }

  def add(mutator: Mutator.Info)
  {
    _mutators = _mutators ::: List(mutator)
    events.event(Mutator_Event.Add(mutator))
  }
}


object Model
{
  /* node info */

  sealed case class Info(name: String, content: XML.Body)

  val empty_info: Info = Info("", Nil)

  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
  {
    import XML.Decode._

    val (name, content) = pair(string, x => x)(body)
    Info(name, content)
  }


  /* graph */

  type Graph = isabelle.Graph[String, Info]

  val decode_graph: XML.Decode.T[Graph] =
    isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
}

class Model(val complete_graph: Model.Graph)
{
  val Mutators =
    new Mutator_Container(
      List(
        Mutator.Node_Expression(".*", false, false, false),
        Mutator.Node_List(Nil, false, false, false),
        Mutator.Edge_Endpoints("", ""),
        Mutator.Add_Node_Expression(""),
        Mutator.Add_Transitive_Closure(true, true)))

  val Colors =
    new Mutator_Container(
      List(
        Mutator.Node_Expression(".*", false, false, false),
        Mutator.Node_List(Nil, false, false, false)))

  def visible_nodes_iterator: Iterator[String] = current_graph.keys_iterator

  def visible_edges_iterator: Iterator[(String, String)] =
    current_graph.keys_iterator.flatMap(k => current_graph.imm_succs(k).iterator.map((k, _)))

  def current_graph: Model.Graph =
    (complete_graph /: Mutators()) {
      case (g, m) => if (!m.enabled) g else m.mutator.mutate(complete_graph, g)
    }

  private var _colors = Map.empty[String, Color]
  def colors = _colors

  private def build_colors()
  {
    _colors =
      (Map.empty[String, Color] /: Colors()) {
        case (colors, m) =>
          (colors /: m.mutator.mutate(complete_graph, complete_graph).keys_iterator) {
            case (colors, k) => colors + (k -> m.color)
          }
      }
  }
  Colors.events += { case _ => build_colors() }
}