aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils/editable_cells.ml
blob: e6d2f4d48c57ebd2fe7b8133e3048d6ce3858523 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
open GTree
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
			       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)