helm/matita/matitaGui.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 open MatitaGeneratedGui
  29 open MatitaGtkMisc
  30 open MatitaMisc
  31
  32 let gui_instance = ref None ;;
  33
  34 class type browserWin =
  35   (* this class exists only because GEdit.combo_box_entry is not supported by
  36    * lablgladecc :-(((( *)
  37 object
  38   inherit MatitaGeneratedGui.browserWin
  39   method browserUri: GEdit.combo_box_entry
  40 end
  41
  42 class console ~(buffer: GText.buffer) () =
  43   object (self)
  44     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
  45     val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
  46     val message_tag = buffer#create_tag []
  47     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
  48     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
  49     method error s   = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
  50     method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
  51     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
  52     method clear () =
  53       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
  54     method log_callback (tag: MatitaLog.log_tag) s =
  55       match tag with
  56       | `Debug -> self#debug (s ^ "\n")
  57       | `Error -> self#error (s ^ "\n")
  58       | `Message -> self#message (s ^ "\n")
  59       | `Warning -> self#warning (s ^ "\n")
  60   end
  61
  62 class gui () =
  63     (* creation order _is_ relevant for windows placement *)
  64   let main = new mainWin () in
  65   let about = new aboutWin () in
  66   let fileSel = new fileSelectionWin () in
  67   let keyBindingBoxes = (* event boxes which should receive global key events *)
  68     [ main#mainWinEventBox ]
  69   in
  70   let console = new console ~buffer:main#logTextView#buffer () in
  71   let (source_view: GSourceView.source_view) =
  72     GSourceView.source_view
  73       ~auto_indent:true
  74       ~insert_spaces_instead_of_tabs:true ~tabs_width:2
  75       ~margin:80 ~show_margin:true
  76       ~smart_home_end:true
  77       ~packing:main#scriptScrolledWin#add
  78       ()
  79   in
  80   let default_font_size =
  81     Helm_registry.get_opt_default Helm_registry.int
  82       ~default:BuildTimeConf.default_font_size "matita.font_size"
  83   in
  84   let source_buffer = source_view#source_buffer in
  85   object (self)
  86     val mutable chosen_file = None
  87     val mutable _ok_not_exists = false
  88     val mutable script_fname = None
  89     val mutable font_size = default_font_size
  90
  91     initializer
  92         (* glade's check widgets *)
  93       List.iter (fun w -> w#check_widgets ())
  94         (let c w = (w :> <check_widgets: unit -> unit>) in
  95          [ c about; c fileSel; c main ]);
  96         (* key bindings *)
  97       List.iter (* global key bindings *)
  98         (fun (key, callback) -> self#addKeyBinding key callback)
  99 (*
 100         [ GdkKeysyms._F3,
 101             toggle_win ~check:main#showProofMenuItem proof#proofWin;
 102           GdkKeysyms._F4,
 103             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 104 *)
 105         [ ];
 106         (* about win *)
 107       ignore (about#aboutWin#event#connect#delete (fun _ -> true));
 108       ignore (main#aboutMenuItem#connect#activate (fun _ ->
 109         about#aboutWin#show ()));
 110       connect_button about#aboutDismissButton (fun _ ->
 111         about#aboutWin#misc#hide ());
 112       about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
 113         ~templ:BuildTimeConf.version about#aboutLabel#label);
 114         (* file selection win *)
 115       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
 116       ignore (fileSel#fileSelectionWin#connect#response (fun event ->
 117         let return r =
 118           chosen_file <- r;
 119           fileSel#fileSelectionWin#misc#hide ();
 120           GMain.Main.quit ()
 121         in
 122         match event with
 123         | `OK ->
 124             let fname = fileSel#fileSelectionWin#filename in
 125             if Sys.file_exists fname then
 126               (if is_regular fname then return (Some fname))
 127             else
 128               (if _ok_not_exists then return (Some fname))
 129         | `CANCEL -> return None
 130         | `HELP -> ()
 131         | `DELETE_EVENT -> return None));
 132         (* menus *)
 133       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
 134       main#helpMenu#set_right_justified true;
 135         (* console *)
 136       let adj = main#logScrolledWin#vadjustment in
 137       ignore (adj#connect#changed
 138                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
 139       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
 140         (* toolbar *)
 141       let module A = TacticAst in
 142       let hole = CicAst.UserInput in
 143       let loc = CicAst.dummy_floc in
 144       let tac ast _ =
 145         if (MatitaScript.instance ())#onGoingProof () then
 146           (MatitaScript.instance ())#advance
 147             ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
 148       in
 149       let tac_w_term ast _ =
 150         if (MatitaScript.instance ())#onGoingProof () then
 151           let buf = source_buffer in
 152           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
 153             ("\n" ^ TacticAstPp.pp_tactic ast)
 154       in
 155       let tbar = self#main in
 156       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
 157       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
 158       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
 159       connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None)));
 160       connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
 161       connect_button tbar#splitButton (tac (A.Split loc));
 162       connect_button tbar#leftButton (tac (A.Left loc));
 163       connect_button tbar#rightButton (tac (A.Right loc));
 164       connect_button tbar#existsButton (tac (A.Exists loc));
 165       connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
 166       connect_button tbar#symmetryButton (tac (A.Symmetry loc));
 167       connect_button tbar#transitivityButton
 168         (tac_w_term (A.Transitivity (loc, hole)));
 169       connect_button tbar#assumptionButton (tac (A.Assumption loc));
 170       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
 171       connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
 172       MatitaGtkMisc.toggle_widget_visibility
 173        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
 174        ~check:self#main#tacticsBarMenuItem;
 175       let module Hr = Helm_registry in
 176       if
 177         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
 178       then
 179         self#main#tacticsBarMenuItem#set_active false;
 180       MatitaGtkMisc.toggle_callback
 181         ~callback:(function
 182           | true -> self#main#toplevel#fullscreen ()
 183           | false -> self#main#toplevel#unfullscreen ())
 184         ~check:self#main#fullscreenMenuItem;
 185       self#main#fullscreenMenuItem#set_active false;
 186         (* log *)
 187       MatitaLog.set_log_callback self#console#log_callback;
 188       GtkSignal.user_handler :=
 189         (fun exn ->
 190            MatitaLog.error
 191              (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
 192         (* script *)
 193       let _ =
 194         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
 195         | None ->
 196             MatitaLog.warn (sprintf "can't load language file %s"
 197               BuildTimeConf.lang_file)
 198         | Some matita_lang ->
 199             source_buffer#set_language matita_lang;
 200             source_buffer#set_highlight true
 201       in
 202       let s () = MatitaScript.instance () in
 203       let disableSave () =
 204         script_fname <- None;
 205         self#main#saveMenuItem#misc#set_sensitive false
 206       in
 207       let loadScript () =
 208         let script = s () in
 209         match self#chooseFile () with
 210         | Some f ->
 211               script#reset ();
 212               script#assignFileName f;
 213               script#loadFromFile ();
 214               console#message ("'"^f^"' loaded.\n");
 215               self#_enableSaveTo f
 216         | None -> ()
 217       in
 218       let saveAsScript () =
 219         let script = s () in
 220         match self#chooseFile ~ok_not_exists:true () with
 221         | Some f ->
 222               script#assignFileName f;
 223               script#saveToFile ();
 224               console#message ("'"^f^"' saved.\n");
 225               self#_enableSaveTo f
 226         | None -> ()
 227       in
 228       let saveScript () =
 229         match script_fname with
 230         | None -> saveAsScript ()
 231         | Some f ->
 232               (s ())#assignFileName f;
 233               (s ())#saveToFile ();
 234               console#message ("'"^f^"' saved.\n");
 235       in
 236       let newScript () = (s ())#reset (); disableSave () in
 237       let cursor () =
 238         source_buffer#place_cursor
 239           (source_buffer#get_iter_at_mark (`NAME "locked"))
 240       in
 241       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
 242       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
 243       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
 244       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
 245       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
 246       let connect_key sym f =
 247         connect_key self#main#mainWinEventBox#event
 248           ~modifiers:[`CONTROL] ~stop:true sym f;
 249         connect_key self#sourceView#event
 250           ~modifiers:[`CONTROL] ~stop:true sym f
 251       in
 252         (* quit *)
 253       self#setQuitCallback (fun () ->
 254         if source_view#buffer#modified then
 255           begin
 256             let rc =
 257               MatitaGtkMisc.ask_confirmation
 258                 ~parent:main#toplevel
 259                 ~title:"Unsaved work!"
 260                 ~message:("Your work is <b>unsaved</b>!\n\n"^
 261                      "<i>Do you want to save the script before exiting?</i>")
 262                 ()
 263             in
 264             match rc with
 265             | `YES -> saveScript ();
 266                       if not source_view#buffer#modified then
 267                         GMain.Main.quit ()
 268             | `NO -> GMain.Main.quit ()
 269             | `CANCEL -> ()
 270           end else GMain.Main.quit ());
 271       connect_button self#main#scriptAdvanceButton advance;
 272       connect_button self#main#scriptRetractButton retract;
 273       connect_button self#main#scriptTopButton top;
 274       connect_button self#main#scriptBottomButton bottom;
 275       connect_key GdkKeysyms._Down advance;
 276       connect_key GdkKeysyms._Up retract;
 277       connect_key GdkKeysyms._Home top;
 278       connect_key GdkKeysyms._End bottom;
 279       connect_button self#main#scriptJumpButton jump;
 280       connect_menu_item self#main#openMenuItem   loadScript;
 281       connect_menu_item self#main#saveMenuItem   saveScript;
 282       connect_menu_item self#main#saveAsMenuItem saveAsScript;
 283       connect_menu_item self#main#newMenuItem    newScript;
 284       connect_key GdkKeysyms._period
 285         (fun () ->
 286           source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
 287             ".\n";
 288           advance ());
 289       connect_key GdkKeysyms._Return
 290         (fun () ->
 291           source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
 292             "\n";
 293           advance ());
 294          (* script monospace font stuff *)
 295       self#updateFontSize ();
 296         (* debug menu *)
 297       self#main#debugMenu#misc#hide ();
 298         (* status bar *)
 299       self#main#hintLowImage#set_file (image_path "matita-bulb-low.png");
 300       self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
 301       self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
 302         (* focus *)
 303       self#sourceView#misc#grab_focus ();
 304         (* main win dimension *)
 305       let width = Gdk.Screen.width () in
 306       let height = Gdk.Screen.height () in
 307       let main_w = width * 90 / 100 in
 308       let main_h = height * 80 / 100 in
 309       let script_w = main_w * 6 / 10 in
 310       self#main#toplevel#resize ~width:main_w ~height:main_h;
 311       self#main#hpaneScriptSequent#set_position script_w
 312
 313     method loadScript file =
 314       let script = MatitaScript.instance () in
 315       script#reset ();
 316       script#assignFileName file;
 317       script#loadFromFile ();
 318       console#message ("'"^file^"' loaded.");
 319       self#_enableSaveTo file
 320
 321     method setStar name b =
 322       let l = main#scriptLabel in
 323       if b then
 324         l#set_text (name ^  " *")
 325       else
 326         l#set_text (name)
 327
 328     method private _enableSaveTo file =
 329       script_fname <- Some file;
 330       self#main#saveMenuItem#misc#set_sensitive true
 331
 332
 333     method console = console
 334     method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
 335     method about = about
 336     method fileSel = fileSel
 337     method main = main
 338
 339     method newBrowserWin () =
 340       object (self)
 341         inherit browserWin ()
 342         val combo = GEdit.combo_box_entry ()
 343         initializer
 344           self#check_widgets ();
 345           let combo_widget = combo#coerce in
 346           uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
 347           combo#entry#misc#grab_focus ()
 348         method browserUri = combo
 349       end
 350
 351     method newUriDialog () =
 352       let dialog = new uriChoiceDialog () in
 353       dialog#check_widgets ();
 354       dialog
 355
 356     method newInterpDialog () =
 357       let dialog = new interpChoiceDialog () in
 358       dialog#check_widgets ();
 359       dialog
 360
 361     method newConfirmationDialog () =
 362       let dialog = new confirmationDialog () in
 363       dialog#check_widgets ();
 364       dialog
 365
 366     method newEmptyDialog () =
 367       let dialog = new emptyDialog () in
 368       dialog#check_widgets ();
 369       dialog
 370
 371     method private addKeyBinding key callback =
 372       List.iter (fun evbox -> add_key_binding key callback evbox)
 373         keyBindingBoxes
 374
 375     method setQuitCallback callback =
 376       ignore (main#quitMenuItem#connect#activate callback);
 377       ignore (main#toplevel#event#connect#delete
 378         (fun _ -> callback ();true));
 379       self#addKeyBinding GdkKeysyms._q callback
 380
 381     method chooseFile ?(ok_not_exists = false) () =
 382       _ok_not_exists <- ok_not_exists;
 383       fileSel#fileSelectionWin#show ();
 384       GtkThread.main ();
 385       chosen_file
 386
 387     method askText ?(title = "") ?(msg = "") () =
 388       let dialog = new textDialog () in
 389       dialog#textDialog#set_title title;
 390       dialog#textDialogLabel#set_label msg;
 391       let text = ref None in
 392       let return v =
 393         text := v;
 394         dialog#textDialog#destroy ();
 395         GMain.Main.quit ()
 396       in
 397       ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
 398       connect_button dialog#textDialogCancelButton (fun _ -> return None);
 399       connect_button dialog#textDialogOkButton (fun _ ->
 400         let text = dialog#textDialogTextView#buffer#get_text () in
 401         return (Some text));
 402       dialog#textDialog#show ();
 403       GtkThread.main ();
 404       !text
 405
 406     method private updateFontSize () =
 407       self#sourceView#misc#modify_font_by_name
 408         (sprintf "%s %d" BuildTimeConf.script_font font_size)
 409
 410     method increaseFontSize () =
 411       font_size <- font_size + 1;
 412       self#updateFontSize ()
 413
 414     method decreaseFontSize () =
 415       font_size <- font_size - 1;
 416       self#updateFontSize ()
 417
 418     method resetFontSize () =
 419       font_size <- default_font_size;
 420       self#updateFontSize ()
 421
 422   end
 423
 424 let gui () =
 425   let g = new gui () in
 426   gui_instance := Some g;
 427   g
 428
 429 let instance = singleton gui
 430
 431 let non p x = not (p x)
 432
 433 (* this is a shit and should be changed :-{ *)
 434 let interactive_uri_choice
 435   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
 436   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
 437   ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
 438   ?copy_cb ()
 439   ~id uris
 440 =
 441   let gui = instance () in
 442   let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
 443   if (selection_mode <> `SINGLE) &&
 444     (Helm_registry.get_bool "matita.auto_disambiguation")
 445   then
 446     Lazy.force nonvars_uris
 447   else begin
 448     let dialog = gui#newUriDialog () in
 449     if hide_uri_entry then
 450       dialog#uriEntryHBox#misc#hide ();
 451     if hide_try then
 452       begin
 453       dialog#uriChoiceSelectedButton#misc#hide ();
 454       dialog#uriChoiceConstantsButton#misc#hide ();
 455       end;
 456     dialog#okLabel#set_label ok_label;
 457     dialog#uriChoiceTreeView#selection#set_mode
 458       (selection_mode :> Gtk.Tags.selection_mode);
 459     let model = new stringListModel dialog#uriChoiceTreeView in
 460     let choices = ref None in
 461     let nonvars = ref false in
 462     (match copy_cb with
 463     | None -> ()
 464     | Some cb ->
 465         dialog#copyButton#misc#show ();
 466         connect_button dialog#copyButton
 467         (fun _ ->
 468           match model#easy_selection () with
 469           | [u] -> (cb u)
 470           | _ -> ()));
 471     dialog#uriChoiceDialog#set_title title;
 472     dialog#uriChoiceLabel#set_text msg;
 473     List.iter model#easy_append (List.map UriManager.string_of_uri uris);
 474     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
 475     let return v =
 476       choices := v;
 477       dialog#uriChoiceDialog#destroy ();
 478       GMain.Main.quit ()
 479     in
 480     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
 481     connect_button dialog#uriChoiceConstantsButton (fun _ ->
 482       return (Some (Lazy.force nonvars_uris)));
 483     if ok_action = `AUTO then
 484       connect_button dialog#uriChoiceAutoButton (fun _ ->
 485         Helm_registry.set_bool "matita.auto_disambiguation" true;
 486         return (Some (Lazy.force nonvars_uris)))
 487     else
 488       connect_button dialog#uriChoiceAutoButton (fun _ ->
 489         match model#easy_selection () with
 490         | [] -> ()
 491         | uris -> return (Some (List.map UriManager.uri_of_string uris)));
 492     connect_button dialog#uriChoiceSelectedButton (fun _ ->
 493       match model#easy_selection () with
 494       | [] -> ()
 495       | uris -> return (Some (List.map UriManager.uri_of_string uris)));
 496     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
 497     dialog#uriChoiceDialog#show ();
 498     GtkThread.main ();
 499     (match !choices with
 500     | None -> raise MatitaTypes.Cancel
 501     | Some uris -> uris)
 502   end
 503
 504 class interpModel =
 505   let cols = new GTree.column_list in
 506   let id_col = cols#add Gobject.Data.string in
 507   let dsc_col = cols#add Gobject.Data.string in
 508   let interp_no_col = cols#add Gobject.Data.int in
 509   let tree_store = GTree.tree_store cols in
 510   let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
 511   let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
 512   let id_view_col = GTree.view_column ~renderer:id_renderer () in
 513   let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
 514   fun tree_view choices ->
 515     object
 516       initializer
 517         tree_view#set_model (Some (tree_store :> GTree.model));
 518         ignore (tree_view#append_column id_view_col);
 519         ignore (tree_view#append_column dsc_view_col);
 520         let name_of_interp =
 521           (* try to find a reasonable name for an interpretation *)
 522           let idx = ref 0 in
 523           fun interp ->
 524             try
 525               List.assoc "0" interp
 526             with Not_found ->
 527               incr idx; string_of_int !idx
 528         in
 529         tree_store#clear ();
 530         let idx = ref ~-1 in
 531         List.iter
 532           (fun interp ->
 533             incr idx;
 534             let interp_row = tree_store#append () in
 535             tree_store#set ~row:interp_row ~column:id_col
 536               (name_of_interp interp);
 537             tree_store#set ~row:interp_row ~column:interp_no_col !idx;
 538             List.iter
 539               (fun (id, dsc) ->
 540                 let row = tree_store#append ~parent:interp_row () in
 541                 tree_store#set ~row ~column:id_col id;
 542                 tree_store#set ~row ~column:dsc_col dsc;
 543                 tree_store#set ~row ~column:interp_no_col !idx)
 544               interp)
 545           choices
 546
 547       method get_interp_no tree_path =
 548         let iter = tree_store#get_iter tree_path in
 549         tree_store#get ~row:iter ~column:interp_no_col
 550     end
 551
 552 let interactive_interp_choice () choices =
 553   let gui = instance () in
 554   assert (choices <> []);
 555   let dialog = gui#newInterpDialog () in
 556   let model = new interpModel dialog#interpChoiceTreeView choices in
 557   let interp_len = List.length (List.hd choices) in
 558   dialog#interpChoiceDialog#set_title "Interpretation choice";
 559   dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
 560   let interp_no = ref None in
 561   let return _ =
 562     dialog#interpChoiceDialog#destroy ();
 563     GMain.Main.quit ()
 564   in
 565   let fail _ = interp_no := None; return () in
 566   ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
 567   connect_button dialog#interpChoiceOkButton (fun _ ->
 568     match !interp_no with None -> () | Some _ -> return ());
 569   connect_button dialog#interpChoiceCancelButton fail;
 570   ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
 571     interp_no := Some (model#get_interp_no path);
 572     return ()));
 573   let selection = dialog#interpChoiceTreeView#selection in
 574   ignore (selection#connect#changed (fun _ ->
 575     match selection#get_selected_rows with
 576     | [path] ->
 577         MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
 578         interp_no := Some (model#get_interp_no path)
 579     | _ -> assert false));
 580   dialog#interpChoiceDialog#show ();
 581   GtkThread.main ();
 582   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
 583