src/Tools/Graphview/src/model.scala
author Markus Kaiser <markus.kaiser@in.tum.de>
Mon Sep 24 20:22:58 2012 +0200 (2012-09-24)
changeset 49557 61988f9df94d
child 49565 ea4308b7ef0f
permissions -rw-r--r--
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
markus@49557
     1
/*  Title:      Tools/Graphview/src/model.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
markus@49557
     3
markus@49557
     4
Internal graph representation.
markus@49557
     5
*/
markus@49557
     6
markus@49557
     7
package isabelle.graphview
markus@49557
     8
markus@49557
     9
markus@49557
    10
import isabelle._
markus@49557
    11
import isabelle.graphview.Mutators._
markus@49557
    12
import java.awt.Color
markus@49557
    13
import scala.actors.Actor
markus@49557
    14
import scala.actors.Actor._
markus@49557
    15
markus@49557
    16
markus@49557
    17
class Mutator_Container(val available: List[Mutator[String, Option[Locale]]]) {
markus@49557
    18
    type Mutator_Markup = (Boolean, Color, Mutator[String, Option[Locale]])
markus@49557
    19
    
markus@49557
    20
    val events = new Event_Bus[Mutator_Event.Message]
markus@49557
    21
    
markus@49557
    22
    private var _mutators : List[Mutator_Markup] = Nil
markus@49557
    23
    def apply() = _mutators
markus@49557
    24
    def apply(mutators: List[Mutator_Markup]){
markus@49557
    25
      _mutators = mutators
markus@49557
    26
      
markus@49557
    27
      events.event(Mutator_Event.NewList(mutators))
markus@49557
    28
    }    
markus@49557
    29
markus@49557
    30
    def add(mutator: Mutator_Markup) = {
markus@49557
    31
      _mutators = _mutators ::: List(mutator)
markus@49557
    32
      
markus@49557
    33
      events.event(Mutator_Event.Add(mutator))
markus@49557
    34
    }
markus@49557
    35
}
markus@49557
    36
markus@49557
    37
class Model(private val graph: Graph[String, Option[Locale]]) {  
markus@49557
    38
  val Mutators = new Mutator_Container(
markus@49557
    39
    List(
markus@49557
    40
      Node_Expression(".*", false, false, false),
markus@49557
    41
      Node_List(Nil, false, false, false),
markus@49557
    42
      Edge_Endpoints("", ""),
markus@49557
    43
      Edge_Transitive(),
markus@49557
    44
      Add_Node_Expression(""),
markus@49557
    45
      Add_Transitive_Closure(true, true)
markus@49557
    46
    ))
markus@49557
    47
  
markus@49557
    48
  val Colors = new Mutator_Container(
markus@49557
    49
    List(
markus@49557
    50
      Node_Expression(".*", false, false, false),
markus@49557
    51
      Node_List(Nil, false, false, false)
markus@49557
    52
    ))  
markus@49557
    53
  
markus@49557
    54
  def visible_nodes(): Iterator[String] = current.keys
markus@49557
    55
  
markus@49557
    56
  def visible_edges(): Iterator[(String, String)] =
markus@49557
    57
    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
markus@49557
    58
  
markus@49557
    59
  def complete = graph
markus@49557
    60
  def current: Graph[String, Option[Locale]] =
markus@49557
    61
      (graph /: Mutators()) {
markus@49557
    62
        case (g, (enabled, _, mutator)) => {
markus@49557
    63
          if (!enabled) g
markus@49557
    64
          else mutator.mutate(graph, g)
markus@49557
    65
        }
markus@49557
    66
      }
markus@49557
    67
    
markus@49557
    68
  private var _colors = Map[String, Color]()
markus@49557
    69
  def colors = _colors
markus@49557
    70
  
markus@49557
    71
  private def build_colors() {
markus@49557
    72
    (Map[String, Color]() /: Colors()) ({
markus@49557
    73
        case (colors, (enabled, color, mutator)) => {
markus@49557
    74
            (colors /: mutator.mutate(graph, graph).keys) ({
markus@49557
    75
                case (colors, k) => colors + (k -> color)
markus@49557
    76
              })
markus@49557
    77
          }
markus@49557
    78
    })
markus@49557
    79
  }
markus@49557
    80
  Colors.events += actor {
markus@49557
    81
    loop {
markus@49557
    82
      react {
markus@49557
    83
        case _ => build_colors()
markus@49557
    84
      }
markus@49557
    85
    }
markus@49557
    86
  }
markus@49557
    87
}