Find and Replace: please add "selected text only" option

[jgroote]

Issue migrated from trac ticket # 1334

component: mcrl2xi | priority: minor | keywords: find, replace, editor

2015-10-01 12:04:27: Gert Veltink [email protected] created the issue

---

Currently the editor only supports changes to the entire document. However, while programming/specifying you often only want the changes in a part of the file and not the entire file. (cf. TextWrangler e.g.) Please consider adding the "selected text only" option.

[jgroote]

2016-11-24 19:38:17: @wiegerw changed status from new to assigned

[jgroote]

2016-11-24 19:38:17: @wiegerw changed owner from rboudewijns,fstapper to jfg

[jgroote]

2016-11-24 19:38:17: @wiegerw

[jgroote]

2016-11-29 17:37:10: @jgroote

[jgroote]

2016-11-29 17:37:10: @jgroote commented

---

This could be a useful option, but it is not an urgent problem to be resolved for the next release. Therefore, I postpone the request to be dealt with at a later moment.

[jgroote]

2017-05-04 15:37:40: @wiegerw changed owner from jfg to tneele