aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-11 16:07:04 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-11 16:07:04 +0200
commitcea76410557f9954c8e15861217bcc4559de9e25 (patch)
tree853557ca2abcce31cc5dbcc77da58df7675f6e48 /ide
parent354ee7d67efda8624cb46e942f2a41211cadd030 (diff)
Remove GeoProof support.
Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml19
-rw-r--r--ide/coqide.mli2
-rw-r--r--ide/coqide_main.ml41
3 files changed, 0 insertions, 22 deletions
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 ();