File: coqide_WIN32.ml.in

package info (click to toggle)
coq-doc 8.16.1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: bookworm
  • size: 42,788 kB
  • sloc: ml: 219,673; sh: 4,035; python: 3,372; ansic: 2,529; makefile: 728; lisp: 279; javascript: 87; xml: 24; sed: 2
file content (57 lines) | stat: -rw-r--r-- 2,210 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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 coqide 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 coqide 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 "coqide_" ".log" in
      Coqide.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 () =
  Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
  set_win32_path ();
  Coq.interrupter := interrupter;
  reroute_stdout_stderr ();
  try ignore (Unix.getenv "GTK_CSD") with Not_found -> Unix.putenv "GTK_CSD" "0"

let init () = ()