# HG changeset patch
# User wenzelm
# Date 1420119445 -3600
# Node ID d0edf67253d313b50b677aa9f911473ace36fc03
# Parent  e3f90d5c00060d0f8cb9f679f5daf1d96a1198de
tuned imports;

diff -r e3f90d5c0006 -r d0edf67253d3 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 14:21:26 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 14:37:25 2015 +0100
@@ -12,10 +12,11 @@
 import java.awt.{Dimension, Graphics2D, Point, Rectangle}
 import java.awt.geom.{AffineTransform, Point2D}
 import java.awt.image.BufferedImage
-import javax.swing.{JScrollPane, JComponent}
+import javax.swing.{JScrollPane, JComponent, SwingUtilities}
 
 import scala.swing.{Panel, ScrollPane}
-import scala.swing.event._
+import scala.swing.event.{Event, Key, KeyTyped, MousePressed, MouseDragged,
+  MouseMoved, MouseClicked, MouseWheelMoved, MouseEvent}
 
 
 class Graph_Panel(
@@ -170,14 +171,12 @@
   {
     object Keyboard
     {
-      import scala.swing.event.Key._
-
       val react: PartialFunction[Event, Unit] =
       {
         case KeyTyped(_, c, m, _) => typed(c, m)
       }
 
-      def typed(c: Char, m: Modifiers) =
+      def typed(c: Char, m: Key.Modifiers) =
         (c, m) match {
           case ('+', _) => rescale(Transform.scale * 5.0/4)
           case ('-', _) => rescale(Transform.scale * 4.0/5)
@@ -190,8 +189,6 @@
 
     object Mouse
     {
-      import scala.swing.event.Key.Modifier._
-      type Modifiers = Int
       type Dummy = ((String, String), Int)
 
       private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
@@ -237,21 +234,19 @@
         draginfo = (at, l, d)
       }
 
-      def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent)
+      def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent)
       {
-        import javax.swing.SwingUtilities
-
         val c = Transform.pane_to_graph_coordinates(at)
         val p = node(c)
 
         def left_click()
         {
           (p, m) match {
-            case (Some(l), Control) => visualizer.Selection.add(l)
-            case (None, Control) =>
+            case (Some(l), Key.Modifier.Control) => visualizer.Selection.add(l)
+            case (None, Key.Modifier.Control) =>
 
-            case (Some(l), Shift) => visualizer.Selection.add(l)
-            case (None, Shift) =>
+            case (Some(l), Key.Modifier.Shift) => visualizer.Selection.add(l)
+            case (None, Key.Modifier.Shift) =>
 
             case (Some(l), _) => visualizer.Selection.set(List(l))
             case (None, _) => visualizer.Selection.clear
diff -r e3f90d5c0006 -r d0edf67253d3 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Thu Jan 01 14:21:26 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Thu Jan 01 14:37:25 2015 +0100
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.collection.JavaConversions._
 import scala.swing.{BorderPanel, Button, BoxPanel,
   Orientation, Swing, CheckBox, Action, FileChooser}