src/Tools/Graphview/src/mutator.scala
changeset 50475 8cc351df4a23
parent 50472 bad1a1ca61e1
child 56372 fadb0fef09d7
equal deleted inserted replaced
50474:6ee044e2d1a7 50475:8cc351df4a23
    32   type Mutator_Markup = (Boolean, Color, Mutator)
    32   type Mutator_Markup = (Boolean, Color, Mutator)
    33   
    33   
    34   val Enabled = true
    34   val Enabled = true
    35   val Disabled = false
    35   val Disabled = false
    36   
    36   
    37   def create(parameters: Parameters, m: Mutator): Mutator_Markup =
    37   def create(visualizer: Visualizer, m: Mutator): Mutator_Markup =
    38     (Mutators.Enabled, parameters.Colors.next, m)
    38     (Mutators.Enabled, visualizer.Colors.next, m)
    39 
    39 
    40   class Graph_Filter(val name: String, val description: String,
    40   class Graph_Filter(val name: String, val description: String,
    41     pred: Model.Graph => Model.Graph)
    41     pred: Model.Graph => Model.Graph)
    42   extends Filter
    42   extends Filter
    43   {
    43   {