diff options
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 8 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
5 files changed, 16 insertions, 2 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 6adeaa705..f127c3034 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -34,3 +34,4 @@ val theories_dirs : string list val contrib_dirs : string list val exec_extension : string (* "" under Unix, ".exe" under MS-windows *) +val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *) @@ -42,6 +42,7 @@ reals_opt=no reals=all arch_spec=no coqide_spec=no +with_geoproof=true COQTOP=`pwd` @@ -110,6 +111,12 @@ while : ; do -coqide|--coqide) coqide_spec=yes COQIDE=$2 shift;; + -with-geoproof|--with-geoproof) + case $2 in + yes) with_geoproof=true;; + no) with_geoproof=false;; + esac + shift;; -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; -debug|--debug) coq_debug_flag=-g;; -profile|--profile) coq_profile_flag=-p;; @@ -483,6 +490,7 @@ let versionsi = "$VERSIONSI" let date = "$DATE" let compile_date = "$COMPILEDATE" let exec_extension = "$EXE" +let with_geoproof = ref $with_geoproof END_OF_COQ_CONFIG diff --git a/ide/coqide.ml b/ide/coqide.ml index 1fb1a6116..2d8291c14 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -3366,7 +3366,7 @@ let start () = Command_windows.main (); Blaster_window.main 9; main files; - ignore (Thread.create check_for_geoproof_input ()); + if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); while true do try GtkThread.main () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 94a70ccda..0dea6415b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -174,7 +174,11 @@ let ide_args = ref [] let parse_args is_ide = let rec parse = function | [] -> () - + | "-with-geoproof" :: s :: rem -> + if s = "yes" then Coq_config.with_geoproof := true + else if s = "no" then Coq_config.with_geoproof := false + else usage (); + parse rem | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 4a1f9e4f2..4944bfede 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -54,6 +54,7 @@ let print_usage_channel co command = -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs -dump-glob f dump globalizations in file f (to be used by coqdoc) + -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) -impredicative-set set sort Set impredicative -dont-load-proofs don't load opaque proofs in memory -xml export XML files either to the hierarchy rooted in |