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 all_disambiguation_passes = ref false
  37
  38 let gui_instance = ref None
  39
  40 class type browserWin =
  41   (* this class exists only because GEdit.combo_box_entry is not supported by
  42    * lablgladecc :-(((( *)
  43 object
  44   inherit MatitaGeneratedGui.browserWin
  45   method browserUri: GEdit.combo_box_entry
  46 end
  47
  48 class console ~(buffer: GText.buffer) () =
  49   object (self)
  50     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
  51     val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
  52     val message_tag = buffer#create_tag []
  53     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
  54     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
  55     method error s   = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
  56     method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
  57     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
  58     method clear () =
  59       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
  60     method log_callback (tag: HLog.log_tag) s =
  61       match tag with
  62       | `Debug -> self#debug (s ^ "\n")
  63       | `Error -> self#error (s ^ "\n")
  64       | `Message -> self#message (s ^ "\n")
  65       | `Warning -> self#warning (s ^ "\n")
  66   end
  67
  68 let clean_current_baseuri grafite_status =
  69   LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
  70
  71 let save_moo lexicon_status grafite_status =
  72   let script = MatitaScript.current () in
  73   let baseuri = GrafiteTypes.get_baseuri grafite_status in
  74   let no_pstatus =
  75     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
  76   in
  77   match script#bos, script#eos, no_pstatus with
  78   | true, _, _ -> ()
  79   | _, true, true ->
  80      let moo_fname =
  81        LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
  82         ~writable:true in
  83      let lexicon_fname =
  84        LibraryMisc.lexicon_file_of_baseuri
  85          ~must_exist:false ~baseuri ~writable:true
  86      in
  87      GrafiteMarshal.save_moo moo_fname
  88        grafite_status.GrafiteTypes.moo_content_rev;
  89      LexiconMarshal.save_lexicon lexicon_fname
  90        lexicon_status.LexiconEngine.lexicon_content_rev
  91   | _ -> clean_current_baseuri grafite_status
  92 ;;
  93
  94 let ask_unsaved parent =
  95   MatitaGtkMisc.ask_confirmation
  96     ~parent ~title:"Unsaved work!"
  97     ~message:("Your work is <b>unsaved</b>!\n\n"^
  98          "<i>Do you want to save the script before continuing?</i>")
  99     ()
 100
 101 class interpErrorModel =
 102   let cols = new GTree.column_list in
 103   let id_col = cols#add Gobject.Data.string in
 104   let dsc_col = cols#add Gobject.Data.string in
 105   let interp_no_col = cols#add Gobject.Data.caml in
 106   let tree_store = GTree.tree_store cols in
 107   let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
 108   let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
 109   let id_view_col = GTree.view_column ~renderer:id_renderer () in
 110   let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
 111   fun (tree_view: GTree.view) choices ->
 112     object
 113       initializer
 114         tree_view#set_model (Some (tree_store :> GTree.model));
 115         ignore (tree_view#append_column id_view_col);
 116         ignore (tree_view#append_column dsc_view_col);
 117         tree_store#clear ();
 118         let idx1 = ref ~-1 in
 119         List.iter
 120           (fun _,lll ->
 121             incr idx1;
 122             let loc_row =
 123              if List.length choices = 1 then
 124               None
 125              else
 126               (let loc_row = tree_store#append () in
 127                 begin
 128                  match lll with
 129                     [passes,envs_and_diffs,_,_] ->
 130                       tree_store#set ~row:loc_row ~column:id_col
 131                        ("Error location " ^ string_of_int (!idx1+1) ^
 132                         ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
 133                         " (in passes " ^
 134                         String.concat " " (List.map string_of_int passes) ^
 135                         ")");
 136                       tree_store#set ~row:loc_row ~column:interp_no_col
 137                        (!idx1,Some 0,None);
 138                   | _ ->
 139                     tree_store#set ~row:loc_row ~column:id_col
 140                      ("Error location " ^ string_of_int (!idx1+1));
 141                     tree_store#set ~row:loc_row ~column:interp_no_col
 142                      (!idx1,None,None);
 143                 end ;
 144                 Some loc_row) in
 145             let idx2 = ref ~-1 in
 146              List.iter
 147               (fun passes,envs_and_diffs,_,_ ->
 148                 incr idx2;
 149                 let msg_row =
 150                  if List.length lll = 1 then
 151                   loc_row
 152                  else
 153                   let msg_row = tree_store#append ?parent:loc_row () in
 154                    (tree_store#set ~row:msg_row ~column:id_col
 155                      ("Error message " ^ string_of_int (!idx1+1) ^ "." ^
 156                       string_of_int (!idx2+1) ^
 157                       " (in passes " ^
 158                       String.concat " " (List.map string_of_int passes) ^
 159                       ")");
 160                     tree_store#set ~row:msg_row ~column:interp_no_col
 161                      (!idx1,Some !idx2,None);
 162                     Some msg_row) in
 163                 let idx3 = ref ~-1 in
 164                 List.iter
 165                  (fun (passes,env,_) ->
 166                    incr idx3;
 167                    let interp_row =
 168                     match envs_and_diffs with
 169                        _::_::_ ->
 170                         let interp_row = tree_store#append ?parent:msg_row () in
 171                         tree_store#set ~row:interp_row ~column:id_col
 172                           ("Interpretation " ^ string_of_int (!idx3+1) ^
 173                            " (in passes " ^
 174                            String.concat " " (List.map string_of_int passes) ^
 175                            ")");
 176                         tree_store#set ~row:interp_row ~column:interp_no_col
 177                          (!idx1,Some !idx2,Some !idx3);
 178                         Some interp_row
 179                      | [_] -> msg_row
 180                      | [] -> assert false
 181                    in
 182                     List.iter
 183                      (fun (_, id, dsc) ->
 184                        let row = tree_store#append ?parent:interp_row () in
 185                        tree_store#set ~row ~column:id_col id;
 186                        tree_store#set ~row ~column:dsc_col dsc;
 187                        tree_store#set ~row ~column:interp_no_col
 188                         (!idx1,Some !idx2,Some !idx3)
 189                      ) env
 190                  ) envs_and_diffs
 191               ) lll ;
 192              if List.length lll > 1 then
 193               HExtlib.iter_option
 194                (fun p -> tree_view#expand_row (tree_store#get_path p))
 195                loc_row
 196           ) choices
 197
 198       method get_interp_no tree_path =
 199         let iter = tree_store#get_iter tree_path in
 200         tree_store#get ~row:iter ~column:interp_no_col
 201     end
 202
 203
 204 let rec interactive_error_interp ~all_passes
 205   (source_buffer:GSourceView.source_buffer) notify_exn offset errorll filename
 206 =
 207   (* hook to save a script for each disambiguation error *)
 208   if false then
 209    (let text =
 210      source_buffer#get_text ~start:source_buffer#start_iter
 211       ~stop:source_buffer#end_iter () in
 212     let md5 = Digest.to_hex (Digest.string text) in
 213     let filename =
 214      Filename.chop_extension filename ^ ".error." ^ md5 ^ ".ma"  in
 215     let ch = open_out filename in
 216      output_string ch text;
 217     close_out ch
 218    );
 219   assert (List.flatten errorll <> []);
 220   let errorll' =
 221    let remove_non_significant =
 222      List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
 223    let annotated_errorll () =
 224     List.rev
 225      (snd
 226        (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[])
 227          errorll)) in
 228    if all_passes then annotated_errorll () else
 229      let safe_list_nth l n = try List.nth l n with Failure _ -> [] in
 230     (* We remove passes 1,2 and 5,6 *)
 231      let res =
 232       (1,[])::(2,[])
 233       ::(3,remove_non_significant (safe_list_nth errorll 2))
 234       ::(4,remove_non_significant (safe_list_nth errorll 3))
 235       ::(5,[])::(6,[])::[]
 236      in
 237       if List.flatten (List.map snd res) <> [] then res
 238       else
 239        (* all errors (if any) are not significant: we keep them *)
 240        let res =
 241         (1,[])::(2,[])
 242         ::(3,(safe_list_nth errorll 2))
 243         ::(4,(safe_list_nth errorll 3))
 244         ::(5,[])::(6,[])::[]
 245        in
 246         if List.flatten (List.map snd res) <> [] then
 247          begin
 248           HLog.warn
 249            "All disambiguation errors are not significant. Showing them anyway." ;
 250           res
 251          end
 252         else
 253          begin
 254           HLog.warn
 255            "No errors in phases 2 and 3. Showing all errors in all phases" ;
 256           annotated_errorll ()
 257          end
 258    in
 259   let choices = MatitaExcPp.compact_disambiguation_errors all_passes errorll' in
 260    match choices with
 261       [] -> assert false
 262     | [loffset,[_,envs_and_diffs,msg,significant]] ->
 263         let _,env,diff = List.hd envs_and_diffs in
 264          notify_exn
 265           (GrafiteDisambiguator.DisambiguationError
 266             (offset,[[env,diff,loffset,msg,significant]]));
 267     | _::_ ->
 268        let dialog = new disambiguationErrors () in
 269        dialog#check_widgets ();
 270        if all_passes then
 271         dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
 272        let model = new interpErrorModel dialog#treeview choices in
 273        dialog#disambiguationErrors#set_title "Disambiguation error";
 274        dialog#disambiguationErrorsLabel#set_label
 275         "Click on an error to see the corresponding message:";
 276        ignore (dialog#treeview#connect#cursor_changed
 277         (fun _ ->
 278           let tree_path =
 279            match fst (dialog#treeview#get_cursor ()) with
 280               None -> assert false
 281            | Some tp -> tp in
 282           let idx1,idx2,idx3 = model#get_interp_no tree_path in
 283           let loffset,lll = List.nth choices idx1 in
 284           let _,envs_and_diffs,msg,significant =
 285            match idx2 with
 286               Some idx2 -> List.nth lll idx2
 287             | None ->
 288                 [],[],lazy "Multiple error messages. Please select one.",true
 289           in
 290           let _,env,diff =
 291            match idx3 with
 292               Some idx3 -> List.nth envs_and_diffs idx3
 293             | None -> [],[],[] (* dymmy value, used *) in
 294           let script = MatitaScript.current () in
 295           let error_tag = script#error_tag in
 296            source_buffer#remove_tag error_tag
 297              ~start:source_buffer#start_iter
 298              ~stop:source_buffer#end_iter;
 299            notify_exn
 300             (GrafiteDisambiguator.DisambiguationError
 301               (offset,[[env,diff,loffset,msg,significant]]))
 302            ));
 303        let return _ =
 304          dialog#disambiguationErrors#destroy ();
 305          GMain.Main.quit ()
 306        in
 307        let fail _ = return () in
 308        ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
 309        connect_button dialog#disambiguationErrorsOkButton
 310         (fun _ ->
 311           let tree_path =
 312            match fst (dialog#treeview#get_cursor ()) with
 313               None -> assert false
 314            | Some tp -> tp in
 315           let idx1,idx2,idx3 = model#get_interp_no tree_path in
 316           let diff =
 317            match idx2,idx3 with
 318               Some idx2, Some idx3 ->
 319                let _,lll = List.nth choices idx1 in
 320                let _,envs_and_diffs,_,_ = List.nth lll idx2 in
 321                let _,_,diff = List.nth envs_and_diffs idx3 in
 322                 diff
 323             | _,_ -> assert false
 324           in
 325            let newtxt =
 326             String.concat "\n"
 327              ("" ::
 328                List.map
 329                 (fun k,value ->
 330                   DisambiguatePp.pp_environment
 331                    (DisambiguateTypes.Environment.add k value
 332                      DisambiguateTypes.Environment.empty))
 333                 diff) ^ "\n"
 334            in
 335             source_buffer#insert
 336              ~iter:
 337                (source_buffer#get_iter_at_mark
 338                 (`NAME "beginning_of_statement")) newtxt ;
 339             return ()
 340         );
 341        connect_button dialog#disambiguationErrorsMoreErrors
 342         (fun _ -> return () ;
 343           interactive_error_interp ~all_passes:true source_buffer
 344            notify_exn offset errorll filename);
 345        connect_button dialog#disambiguationErrorsCancelButton fail;
 346        dialog#disambiguationErrors#show ();
 347        GtkThread.main ()
 348
 349
 350 (** Selection handling
 351  * Two clipboards are used: "clipboard" and "primary".
 352  * "primary" is used by X, when you hit the middle button mouse is content is
 353  *    pasted between applications. In Matita this selection always contain the
 354  *    textual version of the selected term.
 355  * "clipboard" is used inside Matita only and support ATM two different targets:
 356  *    "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may
 357  *    be added
 358  *)
 359
 360 class gui () =
 361     (* creation order _is_ relevant for windows placement *)
 362   let main = new mainWin () in
 363   let fileSel = new fileSelectionWin () in
 364   let findRepl = new findReplWin () in
 365   let develList = new develListWin () in
 366   let newDevel = new newDevelWin () in
 367   let keyBindingBoxes = (* event boxes which should receive global key events *)
 368     [ main#mainWinEventBox ]
 369   in
 370   let console = new console ~buffer:main#logTextView#buffer () in
 371   let (source_view: GSourceView.source_view) =
 372     GSourceView.source_view
 373       ~auto_indent:true
 374       ~insert_spaces_instead_of_tabs:true ~tabs_width:2
 375       ~margin:80 ~show_margin:true
 376       ~smart_home_end:true
 377       ~packing:main#scriptScrolledWin#add
 378       ()
 379   in
 380   let default_font_size =
 381     Helm_registry.get_opt_default Helm_registry.int
 382       ~default:BuildTimeConf.default_font_size "matita.font_size"
 383   in
 384   let source_buffer = source_view#source_buffer in
 385   object (self)
 386     val mutable chosen_file = None
 387     val mutable _ok_not_exists = false
 388     val mutable _only_directory = false
 389     val mutable font_size = default_font_size
 390     val mutable next_devel_must_contain = None
 391     val mutable next_ligatures = []
 392     val clipboard = GData.clipboard Gdk.Atom.clipboard
 393     val primary = GData.clipboard Gdk.Atom.primary
 394
 395     initializer
 396       let s () = MatitaScript.current () in
 397         (* glade's check widgets *)
 398       List.iter (fun w -> w#check_widgets ())
 399         (let c w = (w :> <check_widgets: unit -> unit>) in
 400         [ c fileSel; c main; c findRepl]);
 401         (* key bindings *)
 402       List.iter (* global key bindings *)
 403         (fun (key, callback) -> self#addKeyBinding key callback)
 404 (*
 405         [ GdkKeysyms._F3,
 406             toggle_win ~check:main#showProofMenuItem proof#proofWin;
 407           GdkKeysyms._F4,
 408             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 409 *)
 410         [ ];
 411         (* about win *)
 412       let parse_txt_file file =
 413        let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
 414        let l_rev = ref [] in
 415        try
 416         while true do
 417          l_rev := input_line ch :: !l_rev;
 418         done;
 419         assert false
 420        with
 421         End_of_file ->
 422          close_in ch;
 423          List.rev !l_rev in
 424       let about_dialog =
 425        GWindow.about_dialog
 426         ~authors:(parse_txt_file "AUTHORS")
 427         (*~comments:"comments"*)
 428         ~copyright:"Copyright (C) 2005, the HELM team"
 429         ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
 430         ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png"))
 431         ~name:"Matita"
 432         ~version:BuildTimeConf.version
 433         ~website:"http://helm.cs.unibo.it"
 434         ()
 435       in
 436       connect_menu_item main#contentsMenuItem (fun () ->
 437         let cmd =
 438           sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
 439         in
 440         ignore (Sys.command cmd));
 441       connect_menu_item main#aboutMenuItem about_dialog#present;
 442         (* findRepl win *)
 443       let show_find_Repl () =
 444         findRepl#toplevel#misc#show ();
 445         findRepl#toplevel#misc#grab_focus ()
 446       in
 447       let hide_find_Repl () = findRepl#toplevel#misc#hide () in
 448       let find_forward _ =
 449           let highlight start end_ =
 450             source_buffer#move_mark `INSERT ~where:start;
 451             source_buffer#move_mark `SEL_BOUND ~where:end_;
 452             source_view#scroll_mark_onscreen `INSERT
 453           in
 454           let text = findRepl#findEntry#text in
 455           let iter = source_buffer#get_iter `SEL_BOUND in
 456           match iter#forward_search text with
 457           | None ->
 458               (match source_buffer#start_iter#forward_search text with
 459               | None -> ()
 460               | Some (start,end_) -> highlight start end_)
 461           | Some (start,end_) -> highlight start end_
 462       in
 463       let replace _ =
 464         let text = findRepl#replaceEntry#text in
 465         let ins = source_buffer#get_iter `INSERT in
 466         let sel = source_buffer#get_iter `SEL_BOUND in
 467         if ins#compare sel < 0 then
 468           begin
 469             ignore(source_buffer#delete_selection ());
 470             source_buffer#insert text
 471           end
 472       in
 473       connect_button findRepl#findButton find_forward;
 474       connect_button findRepl#findReplButton replace;
 475       connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
 476       ignore(findRepl#toplevel#event#connect#delete
 477         ~callback:(fun _ -> hide_find_Repl ();true));
 478       let safe_undo =
 479        fun () ->
 480         (* phase 1: we save the actual status of the marks and we undo *)
 481         let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
 482         let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
 483         let locked_iter_offset = locked_iter#offset in
 484         let mark2 =
 485          `MARK
 486            (source_view#buffer#create_mark ~name:"lock_point"
 487              ~left_gravity:true locked_iter) in
 488         source_view#source_buffer#undo ();
 489         (* phase 2: we save the cursor position and we redo, restoring
 490            the previous status of all the marks *)
 491         let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
 492         let mark =
 493          `MARK
 494            (source_view#buffer#create_mark ~name:"undo_point"
 495              ~left_gravity:true cursor_iter)
 496         in
 497          source_view#source_buffer#redo ();
 498          let mark_iter = source_view#buffer#get_iter_at_mark mark in
 499          let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
 500          let mark2_iter = mark2_iter#set_offset locked_iter_offset in
 501           source_view#buffer#move_mark locked_mark ~where:mark2_iter;
 502           source_view#buffer#delete_mark mark;
 503           source_view#buffer#delete_mark mark2;
 504           (* phase 3: if after the undo the cursor was in the locked area,
 505              then we move it there again and we perform a goto *)
 506           if mark_iter#offset < locked_iter_offset then
 507            begin
 508             source_view#buffer#move_mark `INSERT ~where:mark_iter;
 509             (MatitaScript.current ())#goto `Cursor ();
 510            end;
 511           (* phase 4: we perform again the undo. This time we are sure that
 512              the text to undo is not locked *)
 513           source_view#source_buffer#undo ();
 514           source_view#misc#grab_focus () in
 515       let safe_redo =
 516        fun () ->
 517         (* phase 1: we save the actual status of the marks, we redo and
 518            we undo *)
 519         let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
 520         let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
 521         let locked_iter_offset = locked_iter#offset in
 522         let mark2 =
 523          `MARK
 524            (source_view#buffer#create_mark ~name:"lock_point"
 525              ~left_gravity:true locked_iter) in
 526         source_view#source_buffer#redo ();
 527         source_view#source_buffer#undo ();
 528         (* phase 2: we save the cursor position and we restore
 529            the previous status of all the marks *)
 530         let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
 531         let mark =
 532          `MARK
 533            (source_view#buffer#create_mark ~name:"undo_point"
 534              ~left_gravity:true cursor_iter)
 535         in
 536          let mark_iter = source_view#buffer#get_iter_at_mark mark in
 537          let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
 538          let mark2_iter = mark2_iter#set_offset locked_iter_offset in
 539           source_view#buffer#move_mark locked_mark ~where:mark2_iter;
 540           source_view#buffer#delete_mark mark;
 541           source_view#buffer#delete_mark mark2;
 542           (* phase 3: if after the undo the cursor is in the locked area,
 543              then we move it there again and we perform a goto *)
 544           if mark_iter#offset < locked_iter_offset then
 545            begin
 546             source_view#buffer#move_mark `INSERT ~where:mark_iter;
 547             (MatitaScript.current ())#goto `Cursor ();
 548            end;
 549           (* phase 4: we perform again the redo. This time we are sure that
 550              the text to redo is not locked *)
 551           source_view#source_buffer#redo ();
 552           source_view#misc#grab_focus ()
 553       in
 554       connect_menu_item main#undoMenuItem safe_undo;
 555       ignore(source_view#source_buffer#connect#can_undo
 556         ~callback:main#undoMenuItem#misc#set_sensitive);
 557       connect_menu_item main#redoMenuItem safe_redo;
 558       ignore(source_view#source_buffer#connect#can_redo
 559         ~callback:main#redoMenuItem#misc#set_sensitive);
 560       ignore(source_view#connect#after#populate_popup
 561        ~callback:(fun pre_menu ->
 562          let menu = new GMenu.menu pre_menu in
 563          let menuItems = menu#children in
 564          let undoMenuItem, redoMenuItem =
 565           match menuItems with
 566              [undo;redo;sep1;cut;copy;paste;delete;sep2;
 567               selectall;sep3;inputmethod;insertunicodecharacter] ->
 568                 List.iter menu#remove [ copy; cut; delete; paste ];
 569                 undo,redo
 570            | _ -> assert false in
 571          let add_menu_item =
 572            let i = ref 2 in (* last occupied position *)
 573            fun ?label ?stock () ->
 574              incr i;
 575              GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
 576               ()
 577          in
 578          let copy = add_menu_item ~stock:`COPY () in
 579          let cut = add_menu_item ~stock:`CUT () in
 580          let delete = add_menu_item ~stock:`DELETE () in
 581          let paste = add_menu_item ~stock:`PASTE () in
 582          let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
 583          copy#misc#set_sensitive self#canCopy;
 584          cut#misc#set_sensitive self#canCut;
 585          delete#misc#set_sensitive self#canDelete;
 586          paste#misc#set_sensitive self#canPaste;
 587          paste_pattern#misc#set_sensitive self#canPastePattern;
 588          connect_menu_item copy self#copy;
 589          connect_menu_item cut self#cut;
 590          connect_menu_item delete self#delete;
 591          connect_menu_item paste self#paste;
 592          connect_menu_item paste_pattern self#pastePattern;
 593          let new_undoMenuItem =
 594           GMenu.image_menu_item
 595            ~image:(GMisc.image ~stock:`UNDO ())
 596            ~use_mnemonic:true
 597            ~label:"_Undo"
 598            ~packing:(menu#insert ~pos:0) () in
 599          new_undoMenuItem#misc#set_sensitive
 600           (undoMenuItem#misc#get_flag `SENSITIVE);
 601          menu#remove (undoMenuItem :> GMenu.menu_item);
 602          connect_menu_item new_undoMenuItem safe_undo;
 603          let new_redoMenuItem =
 604           GMenu.image_menu_item
 605            ~image:(GMisc.image ~stock:`REDO ())
 606            ~use_mnemonic:true
 607            ~label:"_Redo"
 608            ~packing:(menu#insert ~pos:1) () in
 609          new_redoMenuItem#misc#set_sensitive
 610           (redoMenuItem#misc#get_flag `SENSITIVE);
 611           menu#remove (redoMenuItem :> GMenu.menu_item);
 612           connect_menu_item new_redoMenuItem safe_redo));
 613
 614       connect_menu_item main#editMenu (fun () ->
 615         main#copyMenuItem#misc#set_sensitive self#canCopy;
 616         main#cutMenuItem#misc#set_sensitive self#canCut;
 617         main#deleteMenuItem#misc#set_sensitive self#canDelete;
 618         main#pasteMenuItem#misc#set_sensitive self#canPaste;
 619         main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern);
 620       connect_menu_item main#copyMenuItem self#copy;
 621       connect_menu_item main#cutMenuItem self#cut;
 622       connect_menu_item main#deleteMenuItem self#delete;
 623       connect_menu_item main#pasteMenuItem self#paste;
 624       connect_menu_item main#pastePatternMenuItem self#pastePattern;
 625       connect_menu_item main#selectAllMenuItem (fun () ->
 626         source_buffer#move_mark `INSERT source_buffer#start_iter;
 627         source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
 628       connect_menu_item main#findReplMenuItem show_find_Repl;
 629       connect_menu_item main#externalEditorMenuItem self#externalEditor;
 630       connect_menu_item main#ligatureButton self#nextLigature;
 631       ignore (findRepl#findEntry#connect#activate find_forward);
 632         (* interface lockers *)
 633       let lock_world _ =
 634         main#buttonsToolbar#misc#set_sensitive false;
 635         develList#buttonsHbox#misc#set_sensitive false;
 636         main#scriptMenu#misc#set_sensitive false;
 637         source_view#set_editable false
 638       in
 639       let unlock_world _ =
 640         main#buttonsToolbar#misc#set_sensitive true;
 641         develList#buttonsHbox#misc#set_sensitive true;
 642         main#scriptMenu#misc#set_sensitive true;
 643         source_view#set_editable true;
 644         (*The next line seems sufficient to avoid some unknown race condition *)
 645         GtkThread.sync (fun () -> ()) ()
 646       in
 647       let worker_thread = ref None in
 648       let notify_exn exn =
 649        let floc, msg = MatitaExcPp.to_string exn in
 650         begin
 651          match floc with
 652             None -> ()
 653           | Some floc ->
 654              let (x, y) = HExtlib.loc_of_floc floc in
 655              let script = MatitaScript.current () in
 656              let locked_mark = script#locked_mark in
 657              let error_tag = script#error_tag in
 658              let baseoffset =
 659               (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
 660              let x' = baseoffset + x in
 661              let y' = baseoffset + y in
 662              let x_iter = source_buffer#get_iter (`OFFSET x') in
 663              let y_iter = source_buffer#get_iter (`OFFSET y') in
 664              source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
 665              let id = ref None in
 666              id := Some (source_buffer#connect#changed ~callback:(fun () ->
 667                source_buffer#remove_tag error_tag
 668                  ~start:source_buffer#start_iter
 669                  ~stop:source_buffer#end_iter;
 670                match !id with
 671                | None -> assert false (* a race condition occurred *)
 672                | Some id ->
 673                    (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
 674              source_buffer#place_cursor
 675               (source_buffer#get_iter (`OFFSET x'));
 676         end;
 677         HLog.error msg in
 678       let locker f () =
 679        let thread_main =
 680         fun () ->
 681           lock_world ();
 682           try
 683            f ();
 684            unlock_world ()
 685           with
 686            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
 687               (try
 688                 interactive_error_interp
 689                  ~all_passes:!all_disambiguation_passes source_buffer
 690                  notify_exn offset errorll (s())#filename
 691                with
 692                 exc -> notify_exn exc);
 693               unlock_world ()
 694            | exc ->
 695               notify_exn exc;
 696               unlock_world ()
 697        in
 698        (*thread_main ();*)
 699        worker_thread := Some (Thread.create thread_main ())
 700       in
 701       let kill_worker =
 702        (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
 703        let interrupt = ref None in
 704        let old_callback = ref (function _ -> ()) in
 705        let force_interrupt n =
 706          (* This function is called just before the thread's timeslice ends *)
 707          !old_callback n;
 708          if Some(Thread.id(Thread.self())) = !interrupt then
 709           (interrupt := None; raise Sys.Break) in
 710        let _ =
 711         match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with
 712            Sys.Signal_handle f -> old_callback := f
 713          | Sys.Signal_ignore
 714          | Sys.Signal_default -> assert false
 715        in
 716         fun () ->
 717          match !worker_thread with
 718             None -> assert false
 719           | Some t -> interrupt := Some (Thread.id t) in
 720       let keep_focus f =
 721         fun () ->
 722          try
 723           f (); source_view#misc#grab_focus ()
 724          with
 725           exc -> source_view#misc#grab_focus (); raise exc in
 726         (* developments win *)
 727       let model =
 728         new MatitaGtkMisc.multiStringListModel
 729           ~cols:2 develList#developmentsTreeview
 730       in
 731       let refresh_devels_win () =
 732         model#list_store#clear ();
 733         List.iter
 734           (fun (name, root) -> model#easy_mappend [name;root])
 735           (MatitamakeLib.list_known_developments ())
 736       in
 737       let get_devel_selected () =
 738         match model#easy_mselection () with
 739         | [[name;_]] -> MatitamakeLib.development_for_name name
 740         | _ -> None
 741       in
 742       let refresh () =
 743         while Glib.Main.pending () do
 744           ignore(Glib.Main.iteration false);
 745         done
 746       in
 747       connect_button develList#newButton
 748         (fun () ->
 749           next_devel_must_contain <- None;
 750           newDevel#toplevel#misc#show());
 751       connect_button develList#deleteButton
 752         (locker (fun () ->
 753           (match get_devel_selected () with
 754           | None -> ()
 755           | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
 756           refresh_devels_win ()));
 757       connect_button develList#buildButton
 758         (locker (fun () ->
 759           match get_devel_selected () with
 760           | None -> ()
 761           | Some d ->
 762               let build = locker
 763                 (fun () -> MatitamakeLib.build_development_in_bg refresh d)
 764               in
 765               ignore(build ())));
 766       connect_button develList#cleanButton
 767         (locker (fun () ->
 768           match get_devel_selected () with
 769           | None -> ()
 770           | Some d ->
 771               let clean = locker
 772                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
 773               in
 774               ignore(clean ())));
 775       (* publish button hidden, use command line
 776       connect_button develList#publishButton
 777         (locker (fun () ->
 778           match get_devel_selected () with
 779           | None -> ()
 780           | Some d ->
 781               let publish = locker (fun () ->
 782                 MatitamakeLib.publish_development_in_bg refresh d) in
 783               ignore(publish ())));
 784               *)
 785       develList#publishButton#misc#hide ();
 786       connect_button develList#graphButton (fun () ->
 787         match get_devel_selected () with
 788         | None -> ()
 789         | Some d ->
 790             (match MatitamakeLib.dot_for_development d with
 791             | None -> ()
 792             | Some _ ->
 793                 let browser = MatitaMathView.cicBrowser () in
 794                 browser#load (`Development
 795                   (MatitamakeLib.name_for_development d))));
 796       connect_button develList#closeButton
 797         (fun () -> develList#toplevel#misc#hide());
 798       ignore(develList#toplevel#event#connect#delete
 799         (fun _ -> develList#toplevel#misc#hide();true));
 800       connect_menu_item main#developmentsMenuItem
 801         (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
 802
 803         (* add development win *)
 804       let check_if_root_contains root =
 805         match next_devel_must_contain with
 806         | None -> true
 807         | Some path ->
 808             let is_prefix_of d1 d2 =
 809               let d1 = MatitamakeLib.normalize_path d1 in
 810               let d2 = MatitamakeLib.normalize_path d2 in
 811               let len1 = String.length d1 in
 812               let len2 = String.length d2 in
 813               if len2 < len1 then
 814                 false
 815               else
 816                 let pref = String.sub d2 0 len1 in
 817                 pref = d1
 818             in
 819             is_prefix_of root path
 820       in
 821       connect_button newDevel#addButton
 822        (fun () ->
 823           let name = newDevel#nameEntry#text in
 824           let root = newDevel#rootEntry#text in
 825           if check_if_root_contains root then
 826             begin
 827               ignore (MatitamakeLib.initialize_development name root);
 828               refresh_devels_win ();
 829               newDevel#nameEntry#set_text "";
 830               newDevel#rootEntry#set_text "";
 831               newDevel#toplevel#misc#hide()
 832             end
 833           else
 834             HLog.error ("The selected root does not contain " ^
 835               match next_devel_must_contain with
 836               | Some x -> x
 837               | _ -> assert false));
 838       connect_button newDevel#chooseRootButton
 839        (fun () ->
 840          let path = self#chooseDir () in
 841          match path with
 842          | Some path -> newDevel#rootEntry#set_text path
 843          | None -> ());
 844       connect_button newDevel#cancelButton
 845        (fun () -> newDevel#toplevel#misc#hide ());
 846       ignore(newDevel#toplevel#event#connect#delete
 847         (fun _ -> newDevel#toplevel#misc#hide();true));
 848
 849         (* file selection win *)
 850       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
 851       ignore (fileSel#fileSelectionWin#connect#response (fun event ->
 852         let return r =
 853           chosen_file <- r;
 854           fileSel#fileSelectionWin#misc#hide ();
 855           GMain.Main.quit ()
 856         in
 857         match event with
 858         | `OK ->
 859             let fname = fileSel#fileSelectionWin#filename in
 860             if Sys.file_exists fname then
 861               begin
 862                 if HExtlib.is_regular fname && not (_only_directory) then
 863                   return (Some fname)
 864                 else if _only_directory && HExtlib.is_dir fname then
 865                   return (Some fname)
 866               end
 867             else
 868               begin
 869                 if _ok_not_exists then
 870                   return (Some fname)
 871               end
 872         | `CANCEL -> return None
 873         | `HELP -> ()
 874         | `DELETE_EVENT -> return None));
 875         (* menus *)
 876       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
 877         (* console *)
 878       let adj = main#logScrolledWin#vadjustment in
 879         ignore (adj#connect#changed
 880                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
 881       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
 882       (* TO BE REMOVED *)
 883       main#tacticsButtonsHandlebox#misc#hide ();
 884       main#tacticsBarMenuItem#misc#hide ();
 885       main#scriptNotebook#remove_page 1;
 886       main#scriptNotebook#set_show_tabs false;
 887       (* / TO BE REMOVED *)
 888       let module Hr = Helm_registry in
 889       MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
 890         ~callback:(function
 891           | true -> main#toplevel#fullscreen ()
 892           | false -> main#toplevel#unfullscreen ());
 893       main#fullscreenMenuItem#set_active false;
 894       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
 895         ~callback:(function
 896           | true ->
 897               CicNotation.set_active_notations
 898                 (List.map fst (CicNotation.get_all_notations ()))
 899           | false ->
 900               CicNotation.set_active_notations []);
 901       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
 902         ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
 903       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
 904         ~callback:(fun enabled ->
 905           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
 906       main#unicodeAsTexMenuItem#set_active
 907         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
 908         (* log *)
 909       HLog.set_log_callback self#console#log_callback;
 910       GtkSignal.user_handler :=
 911         (function
 912         | MatitaScript.ActionCancelled s -> HLog.error s
 913         | exn ->
 914           if not (Helm_registry.get_bool "matita.debug") then
 915            notify_exn exn
 916           else raise exn);
 917         (* script *)
 918       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
 919       let _ =
 920         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
 921         | None ->
 922             HLog.warn (sprintf "can't load language file %s"
 923               BuildTimeConf.lang_file)
 924         | Some matita_lang ->
 925             source_buffer#set_language matita_lang;
 926             source_buffer#set_highlight true
 927       in
 928       let disableSave () =
 929         (s())#assignFileName None;
 930         main#saveMenuItem#misc#set_sensitive false
 931       in
 932       let saveAsScript () =
 933         let script = s () in
 934         match self#chooseFile ~ok_not_exists:true () with
 935         | Some f ->
 936               HExtlib.touch f;
 937               script#assignFileName (Some f);
 938               script#saveToFile ();
 939               console#message ("'"^f^"' saved.\n");
 940               self#_enableSaveTo f
 941         | None -> ()
 942       in
 943       let saveScript () =
 944         let script = s () in
 945         if script#has_name then
 946           (script#saveToFile ();
 947           console#message ("'"^script#filename^"' saved.\n"))
 948         else saveAsScript ()
 949       in
 950       let abandon_script () =
 951         let lexicon_status = (s ())#lexicon_status in
 952         let grafite_status = (s ())#grafite_status in
 953         if source_view#buffer#modified then
 954           (match ask_unsaved main#toplevel with
 955           | `YES -> saveScript ()
 956           | `NO -> ()
 957           | `CANCEL -> raise MatitaTypes.Cancel);
 958         save_moo lexicon_status grafite_status
 959       in
 960       let loadScript () =
 961         let script = s () in
 962         try
 963           match self#chooseFile () with
 964           | Some f ->
 965               abandon_script ();
 966               script#reset ();
 967               script#assignFileName (Some f);
 968               source_view#source_buffer#begin_not_undoable_action ();
 969               script#loadFromFile f;
 970               source_view#source_buffer#end_not_undoable_action ();
 971               console#message ("'"^f^"' loaded.\n");
 972               self#_enableSaveTo f
 973           | None -> ()
 974         with MatitaTypes.Cancel -> ()
 975       in
 976       let newScript () =
 977         abandon_script ();
 978         source_view#source_buffer#begin_not_undoable_action ();
 979         (s ())#reset ();
 980         (s ())#template ();
 981         source_view#source_buffer#end_not_undoable_action ();
 982         disableSave ();
 983         (s ())#assignFileName None
 984       in
 985       let cursor () =
 986         source_buffer#place_cursor
 987           (source_buffer#get_iter_at_mark (`NAME "locked")) in
 988       let advance _ = (MatitaScript.current ())#advance (); cursor () in
 989       let retract _ = (MatitaScript.current ())#retract (); cursor () in
 990       let top _ = (MatitaScript.current ())#goto `Top (); cursor () in
 991       let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in
 992       let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () in
 993       let advance = locker (keep_focus advance) in
 994       let retract = locker (keep_focus retract) in
 995       let top = locker (keep_focus top) in
 996       let bottom = locker (keep_focus bottom) in
 997       let jump = locker (keep_focus jump) in
 998         (* quit *)
 999       self#setQuitCallback (fun () ->
1000         let script = MatitaScript.current () in
1001         if source_view#buffer#modified then
1002           match ask_unsaved main#toplevel with
1003           | `YES ->
1004                saveScript ();
1005                save_moo script#lexicon_status script#grafite_status;
1006                GMain.Main.quit ()
1007           | `NO -> GMain.Main.quit ()
1008           | `CANCEL -> ()
1009         else
1010           (save_moo script#lexicon_status script#grafite_status;
1011           GMain.Main.quit ()));
1012       connect_button main#scriptAdvanceButton advance;
1013       connect_button main#scriptRetractButton retract;
1014       connect_button main#scriptTopButton top;
1015       connect_button main#scriptBottomButton bottom;
1016       connect_button main#scriptJumpButton jump;
1017       connect_button main#scriptAbortButton kill_worker;
1018       connect_menu_item main#scriptAdvanceMenuItem advance;
1019       connect_menu_item main#scriptRetractMenuItem retract;
1020       connect_menu_item main#scriptTopMenuItem top;
1021       connect_menu_item main#scriptBottomMenuItem bottom;
1022       connect_menu_item main#scriptJumpMenuItem jump;
1023       connect_menu_item main#openMenuItem   loadScript;
1024       connect_menu_item main#saveMenuItem   saveScript;
1025       connect_menu_item main#saveAsMenuItem saveAsScript;
1026       connect_menu_item main#newMenuItem    newScript;
1027       connect_menu_item main#showCoercionsGraphMenuItem
1028         (fun _ ->
1029           let c = MatitaMathView.cicBrowser () in
1030           c#load (`About `Coercions));
1031       connect_menu_item main#showAutoGuiMenuItem
1032         (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
1033          (* script monospace font stuff *)
1034       self#updateFontSize ();
1035         (* debug menu *)
1036       main#debugMenu#misc#hide ();
1037         (* HBUGS *)
1038       main#hintNotebook#misc#hide ();
1039       (*
1040       main#hintLowImage#set_file (image_path "matita-bulb-low.png");
1041       main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
1042       main#hintHighImage#set_file (image_path "matita-bulb-high.png");
1043       *)
1044         (* focus *)
1045       self#sourceView#misc#grab_focus ();
1046         (* main win dimension *)
1047       let width = Gdk.Screen.width () in
1048       let height = Gdk.Screen.height () in
1049       let main_w = width * 90 / 100 in
1050       let main_h = height * 80 / 100 in
1051       let script_w = main_w * 6 / 10 in
1052       main#toplevel#resize ~width:main_w ~height:main_h;
1053       main#hpaneScriptSequent#set_position script_w;
1054         (* source_view *)
1055       ignore(source_view#connect#after#paste_clipboard
1056         ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock));
1057       (* clean_locked is set to true only "during" a PRIMARY paste
1058          operation (i.e. by clicking with the second mouse button) *)
1059       let clean_locked = ref false in
1060       ignore(source_view#event#connect#button_press
1061         ~callback:
1062           (fun button ->
1063             if GdkEvent.Button.button button = 2 then
1064              clean_locked := true;
1065             false
1066           ));
1067       ignore(source_view#event#connect#button_release
1068         ~callback:(fun button -> clean_locked := false; false));
1069       ignore(source_view#buffer#connect#after#apply_tag
1070        ~callback:(
1071          fun tag ~start:_ ~stop:_ ->
1072           if !clean_locked &&
1073              tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid
1074           then
1075            begin
1076             clean_locked := false;
1077             (MatitaScript.current ())#clean_dirty_lock;
1078             clean_locked := true
1079            end));
1080       (* math view handling *)
1081       connect_menu_item main#newCicBrowserMenuItem (fun () ->
1082         ignore (MatitaMathView.cicBrowser ()));
1083       connect_menu_item main#increaseFontSizeMenuItem (fun () ->
1084         self#increaseFontSize ();
1085         MatitaMathView.increase_font_size ();
1086         MatitaMathView.update_font_sizes ());
1087       connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
1088         self#decreaseFontSize ();
1089         MatitaMathView.decrease_font_size ();
1090         MatitaMathView.update_font_sizes ());
1091       connect_menu_item main#normalFontSizeMenuItem (fun () ->
1092         self#resetFontSize ();
1093         MatitaMathView.reset_font_size ();
1094         MatitaMathView.update_font_sizes ());
1095       MatitaMathView.reset_font_size ();
1096
1097       (** selections / clipboards handling *)
1098
1099     method markupSelected = MatitaMathView.has_selection ()
1100     method private textSelected =
1101       (source_buffer#get_iter_at_mark `INSERT)#compare
1102         (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
1103     method private somethingSelected = self#markupSelected || self#textSelected
1104     method private markupStored = MatitaMathView.has_clipboard ()
1105     method private textStored = clipboard#text <> None
1106     method private somethingStored = self#markupStored || self#textStored
1107
1108     method canCopy = self#somethingSelected
1109     method canCut = self#textSelected
1110     method canDelete = self#textSelected
1111     method canPaste = self#somethingStored
1112     method canPastePattern = self#markupStored
1113
1114     method copy () =
1115       if self#textSelected
1116       then begin
1117         MatitaMathView.empty_clipboard ();
1118         source_view#buffer#copy_clipboard clipboard;
1119       end else
1120         MatitaMathView.copy_selection ()
1121     method cut () =
1122       source_view#buffer#cut_clipboard clipboard;
1123       MatitaMathView.empty_clipboard ()
1124     method delete () = ignore (source_view#buffer#delete_selection ())
1125     method paste () =
1126       if MatitaMathView.has_clipboard ()
1127       then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term)
1128       else source_view#buffer#paste_clipboard clipboard;
1129       (MatitaScript.current ())#clean_dirty_lock
1130     method pastePattern () =
1131       source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)
1132
1133     method private nextLigature () =
1134       let iter = source_buffer#get_iter_at_mark `INSERT in
1135       let write_ligature len s =
1136         assert(Glib.Utf8.validate s);
1137         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
1138         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
1139       in
1140       let get_ligature word =
1141         let len = String.length word in
1142         let aux_tex () =
1143           try
1144             for i = len - 1 downto 0 do
1145               if HExtlib.is_alpha word.[i] then ()
1146               else
1147                 (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1))
1148             done;
1149             None
1150           with Found i ->
1151             if i = ~-1 then None else Some (String.sub word i (len - i))
1152         in
1153         let aux_ligature () =
1154           try
1155             for i = len - 1 downto 0 do
1156               if CicNotationLexer.is_ligature_char word.[i] then ()
1157               else raise (Found (i+1))
1158             done;
1159             raise (Found 0)
1160           with
1161           | Found i ->
1162               (try
1163                 Some (String.sub word i (len - i))
1164               with Invalid_argument _ -> None)
1165         in
1166         match aux_tex () with
1167         | Some macro -> macro
1168         | None -> (match aux_ligature () with Some l -> l | None -> word)
1169       in
1170       (match next_ligatures with
1171       | [] -> (* find ligatures and fill next_ligatures, then try again *)
1172           let last_word =
1173             iter#get_slice
1174               ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace)
1175           in
1176           let ligature = get_ligature last_word in
1177           (match CicNotationLexer.lookup_ligatures ligature with
1178           | [] -> ()
1179           | hd :: tl ->
1180               write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd;
1181               next_ligatures <- tl @ [ hd ])
1182       | hd :: tl ->
1183           write_ligature 1 hd;
1184           next_ligatures <- tl @ [ hd ])
1185
1186     method private externalEditor () =
1187       let cmd = Helm_registry.get "matita.external_editor" in
1188 (* ZACK uncomment to enable interactive ask of external editor command *)
1189 (*      let cmd =
1190          let msg =
1191           "External editor command:
1192 %f  will be substitute for the script name,
1193 %p  for the cursor position in bytes,
1194 %l  for the execution point in bytes."
1195         in
1196         ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false
1197           ~default:(Helm_registry.get "matita.external_editor") ()
1198       in *)
1199       let script = MatitaScript.current () in
1200       let fname = script#filename in
1201       let slice mark =
1202         source_buffer#start_iter#get_slice
1203           ~stop:(source_buffer#get_iter_at_mark mark)
1204       in
1205       let locked = `MARK script#locked_mark in
1206       let string_pos mark = string_of_int (String.length (slice mark)) in
1207       let cursor_pos = string_pos `INSERT in
1208       let locked_pos = string_pos locked in
1209       let cmd =
1210         Pcre.replace ~pat:"%f" ~templ:fname
1211           (Pcre.replace ~pat:"%p" ~templ:cursor_pos
1212             (Pcre.replace ~pat:"%l" ~templ:locked_pos
1213               cmd))
1214       in
1215       let locked_before = slice locked in
1216       let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in
1217       ignore (Unix.system cmd);
1218       source_buffer#set_text (HExtlib.input_file fname);
1219       let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in
1220       source_buffer#move_mark locked locked_iter;
1221       source_buffer#apply_tag script#locked_tag
1222         ~start:source_buffer#start_iter ~stop:locked_iter;
1223       let locked_after = slice locked in
1224       let line = ref 0 in
1225       let col = ref 0 in
1226       try
1227         for i = 0 to String.length locked_before - 1 do
1228           if locked_before.[i] <> locked_after.[i] then begin
1229             source_buffer#place_cursor
1230               ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col)));
1231             script#goto `Cursor ();
1232             raise Exit
1233           end else if locked_before.[i] = '\n' then begin
1234             incr line;
1235             col := 0
1236           end
1237         done
1238       with
1239       | Exit -> ()
1240       | Invalid_argument _ -> script#goto `Bottom ()
1241
1242     method loadScript file =
1243       let script = MatitaScript.current () in
1244       script#reset ();
1245       if Pcre.pmatch ~pat:"\\.p$" file then
1246         begin
1247           let tptppath =
1248             Helm_registry.get_opt_default Helm_registry.string ~default:"./"
1249               "matita.tptppath"
1250           in
1251           let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in
1252           let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
1253           script#assignFileName (Some filename);
1254           source_view#source_buffer#begin_not_undoable_action ();
1255           script#loadFromString data;
1256           source_view#source_buffer#end_not_undoable_action ();
1257           console#message ("'"^filename^"' loaded.");
1258           self#_enableSaveTo filename
1259         end
1260       else
1261         begin
1262           script#assignFileName (Some file);
1263           let content =
1264            if Sys.file_exists file then file
1265            else BuildTimeConf.script_template
1266           in
1267            source_view#source_buffer#begin_not_undoable_action ();
1268            script#loadFromFile content;
1269            source_view#source_buffer#end_not_undoable_action ();
1270            console#message ("'"^file^"' loaded.");
1271            self#_enableSaveTo file
1272         end
1273
1274     method setStar b =
1275       let s = MatitaScript.current () in
1276       let w = main#toplevel in
1277       let set x = w#set_title x in
1278       let name =
1279         "Matita - " ^ Filename.basename s#filename ^
1280         (if b then "*" else "") ^
1281         " in " ^ s#buri_of_current_file
1282       in
1283         set name
1284
1285     method private _enableSaveTo file =
1286       self#main#saveMenuItem#misc#set_sensitive true
1287
1288     method console = console
1289     method sourceView: GSourceView.source_view =
1290       (source_view: GSourceView.source_view)
1291     method fileSel = fileSel
1292     method findRepl = findRepl
1293     method main = main
1294     method develList = develList
1295     method newDevel = newDevel
1296
1297     method newBrowserWin () =
1298       object (self)
1299         inherit browserWin ()
1300         val combo = GEdit.combo_box_entry ()
1301         initializer
1302           self#check_widgets ();
1303           let combo_widget = combo#coerce in
1304           uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
1305           combo#entry#misc#grab_focus ()
1306         method browserUri = combo
1307       end
1308
1309     method newUriDialog () =
1310       let dialog = new uriChoiceDialog () in
1311       dialog#check_widgets ();
1312       dialog
1313
1314     method newConfirmationDialog () =
1315       let dialog = new confirmationDialog () in
1316       dialog#check_widgets ();
1317       dialog
1318
1319     method newEmptyDialog () =
1320       let dialog = new emptyDialog () in
1321       dialog#check_widgets ();
1322       dialog
1323
1324     method private addKeyBinding key callback =
1325       List.iter (fun evbox -> add_key_binding key callback evbox)
1326         keyBindingBoxes
1327
1328     method setQuitCallback callback =
1329       connect_menu_item main#quitMenuItem callback;
1330       ignore (main#toplevel#event#connect#delete
1331         (fun _ -> callback ();true));
1332       self#addKeyBinding GdkKeysyms._q callback
1333
1334     method chooseFile ?(ok_not_exists = false) () =
1335       _ok_not_exists <- ok_not_exists;
1336       _only_directory <- false;
1337       fileSel#fileSelectionWin#show ();
1338       GtkThread.main ();
1339       chosen_file
1340
1341     method private chooseDir ?(ok_not_exists = false) () =
1342       _ok_not_exists <- ok_not_exists;
1343       _only_directory <- true;
1344       fileSel#fileSelectionWin#show ();
1345       GtkThread.main ();
1346       (* we should check that this is a directory *)
1347       chosen_file
1348
1349     method createDevelopment ~containing =
1350       next_devel_must_contain <- containing;
1351       newDevel#toplevel#misc#show()
1352
1353     method askText ?(title = "") ?(msg = "") () =
1354       let dialog = new textDialog () in
1355       dialog#textDialog#set_title title;
1356       dialog#textDialogLabel#set_label msg;
1357       let text = ref None in
1358       let return v =
1359         text := v;
1360         dialog#textDialog#destroy ();
1361         GMain.Main.quit ()
1362       in
1363       ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
1364       connect_button dialog#textDialogCancelButton (fun _ -> return None);
1365       connect_button dialog#textDialogOkButton (fun _ ->
1366         let text = dialog#textDialogTextView#buffer#get_text () in
1367         return (Some text));
1368       dialog#textDialog#show ();
1369       GtkThread.main ();
1370       !text
1371
1372     method private updateFontSize () =
1373       self#sourceView#misc#modify_font_by_name
1374         (sprintf "%s %d" BuildTimeConf.script_font font_size)
1375
1376     method increaseFontSize () =
1377       font_size <- font_size + 1;
1378       self#updateFontSize ()
1379
1380     method decreaseFontSize () =
1381       font_size <- font_size - 1;
1382       self#updateFontSize ()
1383
1384     method resetFontSize () =
1385       font_size <- default_font_size;
1386       self#updateFontSize ()
1387
1388   end
1389
1390 let gui () =
1391   let g = new gui () in
1392   gui_instance := Some g;
1393   MatitaMathView.set_gui g;
1394   g
1395
1396 let instance = singleton gui
1397
1398 let non p x = not (p x)
1399
1400 (* this is a shit and should be changed :-{ *)
1401 let interactive_uri_choice
1402   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
1403   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
1404   ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
1405   ?copy_cb ()
1406   ~id uris
1407 =
1408   let gui = instance () in
1409   let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
1410   if (selection_mode <> `SINGLE) &&
1411     (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
1412   then
1413     Lazy.force nonvars_uris
1414   else begin
1415     let dialog = gui#newUriDialog () in
1416     if hide_uri_entry then
1417       dialog#uriEntryHBox#misc#hide ();
1418     if hide_try then
1419       begin
1420       dialog#uriChoiceSelectedButton#misc#hide ();
1421       dialog#uriChoiceConstantsButton#misc#hide ();
1422       end;
1423     dialog#okLabel#set_label ok_label;
1424     dialog#uriChoiceTreeView#selection#set_mode
1425       (selection_mode :> Gtk.Tags.selection_mode);
1426     let model = new stringListModel dialog#uriChoiceTreeView in
1427     let choices = ref None in
1428     (match copy_cb with
1429     | None -> ()
1430     | Some cb ->
1431         dialog#copyButton#misc#show ();
1432         connect_button dialog#copyButton
1433         (fun _ ->
1434           match model#easy_selection () with
1435           | [u] -> (cb u)
1436           | _ -> ()));
1437     dialog#uriChoiceDialog#set_title title;
1438     dialog#uriChoiceLabel#set_text msg;
1439     List.iter model#easy_append (List.map UriManager.string_of_uri uris);
1440     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
1441     let return v =
1442       choices := v;
1443       dialog#uriChoiceDialog#destroy ();
1444       GMain.Main.quit ()
1445     in
1446     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
1447     connect_button dialog#uriChoiceConstantsButton (fun _ ->
1448       return (Some (Lazy.force nonvars_uris)));
1449     if ok_action = `AUTO then
1450       connect_button dialog#uriChoiceAutoButton (fun _ ->
1451         Helm_registry.set_bool "matita.auto_disambiguation" true;
1452         return (Some (Lazy.force nonvars_uris)))
1453     else
1454       connect_button dialog#uriChoiceAutoButton (fun _ ->
1455         match model#easy_selection () with
1456         | [] -> ()
1457         | uris -> return (Some (List.map UriManager.uri_of_string uris)));
1458     connect_button dialog#uriChoiceSelectedButton (fun _ ->
1459       match model#easy_selection () with
1460       | [] -> ()
1461       | uris -> return (Some (List.map UriManager.uri_of_string uris)));
1462     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
1463     dialog#uriChoiceDialog#show ();
1464     GtkThread.main ();
1465     (match !choices with
1466     | None -> raise MatitaTypes.Cancel
1467     | Some uris -> uris)
1468   end
1469
1470 class interpModel =
1471   let cols = new GTree.column_list in
1472   let id_col = cols#add Gobject.Data.string in
1473   let dsc_col = cols#add Gobject.Data.string in
1474   let interp_no_col = cols#add Gobject.Data.int in
1475   let tree_store = GTree.tree_store cols in
1476   let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
1477   let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
1478   let id_view_col = GTree.view_column ~renderer:id_renderer () in
1479   let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
1480   fun tree_view choices ->
1481     object
1482       initializer
1483         tree_view#set_model (Some (tree_store :> GTree.model));
1484         ignore (tree_view#append_column id_view_col);
1485         ignore (tree_view#append_column dsc_view_col);
1486         let name_of_interp =
1487           (* try to find a reasonable name for an interpretation *)
1488           let idx = ref 0 in
1489           fun interp ->
1490             try
1491               List.assoc "0" interp
1492             with Not_found ->
1493               incr idx; string_of_int !idx
1494         in
1495         tree_store#clear ();
1496         let idx = ref ~-1 in
1497         List.iter
1498           (fun interp ->
1499             incr idx;
1500             let interp_row = tree_store#append () in
1501             tree_store#set ~row:interp_row ~column:id_col
1502               (name_of_interp interp);
1503             tree_store#set ~row:interp_row ~column:interp_no_col !idx;
1504             List.iter
1505               (fun (id, dsc) ->
1506                 let row = tree_store#append ~parent:interp_row () in
1507                 tree_store#set ~row ~column:id_col id;
1508                 tree_store#set ~row ~column:dsc_col dsc;
1509                 tree_store#set ~row ~column:interp_no_col !idx)
1510               interp)
1511           choices
1512
1513       method get_interp_no tree_path =
1514         let iter = tree_store#get_iter tree_path in
1515         tree_store#get ~row:iter ~column:interp_no_col
1516     end
1517
1518 let interactive_string_choice
1519   text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
1520 =
1521   let gui = instance () in
1522     let dialog = gui#newUriDialog () in
1523     dialog#uriEntryHBox#misc#hide ();
1524     dialog#uriChoiceSelectedButton#misc#hide ();
1525     dialog#uriChoiceAutoButton#misc#hide ();
1526     dialog#uriChoiceConstantsButton#misc#hide ();
1527     dialog#uriChoiceTreeView#selection#set_mode
1528       (`SINGLE :> Gtk.Tags.selection_mode);
1529     let model = new stringListModel dialog#uriChoiceTreeView in
1530     let choices = ref None in
1531     dialog#uriChoiceDialog#set_title title;
1532     let hack_len = MatitaGtkMisc.utf8_string_length text in
1533     let rec colorize acc_len = function
1534       | [] ->
1535           let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
1536           fst(MatitaGtkMisc.utf8_parsed_text text floc)
1537       | he::tl ->
1538           let start, stop =  HExtlib.loc_of_floc he in
1539           let floc1 = HExtlib.floc_of_loc (acc_len,start) in
1540           let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
1541           let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
1542           str1 ^ "<b>" ^ str2 ^ "</b>" ^ colorize stop tl
1543     in
1544 (*     List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
1545                 Printf.eprintf "(%d,%d)" start stop) locs; *)
1546     let locs =
1547       List.sort
1548         (fun loc1 loc2 ->
1549           fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2))
1550         locs
1551     in
1552 (*     prerr_endline "XXXXXXXXXXXXXXXXXXXX";
1553     List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
1554                 Printf.eprintf "(%d,%d)" start stop) locs;
1555     prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
1556     dialog#uriChoiceLabel#set_use_markup true;
1557     let txt = colorize 0 locs in
1558     let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
1559       (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
1560     in
1561     dialog#uriChoiceLabel#set_label txt;
1562     List.iter model#easy_append uris;
1563     let return v =
1564       choices := v;
1565       dialog#uriChoiceDialog#destroy ();
1566       GMain.Main.quit ()
1567     in
1568     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
1569     connect_button dialog#uriChoiceForwardButton (fun _ ->
1570       match model#easy_selection () with
1571       | [] -> ()
1572       | uris -> return (Some uris));
1573     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
1574     dialog#uriChoiceDialog#show ();
1575     GtkThread.main ();
1576     (match !choices with
1577     | None -> raise MatitaTypes.Cancel
1578     | Some uris -> uris)
1579
1580 let interactive_interp_choice () text prefix_len choices =
1581 (*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
1582  let filter_choices filter =
1583   let rec is_compatible filter =
1584    function
1585       [] -> true
1586     | ([],_,_)::tl -> is_compatible filter tl
1587     | (loc::tlloc,id,dsc)::tl ->
1588        try
1589         if List.assoc (loc,id) filter = dsc then
1590          is_compatible filter ((tlloc,id,dsc)::tl)
1591         else
1592          false
1593        with
1594         Not_found -> true
1595   in
1596    List.filter (fun (_,interp) -> is_compatible filter interp)
1597  in
1598  let rec get_choices loc id =
1599   function
1600      [] -> []
1601    | (_,he)::tl ->
1602       let _,_,dsc =
1603        List.find (fun (locs,id',_) -> id = id' && List.mem loc locs) he
1604       in
1605        dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices loc id tl))
1606  in
1607  let example_interp =
1608   match choices with
1609      [] -> assert false
1610    | he::_ -> he in
1611  let ask_user id locs choices =
1612   interactive_string_choice
1613    text prefix_len
1614    ~title:"Ambiguous input"
1615    ~msg:("Choose an interpretation for " ^ id) () ~id locs choices
1616  in
1617  let rec classify ids filter partial_interpretations =
1618   match ids with
1619      [] -> List.map fst partial_interpretations
1620    | ([],_,_)::tl -> classify tl filter partial_interpretations
1621    | (loc::tlloc,id,dsc)::tl ->
1622       let choices = get_choices loc id partial_interpretations in
1623       let chosen_dsc =
1624        match choices with
1625           [] -> prerr_endline ("NO CHOICES FOR " ^ id); assert false
1626         | [dsc] -> dsc
1627         | _ ->
1628           match ask_user id [loc] choices with
1629              [x] -> x
1630            | _ -> assert false
1631       in
1632        let filter = ((loc,id),chosen_dsc)::filter in
1633        let compatible_interps = filter_choices filter partial_interpretations in
1634         classify ((tlloc,id,dsc)::tl) filter compatible_interps
1635  in
1636  let enumerated_choices =
1637   let idx = ref ~-1 in
1638   List.map (fun interp -> incr idx; !idx,interp) choices
1639  in
1640   classify example_interp [] enumerated_choices
1641
1642 let _ =
1643   (* disambiguator callbacks *)
1644   GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
1645   GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
1646   (* gtk initialization *)
1647   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
1648   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
1649   ignore (GMain.Main.init ())
1650