Removing dead code and unused opens.

6 files changed, 3 insertions, 44 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index aa1a75db6..6639b0201 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -44,12 +44,9 @@ module SentenceId : sig
   val mk_sentence :
     start:GText.mark -> stop:GText.mark -> flag list -> sentence
 
-  val set_flags : sentence -> flag list -> unit
   val add_flag : sentence -> flag -> unit
   val has_flag : sentence -> mem_flag -> bool
   val remove_flag : sentence -> mem_flag -> unit
-  val same_sentence : sentence -> sentence -> bool
-  val hidden_edit_id : unit -> int
   val find_all_tooltips : sentence -> int -> string list
   val add_tooltip : sentence -> int -> int -> string -> unit
   val set_index : sentence -> int -> unit
@@ -87,18 +84,15 @@ end = struct
     index = -1;
     changed_sig = new GUtil.signal ();
   }
-  let hidden_edit_id () = decr id; !id
 
   let changed s =
     s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags)
 
-  let set_flags s f = s.flags <- f; changed s
   let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s
   let has_flag s mf =
     List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
   let remove_flag s mf =
     s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s
-  let same_sentence s1 s2 = s1.edit_id = s2.edit_id
   let find_all_tooltips s off =
     CList.map_filter (fun (start,stop,t) ->
       if start <= off && off <= stop then Some t else None)
diff --git a/ide/preferences.ml b/ide/preferences.ml
index addea9074..c4dc55972 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -386,14 +386,6 @@ let processing_color =
 let _ = attach_bg processing_color Tags.Script.to_process
 let _ = attach_bg processing_color Tags.Script.incomplete
 
-let default_tag = {
-  tag_fg_color = None;
-  tag_bg_color = None;
-  tag_bold = false;
-  tag_italic = false;
-  tag_underline = false;
-}
-
 let tags = ref Util.String.Map.empty
 
 let list_tags () = !tags
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 580f1fbcb..8f6cb382a 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -52,33 +52,6 @@ let int_of_modifier = function
   | `RELEASE -> 1 lsl 30
   | `SUPER -> 1 lsl 21
 
-let print_modifier l =
-  List.iter
-    (fun m ->
-      print_string
-	(((function
-	    `SHIFT -> "SHIFT"
-	  | `LOCK -> "LOCK"
-	  | `CONTROL -> "CONTROL"
-	  | `MOD1 -> "MOD1"
-	  | `MOD2 -> "MOD2"
-	  | `MOD3 -> "MOD3"
-	  | `MOD4 -> "MOD4"
-	  | `MOD5 -> "MOD5"
-	  | `BUTTON1 -> "B1"
-	  | `BUTTON2 -> "B2"
-	  | `BUTTON3 -> "B3"
-	  | `BUTTON4 -> "B4"
-	  | `BUTTON5 -> "B5"
-          | `HYPER -> "HYPER"                                                                                                     
-          | `META -> "META"                                                                                                       
-          | `RELEASE -> ""                                                                                                        
-          | `SUPER -> "SUPER")
-	    m)^" ")
-    )
-    l;
-  print_newline ()
-
 let int_of_modifiers l =
   List.fold_left (fun acc -> fun m -> acc + (int_of_modifier m)) 0 l
 
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 6c53fc013..aeae3e1fd 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -86,7 +86,7 @@ let signals = [
   end_s#disconnect;
 ] in
 object (self : 'a)
-  inherit GUtil.ml_signals signals as super
+  inherit GUtil.ml_signals signals
   method start_completion = start_s#connect ~after
   method update_completion = update_s#connect ~after
   method end_completion = end_s#connect ~after
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 4d95fdd0d..47c86045a 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -91,7 +91,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       let () = proof#buffer#insert head_str in
       let () = insert_hyp hyps_hints hyps in
       let () =
-        let tags = Tags.Proof.goal :: if goal_hints <> [] then
+        let _ = if goal_hints <> [] then
           let tag = proof#buffer#create_tag [] in
           let () = hook_tag_cb tag goal_hints sel_cb on_hover in
           [tag]
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 83fbda487..218cedb36 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -287,7 +287,7 @@ let completion = new Wg_Completion.complete_model ct view#buffer in
 let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
 
 object (self)
-  inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
+  inherit GSourceView2.source_view (Gobject.unsafe_cast tv)
 
   val undo_manager = new undo_manager view#buffer