equal
deleted
inserted
replaced
88 ///event handler for the case when edge map editor tool is active |
88 ///event handler for the case when edge map editor tool is active |
89 bool edgeMapEditEventHandler(GdkEvent*); |
89 bool edgeMapEditEventHandler(GdkEvent*); |
90 ///event handler for the case when node map editor tool is active |
90 ///event handler for the case when node map editor tool is active |
91 bool nodeMapEditEventHandler(GdkEvent*); |
91 bool nodeMapEditEventHandler(GdkEvent*); |
92 |
92 |
|
93 ///event handler for the case when the entry widget is changed |
|
94 bool entryWidgetChangeHandler(GdkEvent*); |
|
95 |
93 public: |
96 public: |
94 ///Moves the text to new place |
97 ///Moves the text to new place |
95 void textReposition(xy<double>); |
98 void textReposition(xy<double>); |
96 ///Activates an edge belonging to a BrokenEdge |
99 ///Activates an edge belonging to a BrokenEdge |
97 void toggleEdgeActivity(BrokenEdge*, bool); |
100 void toggleEdgeActivity(BrokenEdge*, bool); |