helm/matita/matitaGui.ml

   1 (* Copyright (C) 2004-2005, 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 open Printf
  27
  28 open MatitaGeneratedGui
  29 open MatitaGtkMisc
  30 open MatitaMisc
  31
  32 let gui_instance = ref None ;;
  33
  34 class console ~(buffer: GText.buffer) () =
  35   object (self)
  36     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
  37     val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
  38     val message_tag = buffer#create_tag []
  39     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
  40     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
  41     method error s   = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
  42     method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
  43     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
  44     method clear () =
  45       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
  46     method log_callback (tag: MatitaLog.log_tag) s =
  47       match tag with
  48       | `Debug -> self#debug (s ^ "\n")
  49       | `Error -> self#error (s ^ "\n")
  50       | `Message -> self#message (s ^ "\n")
  51       | `Warning -> self#warning (s ^ "\n")
  52   end
  53
  54 class gui () =
  55     (* creation order _is_ relevant for windows placement *)
  56   let main = new mainWin () in
  57   let about = new aboutWin () in
  58   let fileSel = new fileSelectionWin () in
  59   let keyBindingBoxes = (* event boxes which should receive global key events *)
  60     [ main#mainWinEventBox ]
  61   in
  62   let console = new console ~buffer:main#logTextView#buffer () in
  63   object (self)
  64     val mutable chosen_file = None
  65     val mutable _ok_not_exists = false
  66     val mutable script_fname = None
  67
  68     initializer
  69         (* glade's check widgets *)
  70       List.iter (fun w -> w#check_widgets ())
  71         (let c w = (w :> <check_widgets: unit -> unit>) in
  72          [ c about; c fileSel; c main ]);
  73         (* key bindings *)
  74       List.iter (* global key bindings *)
  75         (fun (key, callback) -> self#addKeyBinding key callback)
  76 (*
  77         [ GdkKeysyms._F3,
  78             toggle_win ~check:main#showProofMenuItem proof#proofWin;
  79           GdkKeysyms._F4,
  80             toggle_win ~check:main#showCheckMenuItem check#checkWin;
  81 *)
  82         [ ];
  83         (* about win *)
  84       ignore (about#aboutWin#event#connect#delete (fun _ -> true));
  85       ignore (main#aboutMenuItem#connect#activate (fun _ ->
  86         about#aboutWin#show ()));
  87       connect_button about#aboutDismissButton (fun _ ->
  88         about#aboutWin#misc#hide ());
  89       about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
  90         ~templ:BuildTimeConf.version about#aboutLabel#label);
  91         (* file selection win *)
  92       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
  93       ignore (fileSel#fileSelectionWin#connect#response (fun event ->
  94         let return r =
  95           chosen_file <- r;
  96           fileSel#fileSelectionWin#misc#hide ();
  97           GMain.Main.quit ()
  98         in
  99         match event with
 100         | `OK ->
 101             let fname = fileSel#fileSelectionWin#filename in
 102             if Sys.file_exists fname then
 103               (if is_regular fname then return (Some fname))
 104             else
 105               (if _ok_not_exists then return (Some fname))
 106         | `CANCEL -> return None
 107         | `HELP -> ()
 108         | `DELETE_EVENT -> return None));
 109         (* menus *)
 110       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
 111       main#helpMenu#set_right_justified true;
 112         (* console *)
 113       let adj = main#logScrolledWin#vadjustment in
 114       ignore (adj#connect#changed
 115                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
 116       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
 117         (* toolbar *)
 118       let module A = TacticAst in
 119       let hole = CicAst.UserInput in
 120       let loc = CicAst.dummy_floc in
 121       let tac ast _ =
 122         if (MatitaScript.instance ())#onGoingProof () then
 123           (MatitaScript.instance ())#advance
 124             ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
 125       in
 126       let tac_w_term ast _ =
 127         if (MatitaScript.instance ())#onGoingProof () then
 128           let (buf: GText.buffer) = self#main#scriptTextView#buffer in
 129           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
 130             ("\n" ^ TacticAstPp.pp_tactic ast)
 131       in
 132       let tbar = self#main in
 133       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
 134       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
 135       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
 136       connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None)));
 137       connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
 138       connect_button tbar#splitButton (tac (A.Split loc));
 139       connect_button tbar#leftButton (tac (A.Left loc));
 140       connect_button tbar#rightButton (tac (A.Right loc));
 141       connect_button tbar#existsButton (tac (A.Exists loc));
 142       connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
 143       connect_button tbar#symmetryButton (tac (A.Symmetry loc));
 144       connect_button tbar#transitivityButton
 145         (tac_w_term (A.Transitivity (loc, hole)));
 146       connect_button tbar#assumptionButton (tac (A.Assumption loc));
 147       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
 148       connect_button tbar#autoButton (tac (A.Auto (loc,None)));
 149         (* quit *)
 150       self#setQuitCallback (fun () -> exit 0);
 151         (* log *)
 152       MatitaLog.set_log_callback self#console#log_callback;
 153       GtkSignal.user_handler :=
 154         (fun exn ->
 155            MatitaLog.error
 156              (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
 157         (* script *)
 158       let s () = MatitaScript.instance () in
 159       let disableSave () =
 160         script_fname <- None;
 161         self#main#saveMenuItem#misc#set_sensitive false
 162       in
 163       let loadScript () =
 164         let script = s () in
 165         match self#chooseFile () with
 166         | Some f ->
 167               script#reset ();
 168               script#loadFrom f;
 169               console#message ("'"^f^"' loaded.");
 170               self#_enableSaveTo f
 171         | None -> ()
 172       in
 173       let saveAsScript () =
 174         let script = s () in
 175         match self#chooseFile ~ok_not_exists:true () with
 176         | Some f ->
 177               script#saveTo f;
 178               console#message ("'"^f^"' saved.");
 179               self#_enableSaveTo f
 180         | None -> ()
 181       in
 182       let saveScript () =
 183         match script_fname with
 184         | None -> saveAsScript ()
 185         | Some f ->
 186               (s ())#saveTo f;
 187               console#message ("'"^f^"' saved.");
 188       in
 189       let newScript () = (s ())#reset (); disableSave () in
 190       let cursor () =
 191         let buf = self#main#scriptTextView#buffer in
 192         buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
 193       in
 194       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
 195       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
 196       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
 197       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
 198       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
 199       let connect_key sym f =
 200         connect_key self#main#mainWinEventBox#event
 201           ~modifiers:[`CONTROL] ~stop:true sym f;
 202         connect_key self#main#scriptTextView#event
 203           ~modifiers:[`CONTROL] ~stop:true sym f
 204       in
 205       connect_button self#main#scriptAdvanceButton advance;
 206       connect_button self#main#scriptRetractButton retract;
 207       connect_button self#main#scriptTopButton top;
 208       connect_button self#main#scriptBottomButton bottom;
 209       connect_key GdkKeysyms._Down advance;
 210       connect_key GdkKeysyms._Up retract;
 211       connect_key GdkKeysyms._Home top;
 212       connect_key GdkKeysyms._End bottom;
 213       connect_button self#main#scriptJumpButton jump;
 214       connect_menu_item self#main#openMenuItem   loadScript;
 215       connect_menu_item self#main#saveMenuItem   saveScript;
 216       connect_menu_item self#main#saveAsMenuItem saveAsScript;
 217       connect_menu_item self#main#newMenuItem    newScript;
 218       connect_key GdkKeysyms._period
 219         (fun () ->
 220            let buf = self#main#scriptTextView#buffer in
 221            buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n";
 222            advance ());
 223       connect_key GdkKeysyms._Return
 224         (fun () ->
 225            let buf = self#main#scriptTextView#buffer in
 226            buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
 227            advance ());
 228         (* debug menu *)
 229       self#main#debugMenu#misc#hide ();
 230         (* status bar *)
 231       self#main#hintLowImage#set_file "icons/matita-bulb-low.png";
 232       self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png";
 233       self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
 234         (* focus *)
 235       self#main#scriptTextView#misc#grab_focus ()
 236
 237     method loadScript file =
 238       let script = MatitaScript.instance () in
 239       script#reset ();
 240       script#loadFrom file;
 241       console#message ("'"^file^"' loaded.");
 242       self#_enableSaveTo file
 243
 244     method private _enableSaveTo file =
 245       script_fname <- Some file;
 246       self#main#saveMenuItem#misc#set_sensitive true
 247
 248
 249     method console = console
 250
 251     method about = about
 252     method fileSel = fileSel
 253     method main = main
 254
 255     method newBrowserWin () =
 256       let win = new browserWin () in
 257       win#whelpImage2#set_file "icons/whelp.png";
 258       win#whelpBarToggleButton#set_active false;
 259       win#whelpBarBox#misc#hide ();
 260       win#mathOrListNotebook#set_show_tabs false;
 261       connect_toggle_button win#whelpBarToggleButton
 262         (fun () ->
 263           if win#whelpBarToggleButton#active then
 264             win#whelpBarBox#misc#show ()
 265           else
 266             win#whelpBarBox#misc#hide ());
 267       let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
 268       let combo,(combo_store,combo_column) =
 269         GEdit.combo_box_text ~strings:queries ()
 270       in
 271       combo#set_active 0;
 272       win#comboVbox#add (combo :> GObj.widget);
 273       let start_query () =
 274         let query = String.lowercase (List.nth queries combo#active) in
 275         let input = win#queryInputText#text in
 276         let statement = "whelp " ^ query ^ " " ^ input ^ "." in
 277         (MatitaScript.instance ())#advance ~statement ()
 278       in
 279       ignore(win#queryInputText#connect#activate ~callback:start_query);
 280       ignore(combo#connect#changed ~callback:start_query);
 281       win#check_widgets ();
 282       win
 283
 284     method newUriDialog () =
 285       let dialog = new uriChoiceDialog () in
 286       dialog#check_widgets ();
 287       dialog
 288
 289     method newInterpDialog () =
 290       let dialog = new interpChoiceDialog () in
 291       dialog#check_widgets ();
 292       dialog
 293
 294     method newConfirmationDialog () =
 295       let dialog = new confirmationDialog () in
 296       dialog#check_widgets ();
 297       dialog
 298
 299     method newEmptyDialog () =
 300       let dialog = new emptyDialog () in
 301       dialog#check_widgets ();
 302       dialog
 303
 304     method private addKeyBinding key callback =
 305       List.iter (fun evbox -> add_key_binding key callback evbox)
 306         keyBindingBoxes
 307
 308     method setQuitCallback callback =
 309       ignore (main#toplevel#connect#destroy callback);
 310       ignore (main#quitMenuItem#connect#activate callback);
 311       self#addKeyBinding GdkKeysyms._q callback
 312
 313     method chooseFile ?(ok_not_exists = false) () =
 314       _ok_not_exists <- ok_not_exists;
 315       fileSel#fileSelectionWin#show ();
 316       GtkThread.main ();
 317       chosen_file
 318
 319     method askText ?(title = "") ?(msg = "") () =
 320       let dialog = new textDialog () in
 321       dialog#textDialog#set_title title;
 322       dialog#textDialogLabel#set_label msg;
 323       let text = ref None in
 324       let return v =
 325         text := v;
 326         dialog#textDialog#destroy ();
 327         GMain.Main.quit ()
 328       in
 329       ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
 330       connect_button dialog#textDialogCancelButton (fun _ -> return None);
 331       connect_button dialog#textDialogOkButton (fun _ ->
 332         let text = dialog#textDialogTextView#buffer#get_text () in
 333         return (Some text));
 334       dialog#textDialog#show ();
 335       GtkThread.main ();
 336       !text
 337
 338   end
 339
 340 let gui () =
 341   let g = new gui () in
 342   gui_instance := Some g;
 343   g
 344
 345 let instance = singleton gui
 346
 347 let non p x = not (p x)
 348
 349 let is_var_uri s =
 350   try
 351     String.sub s (String.length s - 4) 4 = ".var"
 352   with Invalid_argument _ -> false
 353
 354 let interactive_uri_choice
 355   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
 356   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
 357   ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
 358   ~id uris
 359 =
 360   let gui = instance () in
 361   let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
 362   if (selection_mode <> `SINGLE) &&
 363     (Helm_registry.get_bool "matita.auto_disambiguation")
 364   then
 365     Lazy.force nonvars_uris
 366   else begin
 367     let dialog = gui#newUriDialog () in
 368     if hide_uri_entry then
 369       dialog#uriEntryHBox#misc#hide ();
 370     if hide_try then
 371       begin
 372       dialog#uriChoiceSelectedButton#misc#hide ();
 373       dialog#uriChoiceConstantsButton#misc#hide ();
 374       end;
 375     dialog#okLabel#set_label ok_label;
 376     dialog#uriChoiceTreeView#selection#set_mode
 377       (selection_mode :> Gtk.Tags.selection_mode);
 378     let model = new stringListModel dialog#uriChoiceTreeView in
 379     let choices = ref None in
 380     let nonvars = ref false in
 381     (match copy_cb with
 382     | None -> ()
 383     | Some cb ->
 384         dialog#copyButton#misc#show ();
 385         connect_button dialog#copyButton
 386         (fun _ ->
 387           match model#easy_selection () with
 388           | [u] -> (cb u)
 389           | _ -> ()));
 390     dialog#uriChoiceDialog#set_title title;
 391     dialog#uriChoiceLabel#set_text msg;
 392     List.iter model#easy_append uris;
 393     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
 394     let return v =
 395       choices := v;
 396       dialog#uriChoiceDialog#destroy ();
 397       GMain.Main.quit ()
 398     in
 399     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
 400     connect_button dialog#uriChoiceConstantsButton (fun _ ->
 401       return (Some (Lazy.force nonvars_uris)));
 402     connect_button dialog#uriChoiceAutoButton (fun _ ->
 403       Helm_registry.set_bool "matita.auto_disambiguation" true;
 404       return (Some (Lazy.force nonvars_uris)));
 405     connect_button dialog#uriChoiceSelectedButton (fun _ ->
 406       match model#easy_selection () with
 407       | [] -> ()
 408       | uris -> return (Some uris));
 409     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
 410     dialog#uriChoiceDialog#show ();
 411     GtkThread.main ();
 412     (match !choices with
 413     | None -> raise MatitaTypes.Cancel
 414     | Some uris -> uris)
 415   end
 416
 417 class interpModel =
 418   let cols = new GTree.column_list in
 419   let id_col = cols#add Gobject.Data.string in
 420   let dsc_col = cols#add Gobject.Data.string in
 421   let interp_no_col = cols#add Gobject.Data.int in
 422   let tree_store = GTree.tree_store cols in
 423   let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
 424   let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
 425   let id_view_col = GTree.view_column ~renderer:id_renderer () in
 426   let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
 427   fun tree_view choices ->
 428     object
 429       initializer
 430         tree_view#set_model (Some (tree_store :> GTree.model));
 431         ignore (tree_view#append_column id_view_col);
 432         ignore (tree_view#append_column dsc_view_col);
 433         let name_of_interp =
 434           (* try to find a reasonable name for an interpretation *)
 435           let idx = ref 0 in
 436           fun interp ->
 437             try
 438               List.assoc "0" interp
 439             with Not_found ->
 440               incr idx; string_of_int !idx
 441         in
 442         tree_store#clear ();
 443         let idx = ref ~-1 in
 444         List.iter
 445           (fun interp ->
 446             incr idx;
 447             let interp_row = tree_store#append () in
 448             tree_store#set ~row:interp_row ~column:id_col
 449               (name_of_interp interp);
 450             tree_store#set ~row:interp_row ~column:interp_no_col !idx;
 451             List.iter
 452               (fun (id, dsc) ->
 453                 let row = tree_store#append ~parent:interp_row () in
 454                 tree_store#set ~row ~column:id_col id;
 455                 tree_store#set ~row ~column:dsc_col dsc;
 456                 tree_store#set ~row ~column:interp_no_col !idx)
 457               interp)
 458           choices
 459
 460       method get_interp_no tree_path =
 461         let iter = tree_store#get_iter tree_path in
 462         tree_store#get ~row:iter ~column:interp_no_col
 463     end
 464
 465 let interactive_interp_choice () choices =
 466   let gui = instance () in
 467   assert (choices <> []);
 468   let dialog = gui#newInterpDialog () in
 469   let model = new interpModel dialog#interpChoiceTreeView choices in
 470   let interp_len = List.length (List.hd choices) in
 471   dialog#interpChoiceDialog#set_title "Interpretation choice";
 472   dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
 473   let interp_no = ref None in
 474   let return _ =
 475     dialog#interpChoiceDialog#destroy ();
 476     GMain.Main.quit ()
 477   in
 478   let fail _ = interp_no := None; return () in
 479   ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
 480   connect_button dialog#interpChoiceOkButton (fun _ ->
 481     match !interp_no with None -> () | Some _ -> return ());
 482   connect_button dialog#interpChoiceCancelButton fail;
 483   ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
 484     interp_no := Some (model#get_interp_no path);
 485     return ()));
 486   let selection = dialog#interpChoiceTreeView#selection in
 487   ignore (selection#connect#changed (fun _ ->
 488     match selection#get_selected_rows with
 489     | [path] ->
 490         MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
 491         interp_no := Some (model#get_interp_no path)
 492     | _ -> assert false));
 493   dialog#interpChoiceDialog#show ();
 494   GtkThread.main ();
 495   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
 496