From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- ide/coq.ml | 5 ----- ide/document.ml | 6 ------ ide/wg_ProofView.ml | 13 ------------- 3 files changed, 24 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index a60f327b4..268a95a33 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines = "Command was: "^cmd^"\n"^ "Answer was: "^(String.concat "\n " lines)) -let check_remaining_opt arg = - if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg) - let rec filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in @@ -200,8 +197,6 @@ module GlibMainLoop = struct let read_all = Ideutils.io_read_all let async_chan_of_file fd = Glib.Io.channel_of_descr fd let async_chan_of_socket s = !gio_channel_of_descr_socket s - let add_timeout ~sec callback = - ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback) end module CoqTop = Spawn.Async(GlibMainLoop) diff --git a/ide/document.ml b/ide/document.ml index 41d5a7564..bb431e791 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -124,12 +124,6 @@ let context d = let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in List.map (flat pair true) top, List.map (flat pair true) bot -let iter d f = - let a, s, b = to_lists d in - List.iter (flat f false) a; - List.iter (flat f true) s; - List.iter (flat f false) b - let stateid_opt_equal = Option.equal Stateid.equal let is_in_focus d id = diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 148add6e9..642a57787 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -114,19 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with (Some Tags.Proof.goal))); ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) -let mode_cesar (proof : #GText.view_skel) = function - | [] -> assert false - | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ -> - proof#buffer#insert " *** Declarative Mode ***\n"; - List.iter - (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n") - hyps; - proof#buffer#insert "______________________________________\n"; - proof#buffer#insert "thesis := \n "; - insert_xml proof#buffer cur_goal; - proof#buffer#insert "\n"; - ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) - let rec flatten = function | [] -> [] | (lg, rg) :: l -> -- cgit v1.2.3