Accueil Explorer Aide
S'inscrire Connexion
GraphDrawer
/
NodeShuffler
3
2
Fork 0
Fichiers Tickets 0 Pull Requests 0 Wiki
Parcourir la source

bessere darstellung von Arrays in debug tooltips

Kolja Strohm il y a 6 ans
Parent
047672092b
commit
3a2debe2fe
5 fichiers modifiés avec 16 ajouts et 27 suppressions
Vue unifiée Afficher les stats Diff
  1. 5 0
      src/graph/LayeredEdge.java
  2. 7 0
      src/graph/LayeredNode.java
  3. 2 1
      src/lib/TextLayoutHelper.java
  4. 1 1
      src/view/MainView.java
  5. 1 25
      src/view/PseudoCodeRenderer.java

+ 5 - 0
src/graph/LayeredEdge.java
Voir le fichier 

@@ -349,4 +349,9 @@ public class LayeredEdge implements LayeredGraphEdge {
 
     public boolean isReversedEdge() {
 
     public boolean isReversedEdge() {
 
         return reversed;
 
         return reversed;
 
     }
 
     }
 
+    
+    @Override
 
+    public String toString() {
 
+        return "(" + sources.get( 0 ).toString() + "," + targets.get( 0 ).toString() + ")";
 
+    }
 
 }
 
 }

+ 7 - 0
src/graph/LayeredNode.java
Voir le fichier 

@@ -964,4 +964,11 @@ public class LayeredNode implements LayeredGraphNode {
 
     public void setParent(LayeredGraphNode parent) {
 
     public void setParent(LayeredGraphNode parent) {
 
         this.parent = parent;
 
         this.parent = parent;
 
     }
 
     }
 
+    
+    @Override
 
+    public String toString() {
 
+        if( name != null )
 
+            return name;
 
+        return "unnamed node";
 
+    }
 
 }
 
 }

+ 2 - 1
src/lib/TextLayoutHelper.java
Voir le fichier 

@@ -68,7 +68,8 @@ public class TextLayoutHelper {
 
         Matcher m = Pattern.compile( "<font color=#3BB9FF>(.*?)</font>" ).matcher( s );
 
         Matcher m = Pattern.compile( "<font color=#3BB9FF>(.*?)</font>" ).matcher( s );
 
         while( m.find())
 
         while( m.find())
 
         {
 
         {
 
-            list.add( s.substring( m.start( 1 ), m.end( 1 ) ) );
 
+            if( !list.contains( s.substring( m.start( 1 ), m.end( 1 ) ) ) )
 
+                list.add( s.substring( m.start( 1 ), m.end( 1 ) ) );
 
         }
 
         }
 
         return list.toArray( new String[ list.size() ] );
 
         return list.toArray( new String[ list.size() ] );
 
     }
 
     }

+ 1 - 1
src/view/MainView.java
Voir le fichier 

@@ -585,7 +585,7 @@ public class MainView {
 
         {
 
         {
 
             double factor = (graph.getHeight( LayoutType.TOP_BOTTOM_LEFT ) * 2) / (frame.getHeight()-50);
 
             double factor = (graph.getHeight( LayoutType.TOP_BOTTOM_LEFT ) * 2) / (frame.getHeight()-50);
 
             frame.setSize( (int)((frame.getWidth() - 450) / factor) + 450, frame.getHeight() );
 
             frame.setSize( (int)((frame.getWidth() - 450) / factor) + 450, frame.getHeight() );
 
-            spane.setDividerLocation( frame.getWidth() - 330 );
 
+            spane.setDividerLocation( frame.getWidth() - 430 );
 
         }
 
         }
 
 
 
         optionsDialog = new OptionsDialog();
 
         optionsDialog = new OptionsDialog();

+ 1 - 25
src/view/PseudoCodeRenderer.java
Voir le fichier 

@@ -143,31 +143,7 @@ public class PseudoCodeRenderer extends DefaultTreeCellRenderer {
 
             if( mem != null && mem.isSomewhereDefined( var, MemoryType.LOCAL ) )
 
             if( mem != null && mem.isSomewhereDefined( var, MemoryType.LOCAL ) )
 
             {
 
             {
 
                 Object val = mem.read( var, MemoryType.LOCAL );
 
                 Object val = mem.read( var, MemoryType.LOCAL );
 
-                String sVal = "";
 
-                if( val instanceof LayeredGraphNode )
 
-                {
 
-                    if( ((LayeredGraphNode)val).getName() == null )
 
-                        sVal = "unnamed Node";
 
-                    else
 
-                        sVal = ((LayeredGraphNode)val).getName();
 
-                }
 
-                else if( val instanceof LayeredGraphEdge )
 
-                {
 
-                    sVal = "(";
 
-                    if( ((LayeredGraphEdge)val).getSources().get( 0 ).getName() == null )
 
-                        sVal += "unnamed Node";
 
-                    else
 
-                        sVal += ((LayeredGraphEdge)val).getSources().get( 0 ).getName();
 
-                    sVal += ",";
 
-                    if( ((LayeredGraphEdge)val).getTargets().get( 0 ).getName() == null )
 
-                        sVal += "unnamed Node";
 
-                    else
 
-                        sVal += ((LayeredGraphEdge)val).getTargets().get( 0 ).getName();
 
-                    sVal += ")";
 
-                }
 
-                else
 
-                    sVal = val.toString();
 
-                toolTip += var + "=" + sVal + "<br>";
 
+                toolTip += var + "=" + val.toString() + "<br>";
 
             }
 
             }
 
         }
 
         }
 
         if( toolTip.equals( "<html>" ) )
 
         if( toolTip.equals( "<html>" ) )