(* 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/
 *)

exception Not_implemented of string
let not_implemented feature = raise (Not_implemented feature)

let _ = Helm_registry.load_from "mathita.conf.xml"
let _ = GMain.Main.init ()
let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")

(*
let interactive_user_uri_choice
  ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok")
  ?(enable_button_for_non_vars=false) ~title ~msg
  uris
=
  let only_constant_choices =
    lazy
      (List.filter
        (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
        uris)
  in
  if selection_mode <> `SINGLE && !auto_disambiguation then
    Lazy.force only_constant_choices
  else begin
    let choices = ref [] in
    let chosen = ref false in
    let use_only_constants = ref false in
    gui#uriChoice#uriChoiceDialog#set_title title;
    gui#uriChoice#uriChoiceLabel#set_text msg;
    FINQUI

    let clist =
     let expected_height = 18 * List.length uris in
      let height = if expected_height > 400 then 400 else expected_height in
       GList.clist ~columns:1 ~packing:scrolled_window#add
        ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
    let _ = List.map (function x -> clist#append [x]) uris in
    let hbox2 =
     GPack.hbox ~border_width:0
      ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
    let explain_label =
     GMisc.label ~text:"None of the above. Try this one:"
      ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
    let manual_input =
     GEdit.entry ~editable:true
      ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
    let hbox =
     GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
    let okb =
     GButton.button ~label:ok
      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
    let _ = okb#misc#set_sensitive false in
    let nonvarsb =
     GButton.button
      ~packing:
       (function w ->
         if enable_button_for_non_vars then
          hbox#pack ~expand:false ~fill:false ~padding:5 w)
      ~label:"Try constants only" () in
    let autob =
     GButton.button
      ~packing:
       (fun w ->
         if enable_button_for_non_vars then
          hbox#pack ~expand:false ~fill:false ~padding:5 w)
      ~label:"Auto" () in
    let checkb =
     GButton.button ~label:"Check"
      ~packing:(hbox#pack ~padding:5) () in
    let _ = checkb#misc#set_sensitive false in
    let cancelb =
     GButton.button ~label:"Abort"
      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
    (* actions *)
    let check_callback () =
     assert (List.length !choices > 0) ;
     check_window !choices
    in
     ignore (window#connect#destroy GMain.Main.quit) ;
     ignore (cancelb#connect#clicked window#destroy) ;
     ignore
      (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
     ignore
      (nonvarsb#connect#clicked
        (function () ->
          use_only_constants := true ;
          chosen := true ;
          window#destroy ()
      )) ;
     ignore (autob#connect#clicked (fun () ->
       auto_disambiguation := true;
       (rendering_window ())#set_auto_disambiguation true;
       use_only_constants := true ;
       chosen := true;
       window#destroy ()));
     ignore (checkb#connect#clicked check_callback) ;
     ignore
      (clist#connect#select_row
        (fun ~row ~column ~event ->
          checkb#misc#set_sensitive true ;
          okb#misc#set_sensitive true ;
          choices := (List.nth uris row)::!choices)) ;
     ignore
      (clist#connect#unselect_row
        (fun ~row ~column ~event ->
          choices :=
           List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
     ignore
      (manual_input#connect#changed
        (fun _ ->
          if manual_input#text = "" then
           begin
            choices := [] ;
            checkb#misc#set_sensitive false ;
            okb#misc#set_sensitive false ;
            clist#misc#set_sensitive true
           end
          else
           begin
            choices := [manual_input#text] ;
            clist#unselect_all () ;
            checkb#misc#set_sensitive true ;
            okb#misc#set_sensitive true ;
            clist#misc#set_sensitive false
           end));
     window#set_position `CENTER ;
     window#show () ;
     GtkThread.main ();
     if !chosen then
      if !use_only_constants then
        Lazy.force only_constant_choices
      else
       if List.length !choices > 0 then !choices else raise NoChoice
     else
      raise NoChoice
  end
 ;;
*)

(*
module DisambiguateCallbacks =
  struct
    let interactive_user_uri_choice =
      assert false  (* TODO *)
(*       interactive_user_uri_choice *)
    let interactive_interpretation_choice choices =
      assert false  (* TODO *)
    let input_or_locate_uri ~title =
      assert false  (* TODO *)
  end
*)

  (** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
let _ = gui#setQuitCallback quit

let _ = GtkThread.main ()