blob: 7a08d209c67ee0873087b2aa5d46dba8f22aac0f (
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
115
116
117
118
119
120
121
|
let decompose_tab w =
let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
let l = vbox#children in
match l with
| [img;lbl] ->
let img = new GMisc.image
((Gobject.try_cast img#as_widget "GtkImage"):
Gtk.image Gtk.obj)
in
let lbl = GMisc.label_cast lbl in
vbox,img,lbl
| _ -> assert false
class command_window () =
let window = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:320 ~height:200
~title:"CoqIde Commands" ~show:false ()
in
let accel_group = GtkData.AccelGroup.create () in
let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in
let menubar = GMenu.menu_bar ~packing:vbox#pack () in
let factory = new GMenu.factory menubar
in
let accel_group = factory#accel_group in
let notebook = GPack.notebook ~scrollable:true
~packing:(vbox#pack
~expand:true
~fill:true
)
()
in
let hide_menu = factory#add_item "_Hide Window"
~callback:window#misc#hide
in
let new_page_menu = factory#add_item "_New Page" in
let kill_page_menu =
factory#add_item "_Kill Page"
~callback:
(fun () -> notebook#remove_page notebook#current_page)
in
object(self)
val window = window
val menubar = menubar
val new_page_menu = new_page_menu
val notebook = notebook
method window = window
method new_command ?command ?term () =
let frame = GBin.frame
~shadow_type:`ETCHED_OUT
~packing:notebook#append_page
()
in
notebook#next_page ();
let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving
~use_arrows:`DEFAULT
~ok_if_empty:false
~value_in_list:true
~packing:hbox#pack
()
in
combo#disable_activate ();
let on_activate c () = if List.mem combo#entry#text Coq_commands.state_preserving then c () in
let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
entry#misc#set_can_default true;
let r_bin =
GBin.scrolled_window
~vpolicy:`AUTOMATIC
~hpolicy:`AUTOMATIC
~packing:(vbox#pack ~fill:true ~expand:true) () in
let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in
let result = GText.view ~packing:r_bin#add () in
result#misc#set_can_focus true; (* false causes problems for selection *)
result#set_editable false;
let callback () =
let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in
try
ignore(Coq.interp phrase);
result#buffer#set_text (Ideutils.read_stdout ())
with e ->
let (s,loc) = Coq.process_exn e in
assert (Glib.Utf8.validate s);
result#buffer#set_text s
in
ignore (combo#entry#connect#activate ~callback:(on_activate callback));
begin match command,term with
| None,None -> ()
| Some c, None ->
combo#entry#set_text c;
| Some c, Some t ->
combo#entry#set_text c;
entry#set_text t
| None , Some t ->
entry#set_text t
end;
callback ();
entry#misc#grab_focus ();
entry#misc#grab_default ();
ignore (entry#connect#activate ~callback);
ignore (combo#entry#connect#activate ~callback);
self#window#present ()
initializer
ignore (new_page_menu#connect#activate self#new_command);
ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
end
let command_window = ref None
let main () = command_window := Some (new command_window ())
let command_window () = match !command_window with
| None -> failwith "No command window."
| Some c -> c
|
