Searched refs:gra (Results 1 - 10 of 10) sorted by relevance

/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/
H A DGraphView.java19 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 DNormalVertex.java71 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 DConsole.java33 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 DRegion.java17 Graph gra; field in class:Region
19 public Region(Graph g) { gra=g; }
H A DVertex.java23 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 DGraphView.java19 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 DNormalVertex.java71 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 DConsole.java33 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 DRegion.java17 Graph gra; field in class:Region
19 public Region(Graph g) { gra=g; }
H A DVertex.java23 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