Searched refs:gra (Results 1 - 10 of 10) sorted by relevance
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphView.java | 19 Graph gra, gra2; field in class:GraphView 37 public Graph getGraph() { return gra; } 44 gra=(Graph)(gra2.clone()); 53 Graph gra3 = (Graph)gra.clone(); 60 gra.draw(g); 62 size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y); 74 int x = evt.getX() + gra [all...] |
H A D | NormalVertex.java | 71 g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height); 73 g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height); 79 fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY()); 93 g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY()); 99 y<=getY()+gra.box_height); 103 return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0; 107 return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0; 113 int l=gra.box_height*2/3,d=gra.box_height/6; 121 g.fillRect(leftX()+1,getY()+1,gra [all...] |
H A D | Console.java | 33 Graph gra=(Graph)(g.clone()); 37 Vector v=gra.decode(d.getCollapsed()); 39 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed()); 42 g = gra;
|
H A D | Region.java | 17 Graph gra; field in class:Region 19 public Region(Graph g) { gra=g; }
|
H A D | Vertex.java | 23 Graph gra; field in class:Vertex 27 public void setGraph(Graph g) { gra=g; } 182 public int box_width() { return getLabelSize(gra.gfx).width+8; }
|
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphView.java | 19 Graph gra, gra2; field in class:GraphView 37 public Graph getGraph() { return gra; } 44 gra=(Graph)(gra2.clone()); 53 Graph gra3 = (Graph)gra.clone(); 60 gra.draw(g); 62 size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y); 74 int x = evt.getX() + gra [all...] |
H A D | NormalVertex.java | 71 g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height); 73 g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height); 79 fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY()); 93 g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY()); 99 y<=getY()+gra.box_height); 103 return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0; 107 return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0; 113 int l=gra.box_height*2/3,d=gra.box_height/6; 121 g.fillRect(leftX()+1,getY()+1,gra [all...] |
H A D | Console.java | 33 Graph gra=(Graph)(g.clone()); 37 Vector v=gra.decode(d.getCollapsed()); 39 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed()); 42 g = gra;
|
H A D | Region.java | 17 Graph gra; field in class:Region 19 public Region(Graph g) { gra=g; }
|
H A D | Vertex.java | 23 Graph gra; field in class:Vertex 27 public void setGraph(Graph g) { gra=g; } 182 public int box_width() { return getLabelSize(gra.gfx).width+8; }
|
Completed in 39 milliseconds