graph_displayer_canvas-edge.cc
branchgui
changeset 75 d5aadf09197b
parent 62 80eefca04b1e
child 81 5ad61c33487c
equal deleted inserted replaced
13:de3028325d67 14:feeddff356fe
   120 {
   120 {
   121   //the number in the map will be written on the edge
   121   //the number in the map will be written on the edge
   122   //EXCEPT when the name of the map is Default, because
   122   //EXCEPT when the name of the map is Default, because
   123   //in that case empty string will be written, because
   123   //in that case empty string will be written, because
   124   //that is the deleter map
   124   //that is the deleter map
   125 
   125   
   126   if(edge==INVALID)
   126   if(edge==INVALID)
   127     {
   127     {
   128       for (EdgeIt i(mapstorage.graph); i!=INVALID; ++i)
   128       for (EdgeIt i(mapstorage.graph); i!=INVALID; ++i)
   129 	{
   129 	{
   130 	  if(mapname!="Default")
   130 	  if(mapname!="Default")