1999-12-16 04:25:11 -08:00
|
|
|
(*************************************************************************)
|
|
|
|
(* *)
|
|
|
|
(* Objective Caml LablTk library *)
|
|
|
|
(* *)
|
|
|
|
(* Jacques Garrigue, Kyoto University RIMS *)
|
|
|
|
(* *)
|
|
|
|
(* Copyright 1999 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. *)
|
|
|
|
(* *)
|
|
|
|
(*************************************************************************)
|
|
|
|
|
1999-11-30 06:59:39 -08:00
|
|
|
(* $Id$ *)
|
|
|
|
|
|
|
|
open Tk
|
|
|
|
|
|
|
|
(* Listboxes *)
|
|
|
|
|
|
|
|
let update_hooks = ref []
|
|
|
|
|
|
|
|
let add_update_hook f = update_hooks := f :: !update_hooks
|
|
|
|
|
|
|
|
let exec_update_hooks () =
|
2000-04-11 20:43:25 -07:00
|
|
|
update_hooks := List.filter !update_hooks ~f:
|
1999-11-30 06:59:39 -08:00
|
|
|
begin fun f ->
|
|
|
|
try f (); true
|
|
|
|
with Protocol.TkError _ -> false
|
|
|
|
end
|
|
|
|
|
|
|
|
let set_load_path l =
|
|
|
|
Config.load_path := l;
|
|
|
|
exec_update_hooks ()
|
|
|
|
|
|
|
|
let get_load_path () = !Config.load_path
|
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
let renew_dirs box ~var ~dir =
|
2000-04-02 18:57:52 -07:00
|
|
|
Textvariable.set var dir;
|
2000-04-11 20:43:25 -07:00
|
|
|
Listbox.delete box ~first:(`Num 0) ~last:`End;
|
|
|
|
Listbox.insert box ~index:`End
|
|
|
|
~texts:(Useunix.get_directories_in_files ~path:dir
|
1999-11-30 06:59:39 -08:00
|
|
|
(Useunix.get_files_in_directory dir));
|
2000-04-11 20:43:25 -07:00
|
|
|
Jg_box.recenter box ~index:(`Num 0)
|
1999-11-30 06:59:39 -08:00
|
|
|
|
|
|
|
let renew_path box =
|
2000-04-11 20:43:25 -07:00
|
|
|
Listbox.delete box ~first:(`Num 0) ~last:`End;
|
|
|
|
Listbox.insert box ~index:`End ~texts:!Config.load_path;
|
|
|
|
Jg_box.recenter box ~index:(`Num 0)
|
1999-11-30 06:59:39 -08:00
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
let add_to_path ~dirs ?(base="") box =
|
1999-11-30 06:59:39 -08:00
|
|
|
let dirs =
|
|
|
|
if base = "" then dirs else
|
|
|
|
if dirs = [] then [base] else
|
2000-04-11 20:43:25 -07:00
|
|
|
List.map dirs ~f:
|
1999-11-30 06:59:39 -08:00
|
|
|
begin function
|
|
|
|
"." -> base
|
|
|
|
| ".." -> Filename.dirname base
|
|
|
|
| x -> base ^ "/" ^ x
|
|
|
|
end
|
|
|
|
in
|
|
|
|
set_load_path
|
2000-04-11 20:43:25 -07:00
|
|
|
(dirs @ List.fold_left dirs ~init:(get_load_path ())
|
|
|
|
~f:(fun acc x -> List2.exclude x acc))
|
1999-11-30 06:59:39 -08:00
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
let remove_path box ~dirs =
|
1999-11-30 06:59:39 -08:00
|
|
|
set_load_path
|
2000-04-11 20:43:25 -07:00
|
|
|
(List.fold_left dirs ~init:(get_load_path ())
|
|
|
|
~f:(fun acc x -> List2.exclude x acc))
|
1999-11-30 06:59:39 -08:00
|
|
|
|
|
|
|
(* main function *)
|
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
let f ~dir =
|
1999-11-30 06:59:39 -08:00
|
|
|
let current_dir = ref dir in
|
|
|
|
let tl = Jg_toplevel.titled "Edit Load Path" in
|
|
|
|
Jg_bind.escape_destroy tl;
|
2000-04-11 20:43:25 -07:00
|
|
|
let var_dir = Textvariable.create ~on:tl () in
|
|
|
|
let caplab = Label.create tl ~text:"Path"
|
|
|
|
and dir_name = Entry.create tl ~textvariable:var_dir
|
1999-11-30 06:59:39 -08:00
|
|
|
and browse = Frame.create tl in
|
|
|
|
let dirs = Frame.create browse
|
|
|
|
and path = Frame.create browse in
|
|
|
|
let dirframe, dirbox, dirsb = Jg_box.create_with_scrollbar dirs
|
|
|
|
and pathframe, pathbox, pathsb = Jg_box.create_with_scrollbar path
|
|
|
|
in
|
|
|
|
add_update_hook (fun () -> renew_path pathbox);
|
2000-04-11 20:43:25 -07:00
|
|
|
Listbox.configure pathbox ~width:40 ~selectmode:`Multiple;
|
|
|
|
Listbox.configure dirbox ~selectmode:`Multiple;
|
|
|
|
Jg_box.add_completion dirbox ~action:
|
1999-11-30 06:59:39 -08:00
|
|
|
begin fun index ->
|
2000-04-11 20:43:25 -07:00
|
|
|
begin match Listbox.get dirbox ~index with
|
1999-11-30 06:59:39 -08:00
|
|
|
"." -> ()
|
|
|
|
| ".." -> current_dir := Filename.dirname !current_dir
|
|
|
|
| x -> current_dir := !current_dir ^ "/" ^ x
|
|
|
|
end;
|
2000-04-11 20:43:25 -07:00
|
|
|
renew_dirs dirbox ~var:var_dir ~dir:!current_dir;
|
|
|
|
Listbox.selection_clear dirbox ~first:(`Num 0) ~last:`End
|
1999-11-30 06:59:39 -08:00
|
|
|
end;
|
2000-04-11 20:43:25 -07:00
|
|
|
Jg_box.add_completion pathbox ~action:
|
1999-11-30 06:59:39 -08:00
|
|
|
begin fun index ->
|
2000-04-11 20:43:25 -07:00
|
|
|
current_dir := Listbox.get pathbox ~index;
|
|
|
|
renew_dirs dirbox ~var:var_dir ~dir:!current_dir
|
1999-11-30 06:59:39 -08:00
|
|
|
end;
|
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
bind dir_name ~events:[`KeyPressDetail"Return"]
|
|
|
|
~action:(fun _ ->
|
1999-11-30 06:59:39 -08:00
|
|
|
let dir = Textvariable.get var_dir in
|
|
|
|
if Useunix.is_directory dir then begin
|
|
|
|
current_dir := dir;
|
2000-04-11 20:43:25 -07:00
|
|
|
renew_dirs dirbox ~var:var_dir ~dir
|
1999-12-16 00:37:38 -08:00
|
|
|
end);
|
1999-12-21 02:54:06 -08:00
|
|
|
|
|
|
|
(* Avoid space being used by the completion mechanism *)
|
1999-11-30 06:59:39 -08:00
|
|
|
let bind_space_toggle lb =
|
2000-04-11 20:43:25 -07:00
|
|
|
bind lb ~events:[`KeyPressDetail "space"] ~extend:true ~action:ignore in
|
1999-12-21 02:54:06 -08:00
|
|
|
bind_space_toggle dirbox;
|
|
|
|
bind_space_toggle pathbox;
|
|
|
|
|
1999-11-30 06:59:39 -08:00
|
|
|
let add_paths _ =
|
2000-04-11 20:43:25 -07:00
|
|
|
add_to_path pathbox ~base:!current_dir
|
|
|
|
~dirs:(List.map (Listbox.curselection dirbox)
|
|
|
|
~f:(fun x -> Listbox.get dirbox ~index:x));
|
|
|
|
Listbox.selection_clear dirbox ~first:(`Num 0) ~last:`End
|
1999-11-30 06:59:39 -08:00
|
|
|
and remove_paths _ =
|
|
|
|
remove_path pathbox
|
2000-04-11 20:43:25 -07:00
|
|
|
~dirs:(List.map (Listbox.curselection pathbox)
|
|
|
|
~f:(fun x -> Listbox.get pathbox ~index:x))
|
1999-11-30 06:59:39 -08:00
|
|
|
in
|
2000-04-11 20:43:25 -07:00
|
|
|
bind dirbox ~events:[`KeyPressDetail "Insert"] ~action:add_paths;
|
|
|
|
bind pathbox ~events:[`KeyPressDetail "Delete"] ~action:remove_paths;
|
1999-11-30 06:59:39 -08:00
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
let dirlab = Label.create dirs ~text:"Directories"
|
|
|
|
and pathlab = Label.create path ~text:"Load path"
|
|
|
|
and addbutton = Button.create dirs ~text:"Add to path" ~command:add_paths
|
1999-11-30 06:59:39 -08:00
|
|
|
and pathbuttons = Frame.create path in
|
|
|
|
let removebutton =
|
2000-04-11 20:43:25 -07:00
|
|
|
Button.create pathbuttons ~text:"Remove from path" ~command:remove_paths
|
1999-11-30 06:59:39 -08:00
|
|
|
and ok =
|
2000-04-11 20:43:25 -07:00
|
|
|
Jg_button.create_destroyer tl ~parent:pathbuttons
|
1999-11-30 06:59:39 -08:00
|
|
|
in
|
2000-04-11 20:43:25 -07:00
|
|
|
renew_dirs dirbox ~var:var_dir ~dir:!current_dir;
|
1999-11-30 06:59:39 -08:00
|
|
|
renew_path pathbox;
|
2000-04-11 20:43:25 -07:00
|
|
|
pack [dirsb] ~side:`Right ~fill:`Y;
|
|
|
|
pack [dirbox] ~side:`Left ~fill:`Y ~expand:true;
|
|
|
|
pack [pathsb] ~side:`Right ~fill:`Y;
|
|
|
|
pack [pathbox] ~side:`Left ~fill:`Both ~expand:true;
|
|
|
|
pack [dirlab] ~side:`Top ~anchor:`W ~padx:10;
|
|
|
|
pack [addbutton] ~side:`Bottom ~fill:`X;
|
|
|
|
pack [dirframe] ~fill:`Y ~expand:true;
|
|
|
|
pack [pathlab] ~side:`Top ~anchor:`W ~padx:10;
|
|
|
|
pack [removebutton; ok] ~side:`Left ~fill:`X ~expand:true;
|
|
|
|
pack [pathbuttons] ~fill:`X ~side:`Bottom;
|
|
|
|
pack [pathframe] ~fill:`Both ~expand:true;
|
|
|
|
pack [dirs] ~side:`Left ~fill:`Y;
|
|
|
|
pack [path] ~side:`Right ~fill:`Both ~expand:true;
|
|
|
|
pack [caplab] ~side:`Top ~anchor:`W ~padx:10;
|
|
|
|
pack [dir_name] ~side:`Top ~anchor:`W ~fill:`X;
|
|
|
|
pack [browse] ~side:`Bottom ~expand:true ~fill:`Both;
|
1999-11-30 06:59:39 -08:00
|
|
|
tl
|
2000-02-15 02:09:55 -08:00
|
|
|
|
2000-04-11 20:43:25 -07:00
|
|
|
let set ~dir = ignore (f ~dir);;
|