diff options
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rw-r--r-- | configure.ml | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 19 | ||||
| -rw-r--r-- | ide/coqide.mli | 2 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 1 | ||||
| -rw-r--r-- | man/coqtop.1 | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
10 files changed, 1 insertions, 42 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 8bc044c3a..6a834a304 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -61,7 +61,6 @@ val plugins_dirs : string list val all_src_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 *) val browser : string (** default web browser to use, may be overridden by environment diff --git a/configure.ml b/configure.ml index a7acdf532..0952b15f5 100644 --- a/configure.ml +++ b/configure.ml @@ -258,7 +258,6 @@ module Prefs = struct let macintegration = ref true let browser = ref (None : string option) let withdoc = ref false - let geoproof = ref false let byteonly = ref false let flambda_flags = ref [] let debug = ref true @@ -321,8 +320,6 @@ let args_options = Arg.align [ "<command> Use <command> to open URL %s"; "-with-doc", arg_bool Prefs.withdoc, "(yes|no) Compile the documentation or not"; - "-with-geoproof", arg_bool Prefs.geoproof, - "(yes|no) Use Geoproof binding or not"; "-byte-only", Arg.Set Prefs.byteonly, " Compiles only bytecode version of Coq"; "-nodebug", Arg.Clear Prefs.debug, @@ -1073,7 +1070,6 @@ let write_configml f = pr_l "flambda_flags" !Prefs.flambda_flags; pr_i "vo_magic_number" vo_magic; pr_i "state_magic_number" state_magic; - pr "let with_geoproof = ref %B\n" !Prefs.geoproof; pr_s "browser" browser; pr_s "wwwcoq" !Prefs.coqwebsite; pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 892c9931b..8b1fc7c8f 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -214,11 +214,6 @@ The following command-line options are recognized by the commands {\tt % % Switch on the debug flag. -\item[{\tt -with-geoproof} (yes|no)]\ % - - Enable or not special functions for Geoproof within {\CoqIDE} (default - is yes). - \item[{\tt -color} (on|off|auto)]\ % Enable or not the coloring of output of {\tt coqtop}. Default is auto, diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 75f3d18de..436099e74 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -13,8 +13,7 @@ line. Without argument, the main screen is displayed with an ``unnamed buffer'', and with a file name as argument, another buffer displaying the contents of that file. Additionally, \verb|coqide| accepts the same options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having -obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. - +obviously no meaning for \CoqIDE{} being ignored. \begin{figure}[t] \begin{center} diff --git a/ide/coqide.ml b/ide/coqide.ml index 2c8ce0049..842d06859 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1325,25 +1325,6 @@ let main files = Minilib.log "End of Coqide.main" -(** {2 Geoproof } *) - -(** This function check every tenth of second if GeoProof has send - something on his private clipboard *) - -let check_for_geoproof_input () = - let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in - let handler () = match cb_Dr#text with - |None -> true - |Some "Ack" -> true - |Some s -> - on_current_term (fun sn -> sn.buffer#insert (s ^ "\n")); - (* cb_Dr#clear does not work so i use : *) - cb_Dr#set_text "Ack"; - true - in - ignore (GMain.Timeout.add ~ms:100 ~callback:handler) - - (** {2 Argument parsing } *) (** By default, the coqtop we try to launch is exactly the current coqide diff --git a/ide/coqide.mli b/ide/coqide.mli index 39b4d9ae2..42dab9ec5 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -40,5 +40,3 @@ val set_signal_handlers : unit -> unit (** Emergency saving of opened files as "foo.v.crashcoqide", and exit (if the integer isn't 127). *) val crash_save : int -> unit - -val check_for_geoproof_input : unit -> unit diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 73a30b18f..8d99cc3e6 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -142,7 +142,6 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - if !Coq_config.with_geoproof then Coqide.check_for_geoproof_input (); os_specific_init (); try GMain.main (); diff --git a/man/coqtop.1 b/man/coqtop.1 index 62d17aa67..b1fbb3262 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -140,12 +140,6 @@ dump globalizations in file f (to be used by ) .TP -.BI \-with\-geoproof \ (yes|no) -to (de)activate special functions for Geoproof within Coqide (default is -.I yes -) - -.TP .B \-impredicative\-set set sort Set impredicative diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9b58c9a65..cd376214a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -571,7 +571,6 @@ let parse_args arglist = |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) |"-require" -> add_require (next ()) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) - |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> diff --git a/toplevel/usage.ml b/toplevel/usage.ml index d596e36f3..f0215b678 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -74,7 +74,6 @@ let print_usage_channel co command = \n -emacs tells Coq it is executed under Emacs\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ -\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ |