<commit_before>/*  Title:      Tools/Graphview/src/main_panel.scala
    Author:     <NAME>, TU Muenchen

Graph Panel wrapper.
*/

package isabelle.graphview


import isabelle._
import isabelle.graphview.Mutators._

import scala.collection.JavaConversions._
import scala.swing.{BorderPanel, Button, BoxPanel,
  Orientation, Swing, CheckBox, Action, FileChooser}

import java.io.File
import java.awt.{Color, Dimension}
import java.awt.geom.Rectangle2D
import java.awt.image.BufferedImage
import javax.imageio.ImageIO
import javax.swing.border.EmptyBorder
import javax.swing.JComponent


class Main_Panel(graph: Model.Graph)
  extends BorderPanel
{
  focusable = true
  requestFocus()

  val model = new Model(graph)
  val visualizer = new Visualizer(model)

  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
    "<html><pre style=\"font-family: " + visualizer.font_family +
      "; font-size: " + visualizer.tooltip_font_size + "px; \">" +
      HTML.encode(Pretty.string_of(body)) + "</pre></html>"

  val graph_panel = new Graph_Panel(visualizer, make_tooltip)

  listenTo(keys)
  reactions += graph_panel.reactions

  val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)

  val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")

  private val chooser = new FileChooser()
  chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
  chooser.title = "Graph export"

  val options_panel = new BoxPanel(Orientation.Horizontal) {<commit_msg>unused;<commit_after>/*  Title:      Tools/Graphview/src/main_panel.scala
    Author:     <NAME>, TU Muenchen

Graph Panel wrapper.
*/

package isabelle.graphview


import isabelle._
import isabelle.graphview.Mutators._

import scala.collection.JavaConversions._
import scala.swing.{BorderPanel, Button, BoxPanel,
  Orientation, Swing, CheckBox, Action, FileChooser}

import java.io.File
import java.awt.{Color, Dimension}
import java.awt.geom.Rectangle2D
import java.awt.image.BufferedImage
import javax.imageio.ImageIO
import javax.swing.border.EmptyBorder
import javax.swing.JComponent


class Main_Panel(graph: Model.Graph)
  extends BorderPanel
{
  focusable = true
  requestFocus()

  val model = new Model(graph)
  val visualizer = new Visualizer(model)

  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
  val graph_panel = new Graph_Panel(visualizer, make_tooltip)

  listenTo(keys)
  reactions += graph_panel.reactions

  val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)

  val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")

  private val chooser = new FileChooser()
  chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
  chooser.title = "Graph export"

  val options_panel = new BoxPanel(Orientation.Horizontal) {
{'fraction_non_alphanumeric': 0.10314987885081343, 'fraction_numerical': 0.0006922810661128419, 'mean_word_length': 4.862068965517241, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3212025', 'n_tokens_mistral': 945, 'n_tokens_neox': 910, 'n_words': 217}