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