open Gobject let create l = let hbox = GPack.hbox () in let scw = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC ~packing:(hbox#pack ~expand:true) () in let columns = new GTree.column_list in let command_col = columns#add Data.string in let coq_col = columns#add Data.string in let store = GTree.list_store columns in (* populate the store *) let _ = List.iter (fun (x,y) -> let row = store#append () in store#set ~row ~column:command_col x; store#set ~row ~column:coq_col y) l in let view = GTree.view ~model:store ~packing:scw#add_with_viewport () in (* Alternate colors for the rows *) view#set_rules_hint true; let renderer_comm = GTree.cell_renderer_text [`EDITABLE true] in ignore (renderer_comm#connect#edited ~callback:(fun (path:Gtk.tree_path) (s:string) -> store#set ~row:(store#get_iter path) ~column:command_col s)); let first = GTree.view_column ~title:"Coq Command to try" ~renderer:(renderer_comm,["text",command_col]) () in ignore (view#append_column first); let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in ignore(renderer_coq#connect#edited ~callback:(fun (path:Gtk.tree_path) (s:string) -> store#set ~row:(store#get_iter path) ~column:coq_col s)); let second = GTree.view_column ~title:"Coq Command to insert" ~renderer:(renderer_coq,["text",coq_col]) () in ignore (view#append_column second); let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () in let up = GButton.button ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in let down = GButton.button ~stock:`GO_DOWN ~label:"Down" ~packing:(vbox#pack ~expand:true ~fill:false) () in let add = GButton.button ~stock:`ADD ~label:"Add" ~packing:(vbox#pack ~expand:true ~fill:false) () in let remove = GButton.button ~stock:`REMOVE ~label:"Remove" ~packing:(vbox#pack ~expand:true ~fill:false) () in ignore (add#connect#clicked ~callback:(fun b -> let n = store#append () in view#selection#select_iter n)); ignore (remove#connect#clicked ~callback:(fun b -> match view#selection#get_selected_rows with | [] -> () | path::_ -> let iter = store#get_iter path in ignore (store#remove iter); )); ignore (up#connect#clicked ~callback:(fun b -> match view#selection#get_selected_rows with | [] -> () | path::_ -> let iter = store#get_iter path in ignore (GtkTree.TreePath.prev path); let upiter = store#get_iter path in ignore (store#swap iter upiter); )); ignore (down#connect#clicked ~callback:(fun b -> match view#selection#get_selected_rows with | [] -> () | path::_ -> let iter = store#get_iter path in GtkTree.TreePath.next path; try let upiter = store#get_iter path in ignore (store#swap iter upiter) with _ -> () )); let get_data () = let start_path = GtkTree.TreePath.from_string "0" in let start_iter = store#get_iter start_path in let rec all acc = let new_acc = (store#get ~row:start_iter ~column:command_col, store#get ~row:start_iter ~column:coq_col)::acc in if store#iter_next start_iter then all new_acc else List.rev new_acc in all [] in (hbox,get_data)