Quelle  rocqide_WIN32.ml.in

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* On win32, we add the directory of rocqide to the PATH at launch-time
   (this used to be done in a .bat script). *)

let set_win32_path () =
  Unix.putenv "PATH"
    (Filename.dirname Sys.executable_name ^ ";" ^
      (try Sys.getenv "PATH" with _ -> ""))

(* On win32, since rocqide is now console-free, we re-route stdout/stderr
   to avoid Sys_error if someone writes to them. We write to a pipe which
   is never read (by default) or to a temp log file (when in debug mode).
*)

let reroute_stdout_stderr () =
  (* We anticipate a bit the argument parsing and look for -debug *)
  let debug = List.mem "-debug" (Array.to_list Sys.argv) in
  Minilib.debug := debug;
  let out_descr =
    if debug then
      let (name,chan) = Filename.open_temp_file "rocqide_" ".log" in
      Rocqide.logfile := Some name;
      Unix.descr_of_out_channel chan
    else
      snd (Unix.pipe ())
  in
  Unix.set_close_on_exec out_descr;
  Unix.dup2 out_descr Unix.stdout;
  Unix.dup2 out_descr Unix.stderr

(* We also provide a specific interrupt function. *)

external win32_interrupt : int -> unit = "win32_interrupt"

let interrupter pid = 
  (* indicate which process to interrupt *)
  let fd = open_out (Shared.get_interrupt_fname pid) in
  close_out fd;
  win32_interrupt pid
      
let () =
  set_win32_path ();
  RocqDriver.interrupter := interrupter;
  reroute_stdout_stderr ();
  try ignore (Unix.getenv "GTK_CSD") with Not_found -> Unix.putenv "GTK_CSD" "0"

let init () = ()