From 00a8604d89f47c903fc5283eebdda67c87468699 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 31 Oct 2018 15:29:57 +0100 Subject: Select OS specific coqide code with cp. --- ide/coqide_QUARTZ.ml.in | 37 +++++++++++ ide/coqide_WIN32.ml.in | 50 +++++++++++++++ ide/coqide_X11.ml.in | 11 ++++ ide/coqide_main.ml | 72 +++++++++++++++++++++ ide/coqide_main.ml4 | 154 --------------------------------------------- ide/coqide_os_specific.mli | 11 ++++ ide/dune | 6 +- 7 files changed, 184 insertions(+), 157 deletions(-) create mode 100644 ide/coqide_QUARTZ.ml.in create mode 100644 ide/coqide_WIN32.ml.in create mode 100644 ide/coqide_X11.ml.in create mode 100644 ide/coqide_main.ml delete mode 100644 ide/coqide_main.ml4 create mode 100644 ide/coqide_os_specific.mli (limited to 'ide') diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in new file mode 100644 index 0000000000..a08bac5772 --- /dev/null +++ b/ide/coqide_QUARTZ.ml.in @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Coqide.do_load x; true) + in + let _ = osx#connect#ns_application_block_termination + ~callback:Coqide.forbid_quit + in + let _ = osx#connect#ns_application_will_terminate + ~callback:Coqide.close_and_quit + in () + +let init () = + let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication + (GtkMenu.MenuShell.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) + in + let () = GtkosxApplication.Application.insert_app_menu_item + osx#as_osxapplication + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 + in + let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication + (Some (GtkMenu.MenuItem.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) + in + osx#ready () diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in new file mode 100644 index 0000000000..8c4649fc39 --- /dev/null +++ b/ide/coqide_WIN32.ml.in @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* "")) + +(* 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 specific kill and interrupt functions. *) + +external win32_kill : int -> unit = "win32_kill" +external win32_interrupt : int -> unit = "win32_interrupt" +let () = + Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; + set_win32_path (); + Coq.interrupter := win32_interrupt; + reroute_stdout_stderr () + +let init () = () diff --git a/ide/coqide_X11.ml.in b/ide/coqide_X11.ml.in new file mode 100644 index 0000000000..6a5784eac3 --- /dev/null +++ b/ide/coqide_X11.ml.in @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 0 in + if level_is `ERROR then `FATAL + else if level_is `CRITICAL then `ERROR + else if level_is `DEBUG then `DEBUG + else if level_is `WARNING then `WARNING + else if level_is `MESSAGE then `NOTICE + else `INFO + in + let handler ~level msg = + let header = "Coqide internal error: " in + match log_level level with + |`FATAL -> + let () = GToolbox.message_box ~title:"Error" (header ^ msg) in + Coqide.crash_save 1 + |`ERROR -> + if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) + else Printf.eprintf "%s\n" (header ^ msg) + |`DEBUG -> Minilib.log msg + |level when Sys.os_type = "Win32" -> Minilib.log ~level msg + |_ -> Printf.eprintf "%s\n" msg + in + let catch domain = + ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler) + in + List.iter catch ["GLib";"Gtk";"Gdk";"Pango"] + +let () = catch_gtk_messages () + +let load_prefs () = + try Preferences.load_pref () + with e -> Ideutils.flash_info + ("Could not load preferences ("^Printexc.to_string e^").") + +let () = + load_prefs (); + let argl = List.tl (Array.to_list Sys.argv) in + let argl = Coqide.read_coqide_args argl in + let files = Coq.filter_coq_opts argl in + let args = List.filter (fun x -> not (List.mem x files)) argl in + Coq.check_connection args; + Coqide.sup_args := args; + Coqide.main files; + Coqide_os_specific.init (); + try + GMain.main (); + failwith "Gtk loop ended" + with e -> + Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e); + Coqide.crash_save 127 diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 deleted file mode 100644 index 3a92e1bc91..0000000000 --- a/ide/coqide_main.ml4 +++ /dev/null @@ -1,154 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 0 in - if level_is `ERROR then `FATAL - else if level_is `CRITICAL then `ERROR - else if level_is `DEBUG then `DEBUG - else if level_is `WARNING then `WARNING - else if level_is `MESSAGE then `NOTICE - else `INFO - in - let handler ~level msg = - let header = "Coqide internal error: " in - match log_level level with - |`FATAL -> - let () = GToolbox.message_box ~title:"Error" (header ^ msg) in - Coqide.crash_save 1 - |`ERROR -> - if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) - else Printf.eprintf "%s\n" (header ^ msg) - |`DEBUG -> Minilib.log msg - |level when Sys.os_type = "Win32" -> Minilib.log ~level msg - |_ -> Printf.eprintf "%s\n" msg - in - let catch domain = - ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler) - in - List.iter catch ["GLib";"Gtk";"Gdk";"Pango"] - -let () = catch_gtk_messages () - - - -(** System-dependent settings *) - -let os_specific_init () = () - -(** Win32 *) - -IFDEF WIN32 THEN - -(* 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 specific kill and interrupt functions. *) - -external win32_kill : int -> unit = "win32_kill" -external win32_interrupt : int -> unit = "win32_interrupt" -let () = - Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; - set_win32_path (); - Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () -END - -(** MacOSX *) - -IFDEF QUARTZ THEN -let osx = GosxApplication.osxapplication () - -let () = - let _ = osx#connect#ns_application_open_file - ~callback:(fun x -> Coqide.do_load x; true) - in - let _ = osx#connect#ns_application_block_termination - ~callback:Coqide.forbid_quit - in - let _ = osx#connect#ns_application_will_terminate - ~callback:Coqide.close_and_quit - in () - -let os_specific_init () = - let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication - (GtkMenu.MenuShell.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) - in - let () = GtkosxApplication.Application.insert_app_menu_item - osx#as_osxapplication - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 - in - let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication - (Some (GtkMenu.MenuItem.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) - in - osx#ready () -END - -let load_prefs () = - try Preferences.load_pref () - with e -> Ideutils.flash_info - ("Could not load preferences ("^Printexc.to_string e^").") - -let () = - load_prefs (); - let argl = List.tl (Array.to_list Sys.argv) in - let argl = Coqide.read_coqide_args argl in - let files = Coq.filter_coq_opts argl in - let args = List.filter (fun x -> not (List.mem x files)) argl in - Coq.check_connection args; - Coqide.sup_args := args; - Coqide.main files; - os_specific_init (); - try - GMain.main (); - failwith "Gtk loop ended" - with e -> - Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e); - Coqide.crash_save 127 diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli new file mode 100644 index 0000000000..ebd09099f0 --- /dev/null +++ b/ide/coqide_os_specific.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit diff --git a/ide/dune b/ide/dune index 70a1709f37..5714b1370e 100644 --- a/ide/dune +++ b/ide/dune @@ -33,9 +33,9 @@ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2)) (rule - (targets coqide_main.ml) - (deps (:ml4-file coqide_main.ml4)) - (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets}))) + (targets coqide_os_specific.ml) + (deps (:in-file coqide_X11.ml.in)) ; TODO support others + (action (run cp %{in-file} %{targets}))) (executable (name coqide_main) -- cgit v1.2.3