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 let _ = Helm_registry.load_from "mathita.conf.xml"
  30 let _ = GMain.Main.init ()
  31 let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
  32
  33 (*
  34 let interactive_user_uri_choice
  35   ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok")
  36   ?(enable_button_for_non_vars=false) ~title ~msg
  37   uris
  38 =
  39   let only_constant_choices =
  40     lazy
  41       (List.filter
  42         (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
  43         uris)
  44   in
  45   if selection_mode <> `SINGLE && !auto_disambiguation then
  46     Lazy.force only_constant_choices
  47   else begin
  48     let choices = ref [] in
  49     let chosen = ref false in
  50     let use_only_constants = ref false in
  51     gui#uriChoice#uriChoiceDialog#set_title title;
  52     gui#uriChoice#uriChoiceLabel#set_text msg;
  53     FINQUI
  54
  55     let clist =
  56      let expected_height = 18 * List.length uris in
  57       let height = if expected_height > 400 then 400 else expected_height in
  58        GList.clist ~columns:1 ~packing:scrolled_window#add
  59         ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
  60     let _ = List.map (function x -> clist#append [x]) uris in
  61     let hbox2 =
  62      GPack.hbox ~border_width:0
  63       ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
  64     let explain_label =
  65      GMisc.label ~text:"None of the above. Try this one:"
  66       ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
  67     let manual_input =
  68      GEdit.entry ~editable:true
  69       ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
  70     let hbox =
  71      GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
  72     let okb =
  73      GButton.button ~label:ok
  74       ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  75     let _ = okb#misc#set_sensitive false in
  76     let nonvarsb =
  77      GButton.button
  78       ~packing:
  79        (function w ->
  80          if enable_button_for_non_vars then
  81           hbox#pack ~expand:false ~fill:false ~padding:5 w)
  82       ~label:"Try constants only" () in
  83     let autob =
  84      GButton.button
  85       ~packing:
  86        (fun w ->
  87          if enable_button_for_non_vars then
  88           hbox#pack ~expand:false ~fill:false ~padding:5 w)
  89       ~label:"Auto" () in
  90     let checkb =
  91      GButton.button ~label:"Check"
  92       ~packing:(hbox#pack ~padding:5) () in
  93     let _ = checkb#misc#set_sensitive false in
  94     let cancelb =
  95      GButton.button ~label:"Abort"
  96       ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  97     (* actions *)
  98     let check_callback () =
  99      assert (List.length !choices > 0) ;
 100      check_window !choices
 101     in
 102      ignore (window#connect#destroy GMain.Main.quit) ;
 103      ignore (cancelb#connect#clicked window#destroy) ;
 104      ignore
 105       (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 106      ignore
 107       (nonvarsb#connect#clicked
 108         (function () ->
 109           use_only_constants := true ;
 110           chosen := true ;
 111           window#destroy ()
 112       )) ;
 113      ignore (autob#connect#clicked (fun () ->
 114        auto_disambiguation := true;
 115        (rendering_window ())#set_auto_disambiguation true;
 116        use_only_constants := true ;
 117        chosen := true;
 118        window#destroy ()));
 119      ignore (checkb#connect#clicked check_callback) ;
 120      ignore
 121       (clist#connect#select_row
 122         (fun ~row ~column ~event ->
 123           checkb#misc#set_sensitive true ;
 124           okb#misc#set_sensitive true ;
 125           choices := (List.nth uris row)::!choices)) ;
 126      ignore
 127       (clist#connect#unselect_row
 128         (fun ~row ~column ~event ->
 129           choices :=
 130            List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
 131      ignore
 132       (manual_input#connect#changed
 133         (fun _ ->
 134           if manual_input#text = "" then
 135            begin
 136             choices := [] ;
 137             checkb#misc#set_sensitive false ;
 138             okb#misc#set_sensitive false ;
 139             clist#misc#set_sensitive true
 140            end
 141           else
 142            begin
 143             choices := [manual_input#text] ;
 144             clist#unselect_all () ;
 145             checkb#misc#set_sensitive true ;
 146             okb#misc#set_sensitive true ;
 147             clist#misc#set_sensitive false
 148            end));
 149      window#set_position `CENTER ;
 150      window#show () ;
 151      GtkThread.main ();
 152      if !chosen then
 153       if !use_only_constants then
 154         Lazy.force only_constant_choices
 155       else
 156        if List.length !choices > 0 then !choices else raise NoChoice
 157      else
 158       raise NoChoice
 159   end
 160  ;;
 161 *)
 162
 163 (*
 164 module DisambiguateCallbacks =
 165   struct
 166     let interactive_user_uri_choice =
 167       assert false  (* TODO *)
 168 (*       interactive_user_uri_choice *)
 169     let interactive_interpretation_choice choices =
 170       assert false  (* TODO *)
 171     let input_or_locate_uri ~title =
 172       assert false  (* TODO *)
 173   end
 174 *)
 175
 176   (** quit program, possibly asking for confirmation *)
 177 let quit () = GMain.Main.quit ()
 178 let _ = gui#setQuitCallback quit
 179
 180 let _ = GtkThread.main ()
 181