discontinued long names flag -- better done via entity markup, without affecting layout;
--- 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"){
--- 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
}
--- 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)