diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index c433d92ac..5aa615549 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -16,7 +16,6 @@ val doc_url : unit -> string val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int -val debug : bool ref val disconnect_revert_timer : unit -> unit val disconnect_auto_save_timer : unit -> unit val do_convert : string -> string @@ -25,13 +24,8 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a -val is_char_start : char -> bool - val my_stat : string -> Unix.stats option -(** debug printing *) -val prerr_endline : string -> unit - val print_id : 'a -> unit val revert_timer : GMain.Timeout.id option ref @@ -50,8 +44,6 @@ val stock_to_widget : ?size:Gtk.Tags.icon_size -> GtkStock.id -> GObj.widget open Format val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit -val run_command : (string -> unit) -> string -> Unix.process_status*string - val custom_coqtop : string option ref (* @return command to call coqtop - custom_coqtop if set @@ -69,11 +61,6 @@ val set_location : (string -> unit) ref val pbar : GRange.progress_bar -(* - returns an absolute filename equivalent to given filename -*) -val absolute_filename : string -> string - (* In win32, when a command-line is to be executed via cmd.exe (i.e. Sys.command, Unix.open_process, ...), it cannot contain several quoted "..." zones otherwise some quotes are lost. Solution: we re-quote |