graph_displayer_canvas-edge.cc
branchgui
changeset 47 9a0e6e92d06c
parent 45 199f433eb7cd
child 48 b8ec84524fa2
equal deleted inserted replaced
7:0b899270b652 8:5677949c284d
    20       for (EdgeIt i(g); i!=INVALID; ++i)
    20       for (EdgeIt i(g); i!=INVALID; ++i)
    21 	{
    21 	{
    22 	  int w=(int)(*actual_map)[i];
    22 	  int w=(int)(*actual_map)[i];
    23 	  if(w>=0)
    23 	  if(w>=0)
    24 	    {
    24 	    {
    25 	      edgesmap[i]->property_width_pixels().set_value(w);
    25 	      edgesmap[i]->property_width_units().set_value(w);
    26 	    }
    26 	    }
    27 	}
    27 	}
    28     }
    28     }
    29   else
    29   else
    30     {
    30     {
    31       int w=(int)(*actual_map)[edge];
    31       int w=(int)(*actual_map)[edge];
    32       if(w>=0)
    32       if(w>=0)
    33 	{
    33 	{
    34 	  edgesmap[edge]->property_width_pixels().set_value(w);
    34 	  edgesmap[edge]->property_width_units().set_value(w);
    35 	}
    35 	}
    36     }
    36     }
    37   return 0;
    37   return 0;
    38 };
    38 };
    39 
    39