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