(* Copyright (C) 2004, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

  (** quit program, possibly asking for confirmation *)
let quit () =
  GMain.Main.quit ()

  (** given a window and a check menu item it links the two so that the former
   * is only hidden on delete and the latter toggle show/hide of the former *)
let toggle_visibility (win: GWindow.window) (check: GMenu.check_menu_item) =
  ignore (check#connect#toggled (fun _ ->
    if check#active then win#show () else win#misc#hide ()));
  ignore (win#event#connect#delete (fun _ ->
    win#misc#hide ();
    check#set_active false;
    true))

let toggle_win ?check win () =
  if win#is_active then win#misc#hide () else win#show ();
  match check with
  | None -> ()
  | Some check -> check#set_active (not check#active)

let add_key_bindings bindings (evbox: GBin.event_box) =
  List.iter
    (fun (key, callback) ->
      ignore (evbox#event#connect#key_press (function
        | key' when GdkEvent.Key.keyval key' = key ->
            callback ();
            false
        | _ -> false)))
    bindings

class gui file =
  object (self)
    val about = new MathitaGui.aboutWin ~file ()
    val dialog = new MathitaGui.genericDialog ~file ()
    val filesel = new MathitaGui.fileSelectionWin ~file ()
    val main = new MathitaGui.mainWin ~file ()
    val proof = new MathitaGui.proofWin ~file ()
    val toolbar = new MathitaGui.toolBarWin ~file ()
    initializer
      let c w = (w :> <check_widgets: unit -> unit>) in
      List.iter (fun w -> w#check_widgets ())
        [ c about; c dialog; c filesel; c main; c proof; c toolbar ];
      ignore (main#toplevel#connect#destroy quit);
      ignore (main#exitMenuItem#connect#activate quit);
      toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
      toggle_visibility proof#proofWin main#showProofMenuItem;
      let key_bindings = [
        GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin;
        GdkKeysyms._q, quit;
      ] in
      add_key_bindings key_bindings toolbar#toolBarEventBox;
      add_key_bindings key_bindings proof#proofWinEventBox;
      ()
  end

let _ =
  let glade_file = "mathita.glade" in
  let _ = GMain.Main.init () in
  let gui = new gui glade_file in
  GtkThread.main ()