From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- ide/utils/editable_cells.ml | 113 -------------------------------------------- 1 file changed, 113 deletions(-) delete mode 100644 ide/utils/editable_cells.ml (limited to 'ide/utils/editable_cells.ml') diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml deleted file mode 100644 index 33968b8d..00000000 --- a/ide/utils/editable_cells.ml +++ /dev/null @@ -1,113 +0,0 @@ -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) - -- cgit v1.2.3