helm/mathita/mathita.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 exception Not_implemented of string
  27 let not_implemented feature = raise (Not_implemented feature)
  28
  29   (** exceptions whose content should be presented to the user *)
  30 exception Failure of string
  31 let error s = raise (Failure s)
  32
  33 let _ = Helm_registry.load_from "mathita.conf.xml"
  34 let _ = GMain.Main.init ()
  35 let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
  36
  37 let interactive_user_uri_choice
  38   ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
  39   uris
  40 =
  41   let only_constant_choices =
  42     lazy
  43       (List.filter
  44         (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
  45         uris)
  46   in
  47   if (selection_mode <> `SINGLE) &&
  48     (Helm_registry.get_bool "mathita.auto_disambiguation")
  49   then
  50     Lazy.force only_constant_choices
  51   else begin
  52     let win = gui#uriChoice in
  53     let choices = ref [] in
  54     let chosen = ref false in
  55     let use_only_constants = ref false in
  56     win#uriChoiceDialog#set_title title;
  57     win#uriChoiceLabel#set_text msg;
  58     gui#uriChoices#list_store#clear ();
  59     List.iter gui#uriChoices#easy_append uris;
  60     win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
  61     let bye = ref (fun () -> ()) in
  62     let id1 =
  63       win#uriChoiceConstantsButton#connect#clicked (fun _ ->
  64         use_only_constants := true;
  65         !bye ())
  66     in
  67     let id2 =
  68       win#uriChoiceAutoButton#connect#clicked (fun _ ->
  69        use_only_constants := true ;
  70        Helm_registry.set_bool "mathita.auto_disambiguation" true;
  71        !bye ())
  72     in
  73     let id3 =
  74       win#uriChoiceSelectedButton#connect#clicked (fun _ ->
  75         choices := gui#uriChoices#easy_selection ();
  76         !bye ())
  77     in
  78     bye := (fun () ->
  79       win#uriChoiceDialog#misc#hide ();
  80       win#uriChoiceConstantsButton#misc#disconnect id1;
  81       win#uriChoiceAutoButton#misc#disconnect id2;
  82       win#uriChoiceSelectedButton#misc#disconnect id3;
  83       prerr_endline "quit";
  84       GMain.Main.quit ());
  85     win#uriChoiceDialog#show ();
  86     GtkThread.main ();
  87     if !use_only_constants then
  88       Lazy.force only_constant_choices
  89     else
  90       match !choices with
  91       | [] -> error "No choice"
  92       | choices -> choices
  93   end
  94
  95 (*
  96 module DisambiguateCallbacks =
  97   struct
  98     let interactive_user_uri_choice =
  99       assert false  (* TODO *)
 100 (*       interactive_user_uri_choice *)
 101     let interactive_interpretation_choice choices =
 102       assert false  (* TODO *)
 103     let input_or_locate_uri ~title =
 104       assert false  (* TODO *)
 105   end
 106 *)
 107
 108 let debugDialog () =
 109   let dialog =
 110     new MathitaGeneratedGui.debug
 111       ~file:(Helm_registry.get "mathita.glade_file") ()
 112   in
 113   let retval = ref None in
 114   let return v =
 115     retval := Some v;
 116     dialog#debug#destroy ();
 117     GMain.Main.quit ()
 118   in
 119   ignore (dialog#debug#event#connect#delete (fun _ -> true));
 120   ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1));
 121   ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2));
 122   dialog#debug#show ();
 123   GtkThread.main ();
 124   (match !retval with None -> assert false | Some v -> v)
 125
 126 let _ =
 127   gui#main#debugMenuItem2#connect#activate (fun _ ->
 128     prerr_endline (string_of_int (debugDialog ())))
 129
 130   (** quit program, possibly asking for confirmation *)
 131 let quit () = GMain.Main.quit ()
 132 let _ = gui#setQuitCallback quit
 133 let _ =
 134   gui#main#debugMenuItem0#connect#activate (fun _ ->
 135     let uris =
 136       interactive_user_uri_choice
 137         ~selection_mode:`MULTIPLE
 138         ~nonvars_button:false
 139         ~title:"titolo"
 140         ~msg:"messaggio"
 141         ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
 142         "cic:/cinque.var"]
 143     in
 144     List.iter prerr_endline uris; print_newline ())
 145 let _ =
 146   gui#main#debugMenuItem1#connect#activate (fun _ ->
 147     Helm_registry.set_bool "mathita.auto_disambiguation"
 148       (not (Helm_registry.get_bool "mathita.auto_disambiguation")))
 149
 150 let _ =
 151 (*   gui#uriChoices#easy_append "pippo"; *)
 152 (*   gui#uriChoices#list_store#clear (); *)
 153   GtkThread.main ()
 154