Changeset 956

Timestamp:

11/17/10 17:15:16 (3 years ago)

Author:

stefan

Message:

fixed bug #111: selection mark not always removed after search was closed with ESCAPE

Location:

trunk/src

Files:

• jlatexeditor/gproperties/GProperties.java (modified) (1 diff)
• sce/component/SCESearch.java (modified) (2 diffs)

trunk/src/jlatexeditor/gproperties/GProperties.java

@@ -137 +137 @@
     properties.addEntry(new Def("editor.auto_completion.min_number_of_letters", INT_GT_0, "3"));
     properties.addEntry(new Def("editor.auto_completion.delay", INT_GT_0, "200"));
+    properties.addEntry(new Def("editor.clear_selection_when_closing_search", BOOLEAN, "true"));
 
     properties.addEntry(new Comment("\n## Shortcuts"));

trunk/src/sce/component/SCESearch.java

@@ -1 +1 @@
 package sce.component;
+
+import jlatexeditor.gproperties.GProperties;
 
 import javax.swing.*;
@@ -253 +255 @@
       searchPositions.clear();
       // todo: clear selection?
+      if (GProperties.getBoolean("editor.clear_selection_when_closing_search")) {
+        document.clearSelection();
+      }
     }
     clearHighlights(visibility, selectionOnly.isSelected());