aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Command.ml
blob: e0a7427798d951076688dc2d7320021f98642020 (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
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
152
153
154
155
156
157
158
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Preferences

class command_window coqtop =
(*  let window = GWindow.window
		 ~allow_grow:true ~allow_shrink:true
		 ~width:500 ~height:250
		 ~position:`CENTER
		 ~title:"CoqIde queries" ~show:false ()
  in *)
  let views = ref [] in
  let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in
  let _ = frame#misc#hide () in
  let _ = GtkData.AccelGroup.create () in
  let hbox = GPack.hbox ~homogeneous:false ~packing:frame#add () in
  let toolbar = GButton.toolbar
		  ~orientation:`VERTICAL
		  ~style:`ICONS
		  ~tooltips:true
		  ~packing:(hbox#pack
			       ~expand:false
			       ~fill:false)
		  ()
  in
  let notebook = GPack.notebook ~scrollable:true
		   ~packing:(hbox#pack
			       ~expand:true
			       ~fill:true
			    )
		   ()
  in
  let _ =
    toolbar#insert_button
      ~tooltip:"Hide Commands Pane"
      ~text:"Hide Pane"
      ~icon:(Ideutils.stock_to_widget `CLOSE)
      ~callback:frame#misc#hide
      ()
  in
  let new_page_menu =
    toolbar#insert_button
      ~tooltip:"New Page"
      ~text:"New Page"
      ~icon:(Ideutils.stock_to_widget `NEW)
      ()
  in

  let remove_cb () =
    let index = notebook#current_page in
    let () = notebook#remove_page index in
    views := Util.List.filteri (fun i x -> i <> index) !views
  in
  let _ =
    toolbar#insert_button
      ~tooltip:"Delete Page"
      ~text:"Delete Page"
      ~icon:(Ideutils.stock_to_widget `DELETE)
      ~callback:remove_cb
      ()
  in
object(self)
  val frame = frame


  val new_page_menu = new_page_menu
  val notebook = notebook

  method frame = frame
  method new_command ?command ?term () =
    let frame = GBin.frame
		  ~shadow_type:`ETCHED_OUT
		  ()
    in
    let _ = notebook#append_page frame#coerce 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_box_entry_text ~strings:Coq_commands.state_preserving
		  ~packing:hbox#pack
		  ()
    in
    let on_activate c () =
      if List.mem combo#entry#text Coq_commands.state_preserving then c ()
      else Minilib.log "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
    let () = views := !views @ [result] in
    result#misc#modify_font current.text_font;
    let clr = Tags.color_of_string current.background_color in
    result#misc#modify_base [`NORMAL, `COLOR clr];
    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
      let log level message = result#buffer#insert (message^"\n")
      in
      let process =
	Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function
          | Interface.Fail (l,str) ->
            result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
	    Coq.return ()
          | Interface.Good res | Interface.Unsafe res ->
            result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
	    Coq.return ())
      in
      result#buffer#set_text "";
      Coq.try_grab coqtop process ignore
    in
    ignore (combo#entry#connect#activate ~callback:(on_activate callback));
    ignore (ok_b#connect#clicked ~callback:(on_activate callback));

    begin match command with
      | None -> ()
      | Some c -> combo#entry#set_text c
    end;
    begin match term with
      | 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#frame#misc#show ()

  method refresh_font () =
    let iter view = view#misc#modify_font current.text_font in
    List.iter iter !views

  method refresh_color () =
    let clr = Tags.color_of_string current.background_color in
    let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in
    List.iter iter !views

  initializer
    ignore (new_page_menu#connect#clicked ~callback:self#new_command);
   (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
end