aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-28 09:49:48 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-28 09:49:48 +0000
commit7828a2e3c8361b0f04a2bd4fd0127ffcdc87153b (patch)
treed02f238a673ee62853e359c8e5f69247c84f3e8e /ide/coqide.mli
parentc2c3b8cb7c2364c6effc89ab73b3e50874fc616c (diff)
Ide: new option -coqtop <mycoqtop> + remove wrong quoting of args
* Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.mli')
-rw-r--r--ide/coqide.mli13
1 files changed, 12 insertions, 1 deletions
diff --git a/ide/coqide.mli b/ide/coqide.mli
index dd3995eb9..de9eb0238 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -10,9 +10,20 @@
command line, initialize the load path, load the input
state, load the files given on the command line, load the ressource file,
produce the output state if any, and finally will launch the interface. *)
+
+(** The arguments that will be passed to coqtop. No quoting here, since
+ no /bin/sh when using create_process instead of open_process. *)
val sup_args : string list ref
-val do_load : string -> unit
+
+(** Filter the argv from the option -coqtop, and set
+ Minilib.coqtop_path accordingly *)
+val set_coqtop_path : string list -> string list
+
+(** Ask coqtop the remaining options it doesn't recognize *)
val process_argv : string list -> string list
+
+val do_load : string -> unit
+
val crash_save : int -> unit
val ignore_break : unit -> unit
val check_for_geoproof_input : unit -> unit