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)
|
