diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:15 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:15 +0000 |
| commit | 6a43dd3dc162412fbd9a9863840536b01043937d (patch) | |
| tree | f63d5a55b57eb852eb88e23135a26d735c968036 /ide/wg_Find.mli | |
| parent | ad4343b8daf31569fe46c53032ce5fc409076672 (diff) | |
Wg_Find: regex + case insensitive find/replace support
It uses Str, hence it also supports captures \(..\) and \1 .. \n
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_Find.mli')
| -rw-r--r-- | ide/wg_Find.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli index 5337dae7c..a8e734887 100644 --- a/ide/wg_Find.mli +++ b/ide/wg_Find.mli @@ -6,13 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type mode = [ `FIND | `REPLACE ] - -class finder : GText.view -> +class finder : string -> GText.view -> object method coerce : GObj.widget method hide : unit -> unit - method show : mode -> unit + method show : unit -> unit method replace : unit -> unit method replace_all : unit -> unit method find_backward : unit -> unit |