← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to ide/utils/editable_cells.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
ide/utils/editable_cells.ml
 
1
open GTree
 
2
open Gobject
 
3
 
 
4
let create l = 
 
5
  let hbox = GPack.hbox () in
 
6
  let scw = GBin.scrolled_window 
 
7
              ~hpolicy:`AUTOMATIC 
 
8
              ~vpolicy:`AUTOMATIC 
 
9
              ~packing:(hbox#pack ~expand:true) () in
 
10
 
 
11
  let columns = new GTree.column_list in
 
12
  let command_col =  columns#add Data.string in
 
13
  let coq_col = columns#add Data.string in
 
14
  let store = GTree.list_store columns
 
15
  in 
 
16
 
 
17
(* populate the store *)
 
18
  let _ = List.iter (fun (x,y) -> 
 
19
                       let row = store#append () in
 
20
                       store#set ~row ~column:command_col x;
 
21
                       store#set ~row ~column:coq_col y)
 
22
            l
 
23
  in
 
24
  let view = GTree.view ~model:store ~packing:scw#add_with_viewport () in
 
25
 
 
26
  (* Alternate colors for the rows *)
 
27
  view#set_rules_hint true;
 
28
 
 
29
  let renderer_comm = GTree.cell_renderer_text [`EDITABLE true]  in
 
30
  ignore (renderer_comm#connect#edited 
 
31
    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
 
32
                 store#set 
 
33
                 ~row:(store#get_iter path) 
 
34
                 ~column:command_col s));
 
35
  let first = 
 
36
    GTree.view_column ~title:"Coq Command to try" 
 
37
      ~renderer:(renderer_comm,["text",command_col]) 
 
38
      () 
 
39
  in ignore (view#append_column first);
 
40
 
 
41
  let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in
 
42
  ignore(renderer_coq#connect#edited
 
43
           ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
 
44
                        store#set 
 
45
                        ~row:(store#get_iter path) 
 
46
                        ~column:coq_col s));
 
47
  let second = 
 
48
    GTree.view_column ~title:"Coq Command to insert" 
 
49
      ~renderer:(renderer_coq,["text",coq_col]) 
 
50
      () 
 
51
  in ignore (view#append_column second);
 
52
 
 
53
  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () 
 
54
  in
 
55
  let up = GButton.button  ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
 
56
  let down = GButton.button 
 
57
               ~stock:`GO_DOWN 
 
58
               ~label:"Down" 
 
59
               ~packing:(vbox#pack ~expand:true ~fill:false) () 
 
60
  in
 
61
  let add = GButton.button ~stock:`ADD 
 
62
              ~label:"Add" 
 
63
              ~packing:(vbox#pack ~expand:true ~fill:false) 
 
64
              () 
 
65
  in
 
66
  let remove = GButton.button ~stock:`REMOVE 
 
67
                 ~label:"Remove" 
 
68
                 ~packing:(vbox#pack ~expand:true ~fill:false) () 
 
69
  in
 
70
 
 
71
  ignore (add#connect#clicked 
 
72
            ~callback:(fun b ->  
 
73
                         let n = store#append () in
 
74
                         view#selection#select_iter n));
 
75
  ignore (remove#connect#clicked 
 
76
            ~callback:(fun b -> match view#selection#get_selected_rows with 
 
77
                         | [] -> ()
 
78
                         | path::_ ->
 
79
                             let iter = store#get_iter path in
 
80
                             ignore (store#remove iter);
 
81
                      ));
 
82
  ignore (up#connect#clicked 
 
83
            ~callback:(fun b ->  
 
84
                         match view#selection#get_selected_rows with 
 
85
                           | [] -> ()
 
86
                           | path::_ ->
 
87
                               let iter = store#get_iter path in
 
88
                               ignore (GtkTree.TreePath.prev path);
 
89
                               let upiter = store#get_iter path in
 
90
                               ignore (store#swap iter upiter);
 
91
                      ));
 
92
  ignore (down#connect#clicked 
 
93
            ~callback:(fun b ->  
 
94
                         match view#selection#get_selected_rows with 
 
95
                           | [] -> ()
 
96
                           | path::_ ->
 
97
                               let iter = store#get_iter path in
 
98
                               GtkTree.TreePath.next path;
 
99
                               try let upiter = store#get_iter path in
 
100
                               ignore (store#swap iter upiter)
 
101
                               with _ -> ()
 
102
                      ));
 
103
  let get_data () = 
 
104
    let start_path = GtkTree.TreePath.from_string "0" in
 
105
    let start_iter = store#get_iter start_path in
 
106
    let rec all acc = 
 
107
      let new_acc = (store#get ~row:start_iter ~column:command_col,
 
108
                     store#get ~row:start_iter ~column:coq_col)::acc
 
109
      in      
 
110
      if store#iter_next start_iter then all new_acc else List.rev new_acc
 
111
    in all []
 
112
  in
 
113
  (hbox,get_data)
 
114