Added a way to change dynamically coqtop arguments in CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 39 insertions, 1 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 9987ed2109..27566c6cab 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -274,7 +274,7 @@ type reset_kind = Planned | Unexpected
 
 type coqtop = {
   (* non quoted command-line arguments of coqtop *)
-  sup_args : string list;
+  mutable sup_args : string list;
   (* called whenever coqtop dies *)
   mutable reset_handler : reset_kind -> unit task;
   (* called whenever coqtop sends a feedback message *)
@@ -535,6 +535,12 @@ let break_coqtop coqtop =
   try !interrupter coqtop.handle.pid
   with _ -> Minilib.log "Error while sending Ctrl-C"
 
+let get_arguments coqtop = coqtop.sup_args
+
+let set_arguments coqtop args =
+  coqtop.sup_args <- args;
+  reset_coqtop coqtop
+
 let process_task coqtop task =
   assert (coqtop.status = Ready || coqtop.status = New);
   coqtop.status <- Busy;
diff --git a/ide/coq.mli b/ide/coq.mli
index 84ef466d72..ed78e96e28 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -80,6 +80,12 @@ val reset_coqtop : coqtop -> unit
 (** Reset coqtop. Pending requests will be discarded. The reset handler
     of coqtop will be called with [Planned] as first argument *)
 
+val get_arguments : coqtop -> string list
+(** Get the current arguments used by coqtop. *)
+
+val set_arguments : coqtop -> string list -> unit
+(** Set process arguments. This also forces a planned reset. *)
+
 (** In win32, we'll use a different kill function than Unix.kill *)
 
 val killer : (int -> unit) ref
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8cca8eb9ad..c5b6080ffb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -714,6 +714,28 @@ let about _ =
   let comment _ = notebook#current_term.script#comment ()
   let uncomment _ = notebook#current_term.script#uncomment ()
 
+let coqtop_arguments _ =
+  let dialog = GWindow.dialog ~title:"Coqtop arguments" () in
+  let coqtop = notebook#current_term.coqtop in
+  (** Text entry *)
+  let args = Coq.get_arguments coqtop in
+  let text = String.concat " " args in
+  let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in
+  (** Buttons *)
+  let box = dialog#action_area in
+  let ok = GButton.button ~stock:`OK ~packing:box#add () in
+  let ok_cb () =
+    let nargs = CString.split ' ' entry#text in
+    let () = if nargs <> args then Coq.set_arguments coqtop nargs in
+    dialog#destroy ()
+  in
+  let _ = entry#connect#activate ok_cb in
+  let _ = ok#connect#clicked ok_cb in
+  let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in
+  let cancel_cb () = dialog#destroy () in
+  let _ = cancel#connect#clicked cancel_cb in
+  dialog#show ()
+
 end
 
 (** Refresh functions *)
@@ -1095,6 +1117,8 @@ let build_ui () =
       ~callback:MiscMenu.comment;
     item "Uncomment" ~label:"_Uncomment" ~accel:"<CTRL><SHIFT>D"
       ~callback:MiscMenu.uncomment;
+    item "Coqtop arguments" ~label:"Coqtop _arguments"
+      ~callback:MiscMenu.coqtop_arguments;
   ];
 
   menu compile_menu [
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 72bad7926e..6b9517a844 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -125,6 +125,8 @@ let init () =
   <menu name='Tools' action='Tools'>
     <menuitem action='Comment' />
     <menuitem action='Uncomment' />
+    <separator />
+    <menuitem action='Coqtop arguments' />
   </menu>
   <menu action='Compile'>
     <menuitem action='Compile buffer' />