# HG changeset patch
# User wenzelm
# Date 1349723840 -7200
# Node ID dfa100466d2e801fd1bf3094e17abde37cb0f4eb
# Parent  30e2f3f1c6232f1f5e71eaa1874d8f24124a86f6
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;

diff -r 30e2f3f1c623 -r dfa100466d2e src/Tools/Graphview/src/parameters.scala
--- a/src/Tools/Graphview/src/parameters.scala	Mon Oct 08 20:39:57 2012 +0200
+++ b/src/Tools/Graphview/src/parameters.scala	Mon Oct 08 21:17:20 2012 +0200
@@ -42,6 +42,6 @@
     val No_Axioms = Color.LIGHT_GRAY
   }
   
-  var long_names = true
+  var long_names = false
   var arrow_heads = false
 }
diff -r 30e2f3f1c623 -r dfa100466d2e src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Mon Oct 08 20:39:57 2012 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala	Mon Oct 08 21:17:20 2012 +0200
@@ -137,9 +137,9 @@
   }  
   
   object Caption {    
-    def apply(k: String) =
-      if (Parameters.long_names) k
-      else  k.split('.').last
+    def apply(key: String) =
+      if (Parameters.long_names) key
+      else model.complete.get_node(key).name
   }
   
   object Font {