diff options
| -rw-r--r-- | ide/coqide.ml | 37 |
1 files changed, 34 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 1906537f6d..7d664511f1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2060,10 +2060,41 @@ let main files = !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^ " | " ^ !current.cmd_print in - let s,_ = run_command av#insert_message cmd in - !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + let print_window = GWindow.window + ~title:"Print" + ~modal:true + ~position:`CENTER + ~wm_class:"CodIDE" + ~wm_name: "CodIDE" () in + let vbox_print = GPack.vbox + ~spacing:10 + ~border_width:10 + ~packing:print_window#add () in + let _ = GMisc.label + ~justify:`LEFT + ~text:"Print using the following command:" + ~packing:vbox_print#add () in + let print_entry = GEdit.entry + ~text:cmd + ~editable:true + ~width_chars:80 + ~packing:vbox_print#add () in + let hbox_print = GPack.hbox + ~spacing:10 + ~packing:vbox_print#add () in + let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in + let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in + let callback_print () = + let cmd = print_entry#text in + let s,_ = run_command av#insert_message cmd in + !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); + print_window#destroy () + in + ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ; + ignore (print_button#connect#clicked ~callback:callback_print); + print_window#misc#show(); in - let _ = file_factory#add_item "_Print" + let _ = file_factory#add_item "_Print..." ~key:GdkKeysyms._P ~callback:print_f in |