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