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 (* $Id$ *)
  27
  28 open Printf
  29
  30 open MatitaGeneratedGui
  31 open MatitaGtkMisc
  32 open MatitaMisc
  33
  34 exception Found of int
  35
  36 let gui_instance = ref None
  37
  38 class type browserWin =
  39   (* this class exists only because GEdit.combo_box_entry is not supported by
  40    * lablgladecc :-(((( *)
  41 object
  42   inherit MatitaGeneratedGui.browserWin
  43   method browserUri: GEdit.combo_box_entry
  44 end
  45
  46 class console ~(buffer: GText.buffer) () =
  47   object (self)
  48     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
  49     val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
  50     val message_tag = buffer#create_tag []
  51     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
  52     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
  53     method error s   = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
  54     method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
  55     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
  56     method clear () =
  57       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
  58     method log_callback (tag: HLog.log_tag) s =
  59       match tag with
  60       | `Debug -> self#debug (s ^ "\n")
  61       | `Error -> self#error (s ^ "\n")
  62       | `Message -> self#message (s ^ "\n")
  63       | `Warning -> self#warning (s ^ "\n")
  64   end
  65
  66 let clean_current_baseuri grafite_status =
  67     try
  68       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
  69       LibraryClean.clean_baseuris [baseuri]
  70     with GrafiteTypes.Option_error _ -> ()
  71
  72 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
  73   let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
  74   let moo_fname = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true in
  75   let save () =
  76     let metadata_fname =
  77      LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in
  78     let lexicon_fname =
  79      LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
  80     in
  81      GrafiteMarshal.save_moo moo_fname
  82       grafite_status.GrafiteTypes.moo_content_rev;
  83      LibraryNoDb.save_metadata metadata_fname
  84       lexicon_status.LexiconEngine.metadata;
  85      LexiconMarshal.save_lexicon lexicon_fname
  86       lexicon_status.LexiconEngine.lexicon_content_rev
  87   in
  88   if (MatitaScript.current ())#eos &&
  89      grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
  90   then
  91     begin
  92       let rc =
  93         MatitaGtkMisc.ask_confirmation
  94         ~title:"A .moo can be generated"
  95         ~message:(Printf.sprintf
  96           "%s can be generated for %s.\n<i>Should I generate it?</i>"
  97           (Filename.basename moo_fname) (Filename.basename fname))
  98         ~parent ()
  99       in
 100       let b =
 101         match rc with
 102         | `YES -> true
 103         | `NO -> false
 104         | `CANCEL -> raise MatitaTypes.Cancel
 105       in
 106       if b then
 107           save ()
 108       else
 109         clean_current_baseuri grafite_status
 110     end
 111   else
 112     clean_current_baseuri grafite_status
 113
 114 let ask_unsaved parent =
 115   MatitaGtkMisc.ask_confirmation
 116     ~parent ~title:"Unsaved work!"
 117     ~message:("Your work is <b>unsaved</b>!\n\n"^
 118          "<i>Do you want to save the script before continuing?</i>")
 119     ()
 120
 121 (** Selection handling
 122  * Two clipboards are used: "clipboard" and "primary".
 123  * "primary" is used by X, when you hit the middle button mouse is content is
 124  *    pasted between applications. In Matita this selection always contain the
 125  *    textual version of the selected term.
 126  * "clipboard" is used inside Matita only and support ATM two different targets:
 127  *    "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may
 128  *    be added
 129  *)
 130
 131 class gui () =
 132     (* creation order _is_ relevant for windows placement *)
 133   let main = new mainWin () in
 134   let fileSel = new fileSelectionWin () in
 135   let findRepl = new findReplWin () in
 136   let develList = new develListWin () in
 137   let newDevel = new newDevelWin () in
 138   let keyBindingBoxes = (* event boxes which should receive global key events *)
 139     [ main#mainWinEventBox ]
 140   in
 141   let console = new console ~buffer:main#logTextView#buffer () in
 142   let (source_view: GSourceView.source_view) =
 143     GSourceView.source_view
 144       ~auto_indent:true
 145       ~insert_spaces_instead_of_tabs:true ~tabs_width:2
 146       ~margin:80 ~show_margin:true
 147       ~smart_home_end:true
 148       ~packing:main#scriptScrolledWin#add
 149       ()
 150   in
 151   let default_font_size =
 152     Helm_registry.get_opt_default Helm_registry.int
 153       ~default:BuildTimeConf.default_font_size "matita.font_size"
 154   in
 155   let source_buffer = source_view#source_buffer in
 156   object (self)
 157     val mutable chosen_file = None
 158     val mutable _ok_not_exists = false
 159     val mutable _only_directory = false
 160     val mutable script_fname = None
 161     val mutable font_size = default_font_size
 162     val mutable next_devel_must_contain = None
 163     val mutable next_ligatures = []
 164     val clipboard = GData.clipboard Gdk.Atom.clipboard
 165     val primary = GData.clipboard Gdk.Atom.primary
 166
 167     initializer
 168         (* glade's check widgets *)
 169       List.iter (fun w -> w#check_widgets ())
 170         (let c w = (w :> <check_widgets: unit -> unit>) in
 171         [ c fileSel; c main; c findRepl]);
 172         (* key bindings *)
 173       List.iter (* global key bindings *)
 174         (fun (key, callback) -> self#addKeyBinding key callback)
 175 (*
 176         [ GdkKeysyms._F3,
 177             toggle_win ~check:main#showProofMenuItem proof#proofWin;
 178           GdkKeysyms._F4,
 179             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 180 *)
 181         [ ];
 182         (* about win *)
 183       let parse_txt_file file =
 184        let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
 185        let l_rev = ref [] in
 186        try
 187         while true do
 188          l_rev := input_line ch :: !l_rev;
 189         done;
 190         assert false
 191        with
 192         End_of_file ->
 193          close_in ch;
 194          List.rev !l_rev in
 195       let about_dialog =
 196        GWindow.about_dialog
 197         ~authors:(parse_txt_file "AUTHORS")
 198         (*~comments:"comments"*)
 199         ~copyright:"Copyright (C) 2005, the HELM team"
 200         ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
 201         ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png"))
 202         ~name:"Matita"
 203         ~version:BuildTimeConf.version
 204         ~website:"http://helm.cs.unibo.it"
 205         ()
 206       in
 207       connect_menu_item main#contentsMenuItem (fun () ->
 208         let cmd =
 209           sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
 210         in
 211         ignore (Sys.command cmd));
 212       connect_menu_item main#aboutMenuItem about_dialog#present;
 213         (* findRepl win *)
 214       let show_find_Repl () =
 215         findRepl#toplevel#misc#show ();
 216         findRepl#toplevel#misc#grab_focus ()
 217       in
 218       let hide_find_Repl () = findRepl#toplevel#misc#hide () in
 219       let find_forward _ =
 220           let highlight start end_ =
 221             source_buffer#move_mark `INSERT ~where:start;
 222             source_buffer#move_mark `SEL_BOUND ~where:end_;
 223             source_view#scroll_mark_onscreen `INSERT
 224           in
 225           let text = findRepl#findEntry#text in
 226           let iter = source_buffer#get_iter `SEL_BOUND in
 227           match iter#forward_search text with
 228           | None ->
 229               (match source_buffer#start_iter#forward_search text with
 230               | None -> ()
 231               | Some (start,end_) -> highlight start end_)
 232           | Some (start,end_) -> highlight start end_
 233       in
 234       let replace _ =
 235         let text = findRepl#replaceEntry#text in
 236         let ins = source_buffer#get_iter `INSERT in
 237         let sel = source_buffer#get_iter `SEL_BOUND in
 238         if ins#compare sel < 0 then
 239           begin
 240             ignore(source_buffer#delete_selection ());
 241             source_buffer#insert text
 242           end
 243       in
 244       connect_button findRepl#findButton find_forward;
 245       connect_button findRepl#findReplButton replace;
 246       connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
 247       ignore(findRepl#toplevel#event#connect#delete
 248         ~callback:(fun _ -> hide_find_Repl ();true));
 249       let safe_undo =
 250        fun () ->
 251         (* phase 1: we save the actual status of the marks and we undo *)
 252         let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
 253         let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
 254         let locked_iter_offset = locked_iter#offset in
 255         let mark2 =
 256          `MARK
 257            (source_view#buffer#create_mark ~name:"lock_point"
 258              ~left_gravity:true locked_iter) in
 259         source_view#source_buffer#undo ();
 260         (* phase 2: we save the cursor position and we redo, restoring
 261            the previous status of all the marks *)
 262         let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
 263         let mark =
 264          `MARK
 265            (source_view#buffer#create_mark ~name:"undo_point"
 266              ~left_gravity:true cursor_iter)
 267         in
 268          source_view#source_buffer#redo ();
 269          let mark_iter = source_view#buffer#get_iter_at_mark mark in
 270          let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
 271          let mark2_iter = mark2_iter#set_offset locked_iter_offset in
 272           source_view#buffer#move_mark locked_mark ~where:mark2_iter;
 273           source_view#buffer#delete_mark mark;
 274           source_view#buffer#delete_mark mark2;
 275           (* phase 3: if after the undo the cursor was in the locked area,
 276              then we move it there again and we perform a goto *)
 277           if mark_iter#offset < locked_iter_offset then
 278            begin
 279             source_view#buffer#move_mark `INSERT ~where:mark_iter;
 280             (MatitaScript.current ())#goto `Cursor ();
 281            end;
 282           (* phase 4: we perform again the undo. This time we are sure that
 283              the text to undo is not locked *)
 284           source_view#source_buffer#undo ();
 285           source_view#misc#grab_focus () in
 286       let safe_redo =
 287        fun () ->
 288         (* phase 1: we save the actual status of the marks, we redo and
 289            we undo *)
 290         let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
 291         let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
 292         let locked_iter_offset = locked_iter#offset in
 293         let mark2 =
 294          `MARK
 295            (source_view#buffer#create_mark ~name:"lock_point"
 296              ~left_gravity:true locked_iter) in
 297         source_view#source_buffer#redo ();
 298         source_view#source_buffer#undo ();
 299         (* phase 2: we save the cursor position and we restore
 300            the previous status of all the marks *)
 301         let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
 302         let mark =
 303          `MARK
 304            (source_view#buffer#create_mark ~name:"undo_point"
 305              ~left_gravity:true cursor_iter)
 306         in
 307          let mark_iter = source_view#buffer#get_iter_at_mark mark in
 308          let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
 309          let mark2_iter = mark2_iter#set_offset locked_iter_offset in
 310           source_view#buffer#move_mark locked_mark ~where:mark2_iter;
 311           source_view#buffer#delete_mark mark;
 312           source_view#buffer#delete_mark mark2;
 313           (* phase 3: if after the undo the cursor is in the locked area,
 314              then we move it there again and we perform a goto *)
 315           if mark_iter#offset < locked_iter_offset then
 316            begin
 317             source_view#buffer#move_mark `INSERT ~where:mark_iter;
 318             (MatitaScript.current ())#goto `Cursor ();
 319            end;
 320           (* phase 4: we perform again the redo. This time we are sure that
 321              the text to redo is not locked *)
 322           source_view#source_buffer#redo ();
 323           source_view#misc#grab_focus ()
 324       in
 325       connect_menu_item main#undoMenuItem safe_undo;
 326       ignore(source_view#source_buffer#connect#can_undo
 327         ~callback:main#undoMenuItem#misc#set_sensitive);
 328       connect_menu_item main#redoMenuItem safe_redo;
 329       ignore(source_view#source_buffer#connect#can_redo
 330         ~callback:main#redoMenuItem#misc#set_sensitive);
 331       ignore(source_view#connect#after#populate_popup
 332        ~callback:(fun pre_menu ->
 333          let menu = new GMenu.menu pre_menu in
 334          let menuItems = menu#children in
 335          let undoMenuItem, redoMenuItem =
 336           match menuItems with
 337              [undo;redo;sep1;cut;copy;paste;delete;sep2;
 338               selectall;sep3;inputmethod;insertunicodecharacter] ->
 339                 List.iter menu#remove [ copy; cut; delete; paste ];
 340                 undo,redo
 341            | _ -> assert false in
 342          let add_menu_item =
 343            let i = ref 2 in (* last occupied position *)
 344            fun ?label ?stock () ->
 345              incr i;
 346              GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
 347               ()
 348          in
 349          let copy = add_menu_item ~stock:`COPY () in
 350          let cut = add_menu_item ~stock:`CUT () in
 351          let delete = add_menu_item ~stock:`DELETE () in
 352          let paste = add_menu_item ~stock:`PASTE () in
 353          let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
 354          copy#misc#set_sensitive self#canCopy;
 355          cut#misc#set_sensitive self#canCut;
 356          delete#misc#set_sensitive self#canDelete;
 357          paste#misc#set_sensitive self#canPaste;
 358          paste_pattern#misc#set_sensitive self#canPastePattern;
 359          connect_menu_item copy self#copy;
 360          connect_menu_item cut self#cut;
 361          connect_menu_item delete self#delete;
 362          connect_menu_item paste self#paste;
 363          connect_menu_item paste_pattern self#pastePattern;
 364          let new_undoMenuItem =
 365           GMenu.image_menu_item
 366            ~image:(GMisc.image ~stock:`UNDO ())
 367            ~use_mnemonic:true
 368            ~label:"_Undo"
 369            ~packing:(menu#insert ~pos:0) () in
 370          new_undoMenuItem#misc#set_sensitive
 371           (undoMenuItem#misc#get_flag `SENSITIVE);
 372          menu#remove (undoMenuItem :> GMenu.menu_item);
 373          connect_menu_item new_undoMenuItem safe_undo;
 374          let new_redoMenuItem =
 375           GMenu.image_menu_item
 376            ~image:(GMisc.image ~stock:`REDO ())
 377            ~use_mnemonic:true
 378            ~label:"_Redo"
 379            ~packing:(menu#insert ~pos:1) () in
 380          new_redoMenuItem#misc#set_sensitive
 381           (redoMenuItem#misc#get_flag `SENSITIVE);
 382           menu#remove (redoMenuItem :> GMenu.menu_item);
 383           connect_menu_item new_redoMenuItem safe_redo));
 384
 385       connect_menu_item main#editMenu (fun () ->
 386         main#copyMenuItem#misc#set_sensitive self#canCopy;
 387         main#cutMenuItem#misc#set_sensitive self#canCut;
 388         main#deleteMenuItem#misc#set_sensitive self#canDelete;
 389         main#pasteMenuItem#misc#set_sensitive self#canPaste;
 390         main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern);
 391       connect_menu_item main#copyMenuItem self#copy;
 392       connect_menu_item main#cutMenuItem self#cut;
 393       connect_menu_item main#deleteMenuItem self#delete;
 394       connect_menu_item main#pasteMenuItem self#paste;
 395       connect_menu_item main#pastePatternMenuItem self#pastePattern;
 396       connect_menu_item main#selectAllMenuItem (fun () ->
 397         source_buffer#move_mark `INSERT source_buffer#start_iter;
 398         source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
 399       connect_menu_item main#findReplMenuItem show_find_Repl;
 400       connect_menu_item main#externalEditorMenuItem self#externalEditor;
 401       connect_menu_item main#ligatureButton self#nextLigature;
 402       ignore (findRepl#findEntry#connect#activate find_forward);
 403         (* interface lockers *)
 404       let lock_world _ =
 405         main#buttonsToolbar#misc#set_sensitive false;
 406         develList#buttonsHbox#misc#set_sensitive false;
 407         source_view#set_editable false
 408       in
 409       let unlock_world _ =
 410         main#buttonsToolbar#misc#set_sensitive true;
 411         develList#buttonsHbox#misc#set_sensitive true;
 412         source_view#set_editable true
 413       in
 414       let locker f =
 415         fun () ->
 416           lock_world ();
 417           try f ();unlock_world () with exc -> unlock_world (); raise exc in
 418       let keep_focus f =
 419         fun () ->
 420          try
 421           f (); source_view#misc#grab_focus ()
 422          with
 423           exc -> source_view#misc#grab_focus (); raise exc in
 424         (* developments win *)
 425       let model =
 426         new MatitaGtkMisc.multiStringListModel
 427           ~cols:2 develList#developmentsTreeview
 428       in
 429       let refresh_devels_win () =
 430         model#list_store#clear ();
 431         List.iter
 432           (fun (name, root) -> model#easy_mappend [name;root])
 433           (MatitamakeLib.list_known_developments ())
 434       in
 435       let get_devel_selected () =
 436         match model#easy_mselection () with
 437         | [[name;_]] -> MatitamakeLib.development_for_name name
 438         | _ -> None
 439       in
 440       let refresh () =
 441         while Glib.Main.pending () do
 442           ignore(Glib.Main.iteration false);
 443         done
 444       in
 445       connect_button develList#newButton
 446         (fun () ->
 447           next_devel_must_contain <- None;
 448           newDevel#toplevel#misc#show());
 449       connect_button develList#deleteButton
 450         (locker (fun () ->
 451           (match get_devel_selected () with
 452           | None -> ()
 453           | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
 454           refresh_devels_win ()));
 455       connect_button develList#buildButton
 456         (locker (fun () ->
 457           match get_devel_selected () with
 458           | None -> ()
 459           | Some d ->
 460               let build = locker
 461                 (fun () -> MatitamakeLib.build_development_in_bg refresh d)
 462               in
 463               ignore(build ())));
 464       connect_button develList#cleanButton
 465         (locker (fun () ->
 466           match get_devel_selected () with
 467           | None -> ()
 468           | Some d ->
 469               let clean = locker
 470                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
 471               in
 472               ignore(clean ())));
 473       connect_button develList#publishButton
 474         (locker (fun () ->
 475           match get_devel_selected () with
 476           | None -> ()
 477           | Some d ->
 478               let clean = locker
 479                 (fun () -> MatitamakeLib.publish_development_in_bg refresh d)
 480               in
 481               ignore(clean ())));
 482       connect_button develList#closeButton
 483         (fun () -> develList#toplevel#misc#hide());
 484       ignore(develList#toplevel#event#connect#delete
 485         (fun _ -> develList#toplevel#misc#hide();true));
 486       connect_menu_item main#developmentsMenuItem
 487         (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
 488
 489         (* add development win *)
 490       let check_if_root_contains root =
 491         match next_devel_must_contain with
 492         | None -> true
 493         | Some path ->
 494             let is_prefix_of d1 d2 =
 495               let len1 = String.length d1 in
 496               let len2 = String.length d2 in
 497               if len2 < len1 then
 498                 false
 499               else
 500                 let pref = String.sub d2 0 len1 in
 501                 pref = d1
 502             in
 503             is_prefix_of root path
 504       in
 505       connect_button newDevel#addButton
 506        (fun () ->
 507           let name = newDevel#nameEntry#text in
 508           let root = newDevel#rootEntry#text in
 509           if check_if_root_contains root then
 510             begin
 511               ignore (MatitamakeLib.initialize_development name root);
 512               refresh_devels_win ();
 513               newDevel#nameEntry#set_text "";
 514               newDevel#rootEntry#set_text "";
 515               newDevel#toplevel#misc#hide()
 516             end
 517           else
 518             HLog.error ("The selected root does not contain " ^
 519               match next_devel_must_contain with
 520               | Some x -> x
 521               | _ -> assert false));
 522       connect_button newDevel#chooseRootButton
 523        (fun () ->
 524          let path = self#chooseDir () in
 525          match path with
 526          | Some path -> newDevel#rootEntry#set_text path
 527          | None -> ());
 528       connect_button newDevel#cancelButton
 529        (fun () -> newDevel#toplevel#misc#hide ());
 530       ignore(newDevel#toplevel#event#connect#delete
 531         (fun _ -> newDevel#toplevel#misc#hide();true));
 532
 533         (* file selection win *)
 534       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
 535       ignore (fileSel#fileSelectionWin#connect#response (fun event ->
 536         let return r =
 537           chosen_file <- r;
 538           fileSel#fileSelectionWin#misc#hide ();
 539           GMain.Main.quit ()
 540         in
 541         match event with
 542         | `OK ->
 543             let fname = fileSel#fileSelectionWin#filename in
 544             if Sys.file_exists fname then
 545               begin
 546                 if HExtlib.is_regular fname && not (_only_directory) then
 547                   return (Some fname)
 548                 else if _only_directory && HExtlib.is_dir fname then
 549                   return (Some fname)
 550               end
 551             else
 552               begin
 553                 if _ok_not_exists then
 554                   return (Some fname)
 555               end
 556         | `CANCEL -> return None
 557         | `HELP -> ()
 558         | `DELETE_EVENT -> return None));
 559         (* menus *)
 560       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
 561         (* console *)
 562       let adj = main#logScrolledWin#vadjustment in
 563         ignore (adj#connect#changed
 564                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
 565       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
 566         (* toolbar *)
 567       let module A = GrafiteAst in
 568       let hole = CicNotationPt.UserInput in
 569       let loc = HExtlib.dummy_floc in
 570       let tac ast _ =
 571         if (MatitaScript.current ())#onGoingProof () then
 572           (MatitaScript.current ())#advance
 573             ~statement:("\n"
 574               ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
 575                 ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
 576             ()
 577       in
 578       let tac_w_term ast _ =
 579         if (MatitaScript.current ())#onGoingProof () then
 580           let buf = source_buffer in
 581           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
 582             ("\n"
 583             ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
 584               ~lazy_term_pp:CicNotationPp.pp_term ast)
 585       in
 586       let tbar = main in
 587       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
 588       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
 589       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
 590       connect_button tbar#elimButton (tac_w_term
 591         (A.Elim (loc, hole, None, None, [])));
 592       connect_button tbar#elimTypeButton (tac_w_term
 593         (A.ElimType (loc, hole, None, None, [])));
 594       connect_button tbar#splitButton (tac (A.Split loc));
 595       connect_button tbar#leftButton (tac (A.Left loc));
 596       connect_button tbar#rightButton (tac (A.Right loc));
 597       connect_button tbar#existsButton (tac (A.Exists loc));
 598       connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
 599       connect_button tbar#symmetryButton (tac (A.Symmetry loc));
 600       connect_button tbar#transitivityButton
 601         (tac_w_term (A.Transitivity (loc, hole)));
 602       connect_button tbar#assumptionButton (tac (A.Assumption loc));
 603       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
 604       connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
 605       MatitaGtkMisc.toggle_widget_visibility
 606        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
 607        ~check:main#tacticsBarMenuItem;
 608       let module Hr = Helm_registry in
 609       if
 610         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
 611       then
 612         main#tacticsBarMenuItem#set_active false;
 613       MatitaGtkMisc.toggle_callback
 614         ~callback:(function
 615           | true -> main#toplevel#fullscreen ()
 616           | false -> main#toplevel#unfullscreen ())
 617         ~check:main#fullscreenMenuItem;
 618       main#fullscreenMenuItem#set_active false;
 619         (* log *)
 620       HLog.set_log_callback self#console#log_callback;
 621       GtkSignal.user_handler :=
 622         (function
 623         | MatitaScript.ActionCancelled s -> HLog.error s
 624         | exn ->
 625           if not (Helm_registry.get_bool "matita.debug") then
 626            let floc, msg = MatitaExcPp.to_string exn in
 627             begin
 628              match floc with
 629                 None -> ()
 630               | Some floc ->
 631                  let (x, y) = HExtlib.loc_of_floc floc in
 632                  let script = MatitaScript.current () in
 633                  let locked_mark = script#locked_mark in
 634                  let error_tag = script#error_tag in
 635                  let baseoffset =
 636                   (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
 637                  let x' = baseoffset + x in
 638                  let y' = baseoffset + y in
 639                  let x_iter = source_buffer#get_iter (`OFFSET x') in
 640                  let y_iter = source_buffer#get_iter (`OFFSET y') in
 641                  source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
 642                  let id = ref None in
 643                  id := Some (source_buffer#connect#changed ~callback:(fun () ->
 644                    source_buffer#remove_tag error_tag
 645                      ~start:source_buffer#start_iter
 646                      ~stop:source_buffer#end_iter;
 647                    match !id with
 648                    | None -> assert false (* a race condition occurred *)
 649                    | Some id ->
 650                        (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
 651                  source_buffer#place_cursor
 652                   (source_buffer#get_iter (`OFFSET x'));
 653             end;
 654             HLog.error msg
 655           else raise exn);
 656         (* script *)
 657       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
 658       let _ =
 659         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
 660         | None ->
 661             HLog.warn (sprintf "can't load language file %s"
 662               BuildTimeConf.lang_file)
 663         | Some matita_lang ->
 664             source_buffer#set_language matita_lang;
 665             source_buffer#set_highlight true
 666       in
 667       let s () = MatitaScript.current () in
 668       let disableSave () =
 669         script_fname <- None;
 670         main#saveMenuItem#misc#set_sensitive false
 671       in
 672       let saveAsScript () =
 673         let script = s () in
 674         match self#chooseFile ~ok_not_exists:true () with
 675         | Some f ->
 676               script#assignFileName f;
 677               script#saveToFile ();
 678               console#message ("'"^f^"' saved.\n");
 679               self#_enableSaveTo f
 680         | None -> ()
 681       in
 682       let saveScript () =
 683         match script_fname with
 684         | None -> saveAsScript ()
 685         | Some f ->
 686               (s ())#assignFileName f;
 687               (s ())#saveToFile ();
 688               console#message ("'"^f^"' saved.\n");
 689       in
 690       let abandon_script () =
 691         let lexicon_status = (s ())#lexicon_status in
 692         let grafite_status = (s ())#grafite_status in
 693         if source_view#buffer#modified then
 694           (match ask_unsaved main#toplevel with
 695           | `YES -> saveScript ()
 696           | `NO -> ()
 697           | `CANCEL -> raise MatitaTypes.Cancel);
 698         (match script_fname with
 699         | None -> ()
 700         | Some fname ->
 701            ask_and_save_moo_if_needed main#toplevel fname
 702             lexicon_status grafite_status);
 703       in
 704       let loadScript () =
 705         let script = s () in
 706         try
 707           match self#chooseFile () with
 708           | Some f ->
 709               abandon_script ();
 710               script#reset ();
 711               script#assignFileName f;
 712               source_view#source_buffer#begin_not_undoable_action ();
 713               script#loadFromFile f;
 714               source_view#source_buffer#end_not_undoable_action ();
 715               console#message ("'"^f^"' loaded.\n");
 716               self#_enableSaveTo f
 717           | None -> ()
 718         with MatitaTypes.Cancel -> ()
 719       in
 720       let newScript () =
 721         abandon_script ();
 722         source_view#source_buffer#begin_not_undoable_action ();
 723         (s ())#reset ();
 724         (s ())#template ();
 725         source_view#source_buffer#end_not_undoable_action ();
 726         disableSave ();
 727         script_fname <- None
 728       in
 729       let cursor () =
 730         source_buffer#place_cursor
 731           (source_buffer#get_iter_at_mark (`NAME "locked")) in
 732       let advance _ = (MatitaScript.current ())#advance (); cursor () in
 733       let retract _ = (MatitaScript.current ())#retract (); cursor () in
 734       let top _ = (MatitaScript.current ())#goto `Top (); cursor () in
 735       let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in
 736       let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () in
 737       let advance = locker (keep_focus advance) in
 738       let retract = locker (keep_focus retract) in
 739       let top = locker (keep_focus top) in
 740       let bottom = locker (keep_focus bottom) in
 741       let jump = locker (keep_focus jump) in
 742         (* quit *)
 743       self#setQuitCallback (fun () ->
 744         let lexicon_status = (MatitaScript.current ())#lexicon_status in
 745         let grafite_status = (MatitaScript.current ())#grafite_status in
 746         if source_view#buffer#modified then
 747           begin
 748             let rc = ask_unsaved main#toplevel in
 749             try
 750               match rc with
 751               | `YES -> saveScript ();
 752                         if not source_view#buffer#modified then
 753                           begin
 754                             (match script_fname with
 755                             | None -> ()
 756                             | Some fname ->
 757                                ask_and_save_moo_if_needed main#toplevel
 758                                 fname lexicon_status grafite_status);
 759                           GMain.Main.quit ()
 760                           end
 761               | `NO -> GMain.Main.quit ()
 762               | `CANCEL -> raise MatitaTypes.Cancel
 763             with MatitaTypes.Cancel -> ()
 764           end
 765         else
 766           begin
 767             (match script_fname with
 768             | None -> clean_current_baseuri grafite_status; GMain.Main.quit ()
 769             | Some fname ->
 770                 try
 771                   ask_and_save_moo_if_needed main#toplevel fname lexicon_status
 772                    grafite_status;
 773                   GMain.Main.quit ()
 774                 with MatitaTypes.Cancel -> ())
 775           end);
 776       connect_button main#scriptAdvanceButton advance;
 777       connect_button main#scriptRetractButton retract;
 778       connect_button main#scriptTopButton top;
 779       connect_button main#scriptBottomButton bottom;
 780       connect_button main#scriptJumpButton jump;
 781       connect_menu_item main#scriptAdvanceMenuItem advance;
 782       connect_menu_item main#scriptRetractMenuItem retract;
 783       connect_menu_item main#scriptTopMenuItem top;
 784       connect_menu_item main#scriptBottomMenuItem bottom;
 785       connect_menu_item main#scriptJumpMenuItem jump;
 786       connect_menu_item main#openMenuItem   loadScript;
 787       connect_menu_item main#saveMenuItem   saveScript;
 788       connect_menu_item main#saveAsMenuItem saveAsScript;
 789       connect_menu_item main#newMenuItem    newScript;
 790          (* script monospace font stuff *)
 791       self#updateFontSize ();
 792         (* debug menu *)
 793       main#debugMenu#misc#hide ();
 794         (* status bar *)
 795       main#hintLowImage#set_file (image_path "matita-bulb-low.png");
 796       main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
 797       main#hintHighImage#set_file (image_path "matita-bulb-high.png");
 798         (* focus *)
 799       self#sourceView#misc#grab_focus ();
 800         (* main win dimension *)
 801       let width = Gdk.Screen.width () in
 802       let height = Gdk.Screen.height () in
 803       let main_w = width * 90 / 100 in
 804       let main_h = height * 80 / 100 in
 805       let script_w = main_w * 6 / 10 in
 806       main#toplevel#resize ~width:main_w ~height:main_h;
 807       main#hpaneScriptSequent#set_position script_w;
 808         (* source_view *)
 809       ignore(source_view#connect#after#paste_clipboard
 810         ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock));
 811       (* clean_locked is set to true only "during" a PRIMARY paste
 812          operation (i.e. by clicking with the second mouse button) *)
 813       let clean_locked = ref false in
 814       ignore(source_view#event#connect#button_press
 815         ~callback:
 816           (fun button ->
 817             if GdkEvent.Button.button button = 2 then
 818              clean_locked := true;
 819             false
 820           ));
 821       ignore(source_view#event#connect#button_release
 822         ~callback:(fun button -> clean_locked := false; false));
 823       ignore(source_view#buffer#connect#after#apply_tag
 824        ~callback:(
 825          fun tag ~start:_ ~stop:_ ->
 826           if !clean_locked &&
 827              tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid
 828           then
 829            begin
 830             clean_locked := false;
 831             (MatitaScript.current ())#clean_dirty_lock;
 832             clean_locked := true
 833            end));
 834       (* math view handling *)
 835       connect_menu_item main#newCicBrowserMenuItem (fun () ->
 836         ignore (MatitaMathView.cicBrowser ()));
 837       connect_menu_item main#increaseFontSizeMenuItem (fun () ->
 838         self#increaseFontSize ();
 839         MatitaMathView.increase_font_size ();
 840         MatitaMathView.update_font_sizes ());
 841       connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
 842         self#decreaseFontSize ();
 843         MatitaMathView.decrease_font_size ();
 844         MatitaMathView.update_font_sizes ());
 845       connect_menu_item main#normalFontSizeMenuItem (fun () ->
 846         self#resetFontSize ();
 847         MatitaMathView.reset_font_size ();
 848         MatitaMathView.update_font_sizes ());
 849       MatitaMathView.reset_font_size ();
 850
 851       (** selections / clipboards handling *)
 852
 853     method markupSelected = MatitaMathView.has_selection ()
 854     method private textSelected =
 855       (source_buffer#get_iter_at_mark `INSERT)#compare
 856         (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
 857     method private somethingSelected = self#markupSelected || self#textSelected
 858     method private markupStored = MatitaMathView.has_clipboard ()
 859     method private textStored = clipboard#text <> None
 860     method private somethingStored = self#markupStored || self#textStored
 861
 862     method canCopy = self#somethingSelected
 863     method canCut = self#textSelected
 864     method canDelete = self#textSelected
 865     method canPaste = self#somethingStored
 866     method canPastePattern = self#markupStored
 867
 868     method copy () =
 869       if self#textSelected
 870       then begin
 871         MatitaMathView.empty_clipboard ();
 872         source_view#buffer#copy_clipboard clipboard;
 873       end else
 874         MatitaMathView.copy_selection ()
 875     method cut () =
 876       source_view#buffer#cut_clipboard clipboard;
 877       MatitaMathView.empty_clipboard ()
 878     method delete () = ignore (source_view#buffer#delete_selection ())
 879     method paste () =
 880       if MatitaMathView.has_clipboard ()
 881       then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term)
 882       else source_view#buffer#paste_clipboard clipboard;
 883       (MatitaScript.current ())#clean_dirty_lock
 884     method pastePattern () =
 885       source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)
 886
 887     method private nextLigature () =
 888       let iter = source_buffer#get_iter_at_mark `INSERT in
 889       let write_ligature len s =
 890         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
 891         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
 892       in
 893       let get_ligature word =
 894         let len = String.length word in
 895         let aux_tex () =
 896           try
 897             for i = len - 1 downto 0 do
 898               if HExtlib.is_alpha word.[i] then ()
 899               else
 900                 (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1))
 901             done;
 902             None
 903           with Found i ->
 904             if i = ~-1 then None else Some (String.sub word i (len - i))
 905         in
 906         let aux_ligature () =
 907           try
 908             for i = len - 1 downto 0 do
 909               if CicNotationLexer.is_ligature_char word.[i] then ()
 910               else raise (Found (i+1))
 911             done;
 912             raise (Found 0)
 913           with
 914           | Found i ->
 915               (try
 916                 Some (String.sub word i (len - i))
 917               with Invalid_argument _ -> None)
 918         in
 919         match aux_tex () with
 920         | Some macro -> macro
 921         | None -> (match aux_ligature () with Some l -> l | None -> word)
 922       in
 923       (match next_ligatures with
 924       | [] -> (* find ligatures and fill next_ligatures, then try again *)
 925           let last_word =
 926             iter#get_slice
 927               ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace)
 928           in
 929           let ligature = get_ligature last_word in
 930           (match CicNotationLexer.lookup_ligatures ligature with
 931           | [] -> ()
 932           | hd :: tl ->
 933               write_ligature (String.length ligature) hd;
 934               next_ligatures <- tl @ [ hd ])
 935       | hd :: tl ->
 936           write_ligature 1 hd;
 937           next_ligatures <- tl @ [ hd ])
 938
 939     method private externalEditor () =
 940       let cmd = Helm_registry.get "matita.external_editor" in
 941 (* ZACK uncomment to enable interactive ask of external editor command *)
 942 (*      let cmd =
 943          let msg =
 944           "External editor command:
 945 %f  will be substitute for the script name,
 946 %p  for the cursor position in bytes,
 947 %l  for the execution point in bytes."
 948         in
 949         ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false
 950           ~default:(Helm_registry.get "matita.external_editor") ()
 951       in *)
 952       let fname = (MatitaScript.current ())#filename in
 953       let slice mark =
 954         source_buffer#start_iter#get_slice
 955           ~stop:(source_buffer#get_iter_at_mark mark)
 956       in
 957       let script = MatitaScript.current () in
 958       let locked = `MARK script#locked_mark in
 959       let string_pos mark = string_of_int (String.length (slice mark)) in
 960       let cursor_pos = string_pos `INSERT in
 961       let locked_pos = string_pos locked in
 962       let cmd =
 963         Pcre.replace ~pat:"%f" ~templ:fname
 964           (Pcre.replace ~pat:"%p" ~templ:cursor_pos
 965             (Pcre.replace ~pat:"%l" ~templ:locked_pos
 966               cmd))
 967       in
 968       let locked_before = slice locked in
 969       let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in
 970       ignore (Unix.system cmd);
 971       source_buffer#set_text (HExtlib.input_file fname);
 972       let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in
 973       source_buffer#move_mark locked locked_iter;
 974       source_buffer#apply_tag script#locked_tag
 975         ~start:source_buffer#start_iter ~stop:locked_iter;
 976       let locked_after = slice locked in
 977       let line = ref 0 in
 978       let col = ref 0 in
 979       try
 980         for i = 0 to String.length locked_before - 1 do
 981           if locked_before.[i] <> locked_after.[i] then begin
 982             source_buffer#place_cursor
 983               ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col)));
 984             script#goto `Cursor ();
 985             raise Exit
 986           end else if locked_before.[i] = '\n' then begin
 987             incr line;
 988             col := 0
 989           end
 990         done
 991       with
 992       | Exit -> ()
 993       | Invalid_argument _ -> script#goto `Bottom ()
 994
 995     method loadScript file =
 996       let script = MatitaScript.current () in
 997       script#reset ();
 998       script#assignFileName file;
 999       let content =
1000        if Sys.file_exists file then file
1001        else BuildTimeConf.script_template
1002       in
1003        source_view#source_buffer#begin_not_undoable_action ();
1004        script#loadFromFile content;
1005        source_view#source_buffer#end_not_undoable_action ();
1006        console#message ("'"^file^"' loaded.");
1007        self#_enableSaveTo file
1008
1009     method setStar name b =
1010       let l = main#scriptLabel in
1011       if b then
1012         l#set_text (name ^  " *")
1013       else
1014         l#set_text (name)
1015
1016     method private _enableSaveTo file =
1017       script_fname <- Some file;
1018       self#main#saveMenuItem#misc#set_sensitive true
1019
1020     method console = console
1021     method sourceView: GSourceView.source_view =
1022       (source_view: GSourceView.source_view)
1023     method fileSel = fileSel
1024     method findRepl = findRepl
1025     method main = main
1026     method develList = develList
1027     method newDevel = newDevel
1028
1029     method newBrowserWin () =
1030       object (self)
1031         inherit browserWin ()
1032         val combo = GEdit.combo_box_entry ()
1033         initializer
1034           self#check_widgets ();
1035           let combo_widget = combo#coerce in
1036           uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
1037           combo#entry#misc#grab_focus ()
1038         method browserUri = combo
1039       end
1040
1041     method newUriDialog () =
1042       let dialog = new uriChoiceDialog () in
1043       dialog#check_widgets ();
1044       dialog
1045
1046     method newRecordDialog () =
1047       let dialog = new recordChoiceDialog () in
1048       dialog#check_widgets ();
1049       dialog
1050
1051     method newConfirmationDialog () =
1052       let dialog = new confirmationDialog () in
1053       dialog#check_widgets ();
1054       dialog
1055
1056     method newEmptyDialog () =
1057       let dialog = new emptyDialog () in
1058       dialog#check_widgets ();
1059       dialog
1060
1061     method private addKeyBinding key callback =
1062       List.iter (fun evbox -> add_key_binding key callback evbox)
1063         keyBindingBoxes
1064
1065     method setQuitCallback callback =
1066       connect_menu_item main#quitMenuItem callback;
1067       ignore (main#toplevel#event#connect#delete
1068         (fun _ -> callback ();true));
1069       self#addKeyBinding GdkKeysyms._q callback
1070
1071     method chooseFile ?(ok_not_exists = false) () =
1072       _ok_not_exists <- ok_not_exists;
1073       _only_directory <- false;
1074       fileSel#fileSelectionWin#show ();
1075       GtkThread.main ();
1076       chosen_file
1077
1078     method private chooseDir ?(ok_not_exists = false) () =
1079       _ok_not_exists <- ok_not_exists;
1080       _only_directory <- true;
1081       fileSel#fileSelectionWin#show ();
1082       GtkThread.main ();
1083       (* we should check that this is a directory *)
1084       chosen_file
1085
1086     method createDevelopment ~containing =
1087       next_devel_must_contain <- containing;
1088       newDevel#toplevel#misc#show()
1089
1090     method askText ?(title = "") ?(msg = "") () =
1091       let dialog = new textDialog () in
1092       dialog#textDialog#set_title title;
1093       dialog#textDialogLabel#set_label msg;
1094       let text = ref None in
1095       let return v =
1096         text := v;
1097         dialog#textDialog#destroy ();
1098         GMain.Main.quit ()
1099       in
1100       ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
1101       connect_button dialog#textDialogCancelButton (fun _ -> return None);
1102       connect_button dialog#textDialogOkButton (fun _ ->
1103         let text = dialog#textDialogTextView#buffer#get_text () in
1104         return (Some text));
1105       dialog#textDialog#show ();
1106       GtkThread.main ();
1107       !text
1108
1109     method private updateFontSize () =
1110       self#sourceView#misc#modify_font_by_name
1111         (sprintf "%s %d" BuildTimeConf.script_font font_size)
1112
1113     method increaseFontSize () =
1114       font_size <- font_size + 1;
1115       self#updateFontSize ()
1116
1117     method decreaseFontSize () =
1118       font_size <- font_size - 1;
1119       self#updateFontSize ()
1120
1121     method resetFontSize () =
1122       font_size <- default_font_size;
1123       self#updateFontSize ()
1124
1125   end
1126
1127 let gui () =
1128   let g = new gui () in
1129   gui_instance := Some g;
1130   MatitaMathView.set_gui g;
1131   g
1132
1133 let instance = singleton gui
1134
1135 let non p x = not (p x)
1136
1137 (* this is a shit and should be changed :-{ *)
1138 let interactive_uri_choice
1139   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
1140   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
1141   ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
1142   ?copy_cb ()
1143   ~id uris
1144 =
1145   let gui = instance () in
1146   let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
1147   if (selection_mode <> `SINGLE) &&
1148     (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
1149   then
1150     Lazy.force nonvars_uris
1151   else begin
1152     let dialog = gui#newUriDialog () in
1153     if hide_uri_entry then
1154       dialog#uriEntryHBox#misc#hide ();
1155     if hide_try then
1156       begin
1157       dialog#uriChoiceSelectedButton#misc#hide ();
1158       dialog#uriChoiceConstantsButton#misc#hide ();
1159       end;
1160     dialog#okLabel#set_label ok_label;
1161     dialog#uriChoiceTreeView#selection#set_mode
1162       (selection_mode :> Gtk.Tags.selection_mode);
1163     let model = new stringListModel dialog#uriChoiceTreeView in
1164     let choices = ref None in
1165     (match copy_cb with
1166     | None -> ()
1167     | Some cb ->
1168         dialog#copyButton#misc#show ();
1169         connect_button dialog#copyButton
1170         (fun _ ->
1171           match model#easy_selection () with
1172           | [u] -> (cb u)
1173           | _ -> ()));
1174     dialog#uriChoiceDialog#set_title title;
1175     dialog#uriChoiceLabel#set_text msg;
1176     List.iter model#easy_append (List.map UriManager.string_of_uri uris);
1177     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
1178     let return v =
1179       choices := v;
1180       dialog#uriChoiceDialog#destroy ();
1181       GMain.Main.quit ()
1182     in
1183     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
1184     connect_button dialog#uriChoiceConstantsButton (fun _ ->
1185       return (Some (Lazy.force nonvars_uris)));
1186     if ok_action = `AUTO then
1187       connect_button dialog#uriChoiceAutoButton (fun _ ->
1188         Helm_registry.set_bool "matita.auto_disambiguation" true;
1189         return (Some (Lazy.force nonvars_uris)))
1190     else
1191       connect_button dialog#uriChoiceAutoButton (fun _ ->
1192         match model#easy_selection () with
1193         | [] -> ()
1194         | uris -> return (Some (List.map UriManager.uri_of_string uris)));
1195     connect_button dialog#uriChoiceSelectedButton (fun _ ->
1196       match model#easy_selection () with
1197       | [] -> ()
1198       | uris -> return (Some (List.map UriManager.uri_of_string uris)));
1199     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
1200     dialog#uriChoiceDialog#show ();
1201     GtkThread.main ();
1202     (match !choices with
1203     | None -> raise MatitaTypes.Cancel
1204     | Some uris -> uris)
1205   end
1206
1207 class interpModel =
1208   let cols = new GTree.column_list in
1209   let id_col = cols#add Gobject.Data.string in
1210   let dsc_col = cols#add Gobject.Data.string in
1211   let interp_no_col = cols#add Gobject.Data.int in
1212   let tree_store = GTree.tree_store cols in
1213   let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
1214   let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
1215   let id_view_col = GTree.view_column ~renderer:id_renderer () in
1216   let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
1217   fun tree_view choices ->
1218     object
1219       initializer
1220         tree_view#set_model (Some (tree_store :> GTree.model));
1221         ignore (tree_view#append_column id_view_col);
1222         ignore (tree_view#append_column dsc_view_col);
1223         let name_of_interp =
1224           (* try to find a reasonable name for an interpretation *)
1225           let idx = ref 0 in
1226           fun interp ->
1227             try
1228               List.assoc "0" interp
1229             with Not_found ->
1230               incr idx; string_of_int !idx
1231         in
1232         tree_store#clear ();
1233         let idx = ref ~-1 in
1234         List.iter
1235           (fun interp ->
1236             incr idx;
1237             let interp_row = tree_store#append () in
1238             tree_store#set ~row:interp_row ~column:id_col
1239               (name_of_interp interp);
1240             tree_store#set ~row:interp_row ~column:interp_no_col !idx;
1241             List.iter
1242               (fun (id, dsc) ->
1243                 let row = tree_store#append ~parent:interp_row () in
1244                 tree_store#set ~row ~column:id_col id;
1245                 tree_store#set ~row ~column:dsc_col dsc;
1246                 tree_store#set ~row ~column:interp_no_col !idx)
1247               interp)
1248           choices
1249
1250       method get_interp_no tree_path =
1251         let iter = tree_store#get_iter tree_path in
1252         tree_store#get ~row:iter ~column:interp_no_col
1253     end
1254
1255 let interactive_interp_choice () choices =
1256   let gui = instance () in
1257   assert (choices <> []);
1258   let dialog = gui#newRecordDialog () in
1259   let model = new interpModel dialog#recordChoiceTreeView choices in
1260   dialog#recordChoiceDialog#set_title "Interpretation choice";
1261   dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
1262   let interp_no = ref None in
1263   let return _ =
1264     dialog#recordChoiceDialog#destroy ();
1265     GMain.Main.quit ()
1266   in
1267   let fail _ = interp_no := None; return () in
1268   ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
1269   connect_button dialog#recordChoiceOkButton (fun _ ->
1270     match !interp_no with None -> () | Some _ -> return ());
1271   connect_button dialog#recordChoiceCancelButton fail;
1272   ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
1273     interp_no := Some (model#get_interp_no path);
1274     return ()));
1275   let selection = dialog#recordChoiceTreeView#selection in
1276   ignore (selection#connect#changed (fun _ ->
1277     match selection#get_selected_rows with
1278     | [path] -> interp_no := Some (model#get_interp_no path)
1279     | _ -> assert false));
1280   dialog#recordChoiceDialog#show ();
1281   GtkThread.main ();
1282   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
1283
1284 let _ =
1285   (* disambiguator callbacks *)
1286   GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
1287   GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
1288   (* gtk initialization *)
1289   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
1290   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
1291   ignore (GMain.Main.init ())
1292