2002-04-26 05:16:26 -07:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
|
|
|
(* MLTk, Tcl/Tk interface of Objective Caml *)
|
|
|
|
(* *)
|
|
|
|
(* Francois Rouaix, Francois Pessaux, Jun Furuse and Pierre Weis *)
|
|
|
|
(* projet Cristal, INRIA Rocquencourt *)
|
|
|
|
(* Jacques Garrigue, Kyoto University RIMS *)
|
|
|
|
(* *)
|
|
|
|
(* Copyright 2002 Institut National de Recherche en Informatique et *)
|
|
|
|
(* en Automatique and Kyoto University. All rights reserved. *)
|
|
|
|
(* This file is distributed under the terms of the GNU Library *)
|
|
|
|
(* General Public License, with the special exception on linking *)
|
|
|
|
(* described in file LICENSE found in the Objective Caml source tree. *)
|
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
open Camltk
|
|
|
|
|
|
|
|
let version = "$Id$"
|
|
|
|
|
|
|
|
(*
|
|
|
|
* convert an integer to an absolute index
|
|
|
|
*)
|
|
|
|
let abs_index n =
|
|
|
|
TextIndex (LineChar(0,0), [CharOffset n])
|
|
|
|
|
|
|
|
let insertMark =
|
|
|
|
TextIndex(Mark "insert", [])
|
|
|
|
|
|
|
|
let currentMark =
|
|
|
|
TextIndex(Mark "current", [])
|
|
|
|
|
|
|
|
let textEnd =
|
|
|
|
TextIndex(End, [])
|
|
|
|
|
|
|
|
let textBegin =
|
|
|
|
TextIndex (LineChar(0,0), [])
|
|
|
|
|
|
|
|
(*
|
|
|
|
* Link a scrollbar and a text widget
|
|
|
|
*)
|
|
|
|
let scroll_link sb tx =
|
|
|
|
Text.configure tx [YScrollCommand (Scrollbar.set sb)];
|
|
|
|
Scrollbar.configure sb [ScrollCommand (Text.yview tx)]
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
* Tk 4.0 has navigation in Text widgets, sometimes using scrolling
|
|
|
|
* sometimes using the insertion mark. It is a pain to add more
|
|
|
|
* compatible bindings. We do our own.
|
|
|
|
*)
|
|
|
|
let page_up tx = Text.yview tx (ScrollPage (-1))
|
|
|
|
and page_down tx = Text.yview tx (ScrollPage 1)
|
|
|
|
and line_up tx = Text.yview tx (ScrollUnit (-1))
|
|
|
|
and line_down tx = Text.yview tx (ScrollUnit 1)
|
|
|
|
and top tx = Text.yview_index tx textBegin
|
|
|
|
and bottom tx = Text.yview_index tx textEnd
|
|
|
|
|
|
|
|
let navigation_keys tx =
|
|
|
|
let tags = bindtags_get tx in
|
|
|
|
match tags with
|
|
|
|
(WidgetBindings t)::l when t = tx ->
|
2002-07-23 07:12:03 -07:00
|
|
|
bindtags tx ((WidgetBindings tx) :: (TagBindings "TEXT_RO") :: l)
|
2002-04-26 05:16:26 -07:00
|
|
|
| _ -> ()
|
|
|
|
|
|
|
|
let new_scrollable_text top options navigation =
|
|
|
|
let f = Frame.create top [] in
|
|
|
|
let tx = Text.create f options
|
|
|
|
and sb = Scrollbar.create f [] in
|
|
|
|
scroll_link sb tx;
|
|
|
|
(* IN THIS ORDER -- RESIZING *)
|
|
|
|
pack [sb] [Side Side_Right; Fill Fill_Y];
|
|
|
|
pack [tx] [Side Side_Left; Fill Fill_Both; Expand true];
|
|
|
|
if navigation then navigation_keys tx;
|
|
|
|
f, tx
|
|
|
|
|
|
|
|
(*
|
|
|
|
* Searching
|
|
|
|
*)
|
|
|
|
let patternv = Frx_misc.autodef Textvariable.create
|
|
|
|
and casev = Frx_misc.autodef Textvariable.create
|
|
|
|
|
|
|
|
let topsearch t =
|
|
|
|
(* The user interface *)
|
|
|
|
let top = Toplevel.create t [Class "TextSearch"] in
|
|
|
|
Wm.title_set top "Text search";
|
|
|
|
let f = Frame.create_named top "fpattern" [] in
|
|
|
|
let m = Label.create_named f "search" [Text "Search pattern"]
|
|
|
|
and e = Entry.create_named f "pattern"
|
2002-07-23 07:12:03 -07:00
|
|
|
[Relief Sunken; TextVariable (patternv()) ] in
|
2002-04-26 05:16:26 -07:00
|
|
|
let hgroup = Frame.create top []
|
|
|
|
and bgroup = Frame.create top [] in
|
|
|
|
let fdir = Frame.create hgroup []
|
|
|
|
and fmisc = Frame.create hgroup [] in
|
|
|
|
let direction = Textvariable.create_temporary fdir
|
|
|
|
and exactv = Textvariable.create_temporary fdir
|
|
|
|
in
|
|
|
|
let forw = Radiobutton.create_named fdir "forward"
|
2002-07-23 07:12:03 -07:00
|
|
|
[Text "Forward"; Variable direction; Value "f"]
|
2002-04-26 05:16:26 -07:00
|
|
|
and backw = Radiobutton.create_named fdir "backward"
|
2002-07-23 07:12:03 -07:00
|
|
|
[Text "Backward"; Variable direction; Value "b"]
|
2002-04-26 05:16:26 -07:00
|
|
|
and exact = Checkbutton.create_named fmisc "exact"
|
2002-07-23 07:12:03 -07:00
|
|
|
[Text "Exact match"; Variable exactv]
|
2002-04-26 05:16:26 -07:00
|
|
|
and case = Checkbutton.create_named fmisc "case"
|
2002-07-23 07:12:03 -07:00
|
|
|
[Text "Fold Case"; Variable (casev())]
|
2002-04-26 05:16:26 -07:00
|
|
|
and searchb = Button.create_named bgroup "search" [Text "Search"]
|
|
|
|
and contb = Button.create_named bgroup "continue" [Text "Continue"]
|
|
|
|
and dismissb = Button.create_named bgroup "dismiss"
|
2002-07-23 07:12:03 -07:00
|
|
|
[Text "Dismiss";
|
2002-04-26 05:16:26 -07:00
|
|
|
Command (fun () -> Text.tag_delete t ["search"]; destroy top)] in
|
|
|
|
|
|
|
|
Radiobutton.invoke forw;
|
|
|
|
pack [m][Side Side_Left];
|
|
|
|
pack [e][Side Side_Right; Fill Fill_X; Expand true];
|
|
|
|
pack [forw; backw] [Anchor W];
|
|
|
|
pack [exact; case] [Anchor W];
|
|
|
|
pack [fdir; fmisc] [Side Side_Left; Anchor Center];
|
|
|
|
pack [searchb; contb; dismissb] [Side Side_Left; Fill Fill_X];
|
|
|
|
pack [f;hgroup;bgroup] [Fill Fill_X; Expand true];
|
|
|
|
|
|
|
|
let current_index = ref textBegin in
|
|
|
|
|
|
|
|
let search cont = fun () ->
|
|
|
|
let opts = ref [] in
|
|
|
|
if Textvariable.get direction = "f" then
|
2002-07-23 07:12:03 -07:00
|
|
|
opts := Forwards :: !opts
|
2002-04-26 05:16:26 -07:00
|
|
|
else opts := Backwards :: !opts ;
|
|
|
|
if Textvariable.get exactv = "1" then
|
|
|
|
opts := Exact :: !opts;
|
|
|
|
if Textvariable.get (casev()) = "1" then
|
|
|
|
opts := Nocase :: !opts;
|
|
|
|
try
|
|
|
|
let forward = Textvariable.get direction = "f" in
|
|
|
|
let i = Text.search t !opts (Entry.get e)
|
2002-07-23 07:12:03 -07:00
|
|
|
(if cont then !current_index
|
|
|
|
else if forward then textBegin
|
|
|
|
else TextIndex(End, [CharOffset (-1)])) (* does not work with end *)
|
|
|
|
(if forward then textEnd
|
|
|
|
else textBegin) in
|
2002-04-26 05:16:26 -07:00
|
|
|
let found = TextIndex (i, []) in
|
2002-07-23 07:12:03 -07:00
|
|
|
current_index :=
|
|
|
|
TextIndex(i, [CharOffset (if forward then 1 else (-1))]);
|
|
|
|
Text.tag_delete t ["search"];
|
|
|
|
Text.tag_add t "search" found (TextIndex (i, [WordEnd]));
|
|
|
|
Text.tag_configure t "search"
|
|
|
|
[Relief Raised; BorderWidth (Pixels 1);
|
|
|
|
Background Red];
|
|
|
|
Text.see t found
|
2002-04-26 05:16:26 -07:00
|
|
|
with
|
|
|
|
Invalid_argument _ -> Bell.ring() in
|
|
|
|
|
|
|
|
bind e [[], KeyPressDetail "Return"]
|
2002-07-23 07:12:03 -07:00
|
|
|
(BindSet ([], fun _ -> search false ()));
|
2002-04-26 05:16:26 -07:00
|
|
|
Button.configure searchb [Command (search false)];
|
|
|
|
Button.configure contb [Command (search true)];
|
|
|
|
Tkwait.visibility top;
|
|
|
|
Focus.set e
|
|
|
|
|
|
|
|
let addsearch tx =
|
|
|
|
let tags = bindtags_get tx in
|
|
|
|
match tags with
|
|
|
|
(WidgetBindings t)::l when t = tx ->
|
2002-07-23 07:12:03 -07:00
|
|
|
bindtags tx ((WidgetBindings tx) :: (TagBindings "SEARCH") :: l)
|
2002-04-26 05:16:26 -07:00
|
|
|
| _ -> ()
|
|
|
|
|
|
|
|
(* We use Mod1 instead of Meta or Alt *)
|
|
|
|
let init () =
|
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "TEXT_RO" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> page_up ei.ev_Widget; break()))))
|
|
|
|
[
|
|
|
|
[[], KeyPressDetail "BackSpace"];
|
|
|
|
[[], KeyPressDetail "Delete"];
|
|
|
|
[[], KeyPressDetail "Prior"];
|
|
|
|
[[], KeyPressDetail "b"];
|
|
|
|
[[Mod1], KeyPressDetail "v"]
|
|
|
|
];
|
2002-04-26 05:16:26 -07:00
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "TEXT_RO" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> page_down ei.ev_Widget; break()))))
|
|
|
|
[
|
|
|
|
[[], KeyPressDetail "space"];
|
|
|
|
[[], KeyPressDetail "Next"];
|
|
|
|
[[Control], KeyPressDetail "v"]
|
|
|
|
];
|
2002-04-26 05:16:26 -07:00
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "TEXT_RO" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> line_up ei.ev_Widget; break()))))
|
|
|
|
[
|
|
|
|
[[], KeyPressDetail "Up"];
|
|
|
|
[[Mod1], KeyPressDetail "z"]
|
|
|
|
];
|
2002-04-26 05:16:26 -07:00
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "TEXT_RO" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> line_down ei.ev_Widget; break()))))
|
|
|
|
[
|
|
|
|
[[], KeyPressDetail "Down"];
|
|
|
|
[[Control], KeyPressDetail "z"]
|
|
|
|
];
|
2002-04-26 05:16:26 -07:00
|
|
|
|
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "TEXT_RO" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> top ei.ev_Widget; break()))))
|
|
|
|
[
|
|
|
|
[[], KeyPressDetail "Home"];
|
|
|
|
[[Mod1], KeyPressDetail "less"]
|
|
|
|
];
|
2002-04-26 05:16:26 -07:00
|
|
|
|
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "TEXT_RO" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> bottom ei.ev_Widget; break()))))
|
|
|
|
[
|
|
|
|
[[], KeyPressDetail "End"];
|
|
|
|
[[Mod1], KeyPressDetail "greater"]
|
|
|
|
];
|
2002-04-26 05:16:26 -07:00
|
|
|
|
|
|
|
List.iter (function ev ->
|
2002-07-23 07:12:03 -07:00
|
|
|
tag_bind "SEARCH" ev
|
|
|
|
(BindSetBreakable ([Ev_Widget],
|
|
|
|
(fun ei -> topsearch ei.ev_Widget; break()))))
|
|
|
|
[
|
2002-04-26 05:16:26 -07:00
|
|
|
[[Control], KeyPressDetail "s"]
|
2002-07-23 07:12:03 -07:00
|
|
|
]
|
2002-04-26 05:16:26 -07:00
|
|
|
|