Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Tools/Graphview/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 11 kB

Quellcode-Bibliothek mutator_dialog.scala Sprache: Scala

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

Mutator selection and configuration dialog.
*/

package isabelle.graphview

import isabelle._

import java.awt.FocusTraversalPolicy
import javax.swing.JColorChooser
import javax.swing.border.EmptyBorder
import scala.swing.{Dialog, Button, BoxPanel, Swing, Orientation, ComboBox, Action,
  Dimension, BorderPanel, ScrollPane, Label, CheckBox, Alignment, Component, TextField}
import scala.swing.event.ValueChanged

class Mutator_Dialog(
    graphview: Graphview,
    container: Mutator_Container,
    caption: String,
    reverse_caption: String = "Inverse",
    show_color_chooser: Boolean = true
) extends Dialog {
  title = caption

  private var _panels: List[Mutator_Panel] = Nil
  private def panels = _panels
  private def panels_=(panels: List[Mutator_Panel]): Unit = {
    _panels = panels
    paint_panels()
  }

  container.events +=
    {
      case Mutator_Event.Message.Add(m) => add_panel(new Mutator_Panel(m))
      case Mutator_Event.Message.New_List(ms) => panels = get_panels(ms)
    }

  override def open(): Unit = {
    if (!visible) panels = get_panels(container())
    super.open()
  }

  minimumSize = new Dimension(700, 200)
  preferredSize = new Dimension(1000, 300)
  peer.setFocusTraversalPolicy(Focus_Traveral_Policy)

  private def get_panels(m: List[Mutator.Info]): List[Mutator_Panel] =
    m.filter({ case Mutator.Info(_, _, Mutator.Identity()) => false case _ => true })
    .map(m => new Mutator_Panel(m))

  private def get_mutators(panels: List[Mutator_Panel]): List[Mutator.Info] =
    panels.map(panel => panel.get_mutator)

  private def movePanelUp(m: Mutator_Panel) = {
    def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] =
      l match {
        case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
        case _ => l
      }

    panels = moveUp(panels)
  }

  private def movePanelDown(m: Mutator_Panel) = {
    def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] =
      l match {
        case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
        case _ => l
      }

    panels = moveDown(panels)
  }

  private def removePanel(m: Mutator_Panel): Unit = {
    panels = panels.filter(_ != m).toList
  }

  private def add_panel(m: Mutator_Panel): Unit = {
    panels = panels ::: List(m)
  }

  def paint_panels(): Unit = {
    Focus_Traveral_Policy.clear()
    filter_panel.contents.clear()
    panels.map { x =>
      filter_panel.contents += x
      Focus_Traveral_Policy.addAll(x.focusList)
    }
    filter_panel.contents += Swing.VGlue

    Focus_Traveral_Policy.add(mutator_box.peer.asInstanceOf[java.awt.Component])
    Focus_Traveral_Policy.add(add_button.peer)
    Focus_Traveral_Policy.add(apply_button.peer)
    Focus_Traveral_Policy.add(cancel_button.peer)
    filter_panel.revalidate()
    filter_panel.repaint()
  }

  val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}

  private val mutator_box = new ComboBox[Mutator](container.available)

  private val add_button = new Button {
    action = Action("Add") {
      add_panel(
        new Mutator_Panel(Mutator.Info(true, graphview.Colors.next(), mutator_box.selection.item)))
    }
  }

  private val apply_button = new Button {
    action = Action("Apply") { container(get_mutators(panels)) }
  }

  private val reset_button = new Button {
    action = Action("Reset") { panels = get_panels(container()) }
  }

  private val cancel_button = new Button {
    action = Action("Close") { close() }
  }
  defaultButton = cancel_button

  private val botPanel = new BoxPanel(Orientation.Horizontal) {
    border = new EmptyBorder(10, 0, 0, 0)

    contents += mutator_box
    contents += Swing.RigidBox(new Dimension(10, 0))
    contents += add_button

    contents += Swing.HGlue
    contents += Swing.RigidBox(new Dimension(30, 0))
    contents += apply_button

    contents += Swing.RigidBox(new Dimension(5, 0))
    contents += reset_button

    contents += Swing.RigidBox(new Dimension(5, 0))
    contents += cancel_button
  }

  contents = new BorderPanel {
    border = new EmptyBorder(5, 5, 5, 5)

    layout(new ScrollPane(filter_panel)) = BorderPanel.Position.Center
    layout(botPanel) = BorderPanel.Position.South
  }

  private class Mutator_Panel(initials: Mutator.Info)
  extends BoxPanel(Orientation.Horizontal) {
    private val inputs: List[(String, Input)] = get_inputs()
    var focusList = List.empty[java.awt.Component]
    private val enabledBox = new Check_Box_Input("Enabled", initials.enabled)

    border = new EmptyBorder(5, 5, 5, 5)
    maximumSize = new Dimension(Int.MaxValue, 30)
    background = initials.color

    contents += new Label(initials.mutator.name) {
      preferredSize = new Dimension(175, 20)
      horizontalAlignment = Alignment.Left
      if (initials.mutator.description != "") tooltip = initials.mutator.description
    }
    contents += Swing.RigidBox(new Dimension(10, 0))
    contents += enabledBox
    contents += Swing.RigidBox(new Dimension(5, 0))
    focusList = enabledBox.peer :: focusList
    inputs.map({
      case (n, c) =>
        contents += Swing.RigidBox(new Dimension(10, 0))
        if (n != "") {
          contents += new Label(n)
          contents += Swing.RigidBox(new Dimension(5, 0))
        }
        contents += c.asInstanceOf[Component]

        focusList = c.asInstanceOf[Component].peer :: focusList
    })

    {
      val t = this
      contents += Swing.HGlue
      contents += Swing.RigidBox(new Dimension(10, 0))

      if (show_color_chooser) {
        contents += new Button {
          maximumSize = new Dimension(20, 20)

          action = Action("Color") {
            t.background =
              JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
          }

          focusList = this.peer :: focusList
        }
        contents += Swing.RigidBox(new Dimension(2, 0))
      }

      contents += new Button {
        maximumSize = new Dimension(20, 20)

        action = Action("Up") {
          movePanelUp(t)
        }

        focusList = this.peer :: focusList
      }
      contents += Swing.RigidBox(new Dimension(2, 0))
      contents += new Button {
        maximumSize = new Dimension(20, 20)

        action = Action("Down") {
          movePanelDown(t)
        }

        focusList = this.peer :: focusList
      }
      contents += Swing.RigidBox(new Dimension(2, 0))
      contents += new Button {
        maximumSize = new Dimension(20, 20)

        action = Action("Del") {
          removePanel(t)
        }

        focusList = this.peer :: focusList
      }
    }

    focusList = focusList.reverse

    def get_mutator: Mutator.Info = {
      val model = graphview.model
      val m =
        initials.mutator match {
          case Mutator.Identity() =>
            Mutator.Identity()
          case Mutator.Node_Expression(r, _, _, _) =>
            val r1 = inputs(2)._2.string
            Mutator.Node_Expression(
              if (Library.make_regex(r1).isDefined) r1 else r,
              inputs(3)._2.bool,
              // "Parents" means "Show parents" or "Matching Children"
              inputs(1)._2.bool,
              inputs(0)._2.bool)
          case Mutator.Node_List(_, _, _, _) =>
            Mutator.Node_List(
              for {
                ident <- space_explode(',', inputs(2)._2.string)
                node <- model.find_node(ident)
              } yield node,
              inputs(3)._2.bool,
              // "Parents" means "Show parents" or "Matching Children"
              inputs(1)._2.bool,
              inputs(0)._2.bool)
          case Mutator.Edge_Endpoints(_) =>
            (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match {
              case (Some(node1), Some(node2)) =>
                Mutator.Edge_Endpoints((node1, node2))
              case _ =>
                Mutator.Identity()
            }
          case Mutator.Add_Node_Expression(r) =>
            val r1 = inputs(0)._2.string
            Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r)
          case Mutator.Add_Transitive_Closure(_, _) =>
            Mutator.Add_Transitive_Closure(
              inputs(0)._2.bool,
              inputs(1)._2.bool)
          case _ =>
            Mutator.Identity()
        }

      Mutator.Info(enabledBox.selected, background, m)
    }

    private def get_inputs(): List[(String, Input)] =
      initials.mutator match {
        case Mutator.Node_Expression(regex, reverse, check_parents, check_children) =>
          List(
            ("", new Check_Box_Input("Parents", check_children)),
            ("", new Check_Box_Input("Children", check_parents)),
            ("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)),
            ("", new Check_Box_Input(reverse_caption, reverse)))
        case Mutator.Node_List(list, reverse, check_parents, check_children) =>
          List(
            ("", new Check_Box_Input("Parents", check_children)),
            ("", new Check_Box_Input("Children", check_parents)),
            ("Names", new Text_Field_Input(list.map(_.ident).mkString(","))),
            ("", new Check_Box_Input(reverse_caption, reverse)))
        case Mutator.Edge_Endpoints((source, dest)) =>
          List(
            ("Source", new Text_Field_Input(source.ident)),
            ("Destination", new Text_Field_Input(dest.ident)))
        case Mutator.Add_Node_Expression(regex) =>
          List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)))
        case Mutator.Add_Transitive_Closure(parents, children) =>
          List(
            ("", new Check_Box_Input("Parents", parents)),
            ("", new Check_Box_Input("Children", children)))
        case _ => Nil
      }
  }

  private trait Input {
    def string: String
    def bool: Boolean
  }

  private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true)
  extends TextField(txt) with Input {
    preferredSize = new Dimension(125, 18)

    private val default_foreground = foreground
    reactions +=
      {
        case ValueChanged(_) =>
          foreground = if (check(text)) default_foreground else graphview.error_color
      }

    def string = text
    def bool = true
  }

  private class Check_Box_Input(txt: String, s: Boolean)
  extends CheckBox(txt) with Input {
    selected = s

    def string = ""
    def bool = selected
  }

  private object Focus_Traveral_Policy extends FocusTraversalPolicy {
    private var items = Vector.empty[java.awt.Component]

    def add(c: java.awt.Component): Unit = { items = items :+ c }
    def addAll(cs: IterableOnce[java.awt.Component]): Unit = { items = items ++ cs }
    def clear(): Unit = { items = Vector.empty }

    def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component = {
      val i = items.indexOf(c)
      if (i < 0) getDefaultComponent(root)
      else items((i + 1) % items.length)
    }

    def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component = {
      val i = items.indexOf(c)
      if (i < 0) getDefaultComponent(root)
      else items((i - 1) % items.length)
    }

    def getFirstComponent(root: java.awt.Container): java.awt.Component =
      if (items.nonEmpty) items(0) else null

    def getDefaultComponent(root: java.awt.Container): java.awt.Component =
      getFirstComponent(root)

    def getLastComponent(root: java.awt.Container): java.awt.Component =
      if (items.nonEmpty) items.last else null
  }
}

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.16Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.