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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: command_windows.ml,v 1.13.2.1 2004/07/16 19:30:19 herbelin Exp $ *)
class command_window () =
let window = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:320 ~height:200
~position:`CENTER
~title:"CoqIde queries" ~show:false ()
in
let accel_group = GtkData.AccelGroup.create () in
let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in
let toolbar = GButton.toolbar
~orientation:`HORIZONTAL
~style:`ICONS
~tooltips:true
~packing:(vbox#pack
~expand:false
~fill:false)
()
in
let notebook = GPack.notebook ~scrollable:true
~packing:(vbox#pack
~expand:true
~fill:true
)
()
in
let _ =
toolbar#insert_button
~tooltip:"Hide Window"
~text:"Hide Window"
~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `CLOSE)
~callback:window#misc#hide
()
in
let new_page_menu =
toolbar#insert_button
~tooltip:"New Page"
~text:"New Page"
~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `NEW)
(*
~callback:window#misc#hide
*)
()
in
let kill_page_menu =
toolbar#insert_button
~tooltip:"Kill Page"
~text:"Kill Page"
~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `DELETE)
~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#goto_page (notebook#page_num frame#coerce);
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
~enable_arrow_keys:true
~allow_empty:false
~value_in_list:false (* true is not ok with disable_activate...*)
~packing:hbox#pack
()
in
combo#disable_activate ();
let on_activate c () =
if List.mem combo#entry#text Coq_commands.state_preserving then c ()
else prerr_endline "Not a state preserving command"
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 com = combo#entry#text in
let phrase =
if String.get com (String.length com - 1) = '.'
then com ^ " " else com ^ " " ^ entry#text ^" . "
in
try
ignore(Coq.interp false phrase);
result#buffer#set_text
("Result for command " ^ phrase ^ ":\n" ^ 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));
ignore (ok_b#connect#clicked ~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;
on_activate 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#clicked 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
|
