# HG changeset patch
# User wenzelm
# Date 1355171281 -3600
# Node ID a5930c929b1eedc950de3a44d9c6f0bb942abf70
# Parent  cb73e91bb019c40589f0ec7362cdfb36eb5cf49d
discontinued long names flag -- better done via entity markup, without affecting layout;

diff -r cb73e91bb019 -r a5930c929b1e src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Mon Dec 10 20:52:57 2012 +0100
+++ b/src/Tools/Graphview/src/main_panel.scala	Mon Dec 10 21:28:01 2012 +0100
@@ -68,14 +68,6 @@
         graph_panel.repaint()
       }
     }
-    contents += Swing.RigidBox(new Dimension(10, 0))    
-    contents += new CheckBox(){
-      selected = Parameters.long_names
-      action = Action("Long Names"){
-        Parameters.long_names = selected
-        graph_panel.repaint()
-      }
-    }    
     contents += Swing.RigidBox(new Dimension(10, 0))
     contents += new Button{
       action = Action("Save as PNG"){
diff -r cb73e91bb019 -r a5930c929b1e src/Tools/Graphview/src/parameters.scala
--- a/src/Tools/Graphview/src/parameters.scala	Mon Dec 10 20:52:57 2012 +0100
+++ b/src/Tools/Graphview/src/parameters.scala	Mon Dec 10 21:28:01 2012 +0100
@@ -42,6 +42,5 @@
     val No_Axioms = Color.LIGHT_GRAY
   }
   
-  var long_names = false
   var arrow_heads = false
 }
diff -r cb73e91bb019 -r a5930c929b1e src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 20:52:57 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 21:28:01 2012 +0100
@@ -150,9 +150,7 @@
 
   object Caption
   {
-    def apply(key: String) =
-      if (Parameters.long_names) key
-      else model.complete.get_node(key).name
+    def apply(key: String) = model.complete.get_node(key).name
   }
 
   val font = new Font(Parameters.font_family, Font.BOLD, Parameters.font_size)