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 let clean_current_baseuri status =
  63     try
  64       let baseuri = MatitaTypes.get_string_option status "baseuri" in
  65       MatitacleanLib.clean_baseuris [baseuri]
  66     with MatitaTypes.Option_error _ -> ()
  67
  68 let ask_and_save_moo_if_needed parent fname status =
  69   let save () =
  70     MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
  71   in
  72   if (MatitaScript.instance ())#eos then
  73     begin
  74       let mooname =
  75         MatitaMisc.obj_file_of_script fname
  76       in
  77       let rc =
  78         MatitaGtkMisc.ask_confirmation
  79         ~title:"A .moo can be generated"
  80         ~message:(Printf.sprintf
  81           "%s can be generated for %s.\n<i>Should I generate it?</i>"
  82           mooname fname)
  83         ~parent ()
  84       in
  85       let b =
  86         match rc with
  87         | `YES -> true
  88         | `NO -> false
  89         | `CANCEL -> raise MatitaTypes.Cancel
  90       in
  91       if b then
  92         save ()
  93       else
  94         clean_current_baseuri status
  95     end
  96   else
  97     clean_current_baseuri status
  98
  99 let ask_unsaved parent =
 100   MatitaGtkMisc.ask_confirmation
 101     ~parent ~title:"Unsaved work!"
 102     ~message:("Your work is <b>unsaved</b>!\n\n"^
 103          "<i>Do you want to save the script before exiting?</i>")
 104     ()
 105
 106 class gui () =
 107     (* creation order _is_ relevant for windows placement *)
 108   let main = new mainWin () in
 109   let about = new aboutWin () in
 110   let fileSel = new fileSelectionWin () in
 111   let keyBindingBoxes = (* event boxes which should receive global key events *)
 112     [ main#mainWinEventBox ]
 113   in
 114   let console = new console ~buffer:main#logTextView#buffer () in
 115   let (source_view: GSourceView.source_view) =
 116     GSourceView.source_view
 117       ~auto_indent:true
 118       ~insert_spaces_instead_of_tabs:true ~tabs_width:2
 119       ~margin:80 ~show_margin:true
 120       ~smart_home_end:true
 121       ~packing:main#scriptScrolledWin#add
 122       ()
 123   in
 124   let default_font_size =
 125     Helm_registry.get_opt_default Helm_registry.int
 126       ~default:BuildTimeConf.default_font_size "matita.font_size"
 127   in
 128   let source_buffer = source_view#source_buffer in
 129   object (self)
 130     val mutable chosen_file = None
 131     val mutable _ok_not_exists = false
 132     val mutable script_fname = None
 133     val mutable font_size = default_font_size
 134
 135     initializer
 136         (* glade's check widgets *)
 137       List.iter (fun w -> w#check_widgets ())
 138         (let c w = (w :> <check_widgets: unit -> unit>) in
 139          [ c about; c fileSel; c main ]);
 140         (* key bindings *)
 141       List.iter (* global key bindings *)
 142         (fun (key, callback) -> self#addKeyBinding key callback)
 143 (*
 144         [ GdkKeysyms._F3,
 145             toggle_win ~check:main#showProofMenuItem proof#proofWin;
 146           GdkKeysyms._F4,
 147             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 148 *)
 149         [ ];
 150         (* about win *)
 151       ignore (about#aboutWin#event#connect#delete (fun _ -> true));
 152       ignore (main#aboutMenuItem#connect#activate (fun _ ->
 153         about#aboutWin#show ()));
 154       connect_button about#aboutDismissButton (fun _ ->
 155         about#aboutWin#misc#hide ());
 156       about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
 157         ~templ:BuildTimeConf.version about#aboutLabel#label);
 158         (* file selection win *)
 159       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
 160       ignore (fileSel#fileSelectionWin#connect#response (fun event ->
 161         let return r =
 162           chosen_file <- r;
 163           fileSel#fileSelectionWin#misc#hide ();
 164           GMain.Main.quit ()
 165         in
 166         match event with
 167         | `OK ->
 168             let fname = fileSel#fileSelectionWin#filename in
 169             if Sys.file_exists fname then
 170               (if is_regular fname then return (Some fname))
 171             else
 172               (if _ok_not_exists then return (Some fname))
 173         | `CANCEL -> return None
 174         | `HELP -> ()
 175         | `DELETE_EVENT -> return None));
 176         (* menus *)
 177       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
 178       main#helpMenu#set_right_justified true;
 179         (* console *)
 180       let adj = main#logScrolledWin#vadjustment in
 181       ignore (adj#connect#changed
 182                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
 183       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
 184         (* toolbar *)
 185       let module A = TacticAst in
 186       let hole = CicAst.UserInput in
 187       let loc = CicAst.dummy_floc in
 188       let tac ast _ =
 189         if (MatitaScript.instance ())#onGoingProof () then
 190           (MatitaScript.instance ())#advance
 191             ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
 192       in
 193       let tac_w_term ast _ =
 194         if (MatitaScript.instance ())#onGoingProof () then
 195           let buf = source_buffer in
 196           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
 197             ("\n" ^ TacticAstPp.pp_tactic ast)
 198       in
 199       let tbar = self#main in
 200       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
 201       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
 202       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
 203       connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, [])));
 204       connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
 205       connect_button tbar#splitButton (tac (A.Split loc));
 206       connect_button tbar#leftButton (tac (A.Left loc));
 207       connect_button tbar#rightButton (tac (A.Right loc));
 208       connect_button tbar#existsButton (tac (A.Exists loc));
 209       connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
 210       connect_button tbar#symmetryButton (tac (A.Symmetry loc));
 211       connect_button tbar#transitivityButton
 212         (tac_w_term (A.Transitivity (loc, hole)));
 213       connect_button tbar#assumptionButton (tac (A.Assumption loc));
 214       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
 215       connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
 216       MatitaGtkMisc.toggle_widget_visibility
 217        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
 218        ~check:self#main#tacticsBarMenuItem;
 219       let module Hr = Helm_registry in
 220       if
 221         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
 222       then
 223         self#main#tacticsBarMenuItem#set_active false;
 224       MatitaGtkMisc.toggle_callback
 225         ~callback:(function
 226           | true -> self#main#toplevel#fullscreen ()
 227           | false -> self#main#toplevel#unfullscreen ())
 228         ~check:self#main#fullscreenMenuItem;
 229       self#main#fullscreenMenuItem#set_active false;
 230         (* log *)
 231       MatitaLog.set_log_callback self#console#log_callback;
 232       GtkSignal.user_handler :=
 233         (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
 234         (* script *)
 235       let _ =
 236         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
 237         | None ->
 238             MatitaLog.warn (sprintf "can't load language file %s"
 239               BuildTimeConf.lang_file)
 240         | Some matita_lang ->
 241             source_buffer#set_language matita_lang;
 242             source_buffer#set_highlight true
 243       in
 244       let s () = MatitaScript.instance () in
 245       let disableSave () =
 246         script_fname <- None;
 247         self#main#saveMenuItem#misc#set_sensitive false
 248       in
 249       let saveAsScript () =
 250         let script = s () in
 251         match self#chooseFile ~ok_not_exists:true () with
 252         | Some f ->
 253               script#assignFileName f;
 254               script#saveToFile ();
 255               console#message ("'"^f^"' saved.\n");
 256               self#_enableSaveTo f
 257         | None -> ()
 258       in
 259       let saveScript () =
 260         match script_fname with
 261         | None -> saveAsScript ()
 262         | Some f ->
 263               (s ())#assignFileName f;
 264               (s ())#saveToFile ();
 265               console#message ("'"^f^"' saved.\n");
 266       in
 267       let loadScript () =
 268         let script = s () in
 269         let status = script#status in
 270         try
 271           if source_view#buffer#modified then
 272             begin
 273               match ask_unsaved main#toplevel with
 274               | `YES -> saveScript ()
 275               | `NO -> ()
 276               | `CANCEL -> raise MatitaTypes.Cancel
 277             end;
 278           (match script_fname with
 279           | None -> ()
 280           | Some fname ->
 281               ask_and_save_moo_if_needed main#toplevel fname status);
 282           match self#chooseFile () with
 283           | Some f ->
 284                 script#reset ();
 285                 script#assignFileName f;
 286                 script#loadFromFile ();
 287                 console#message ("'"^f^"' loaded.\n");
 288                 self#_enableSaveTo f
 289           | None -> ()
 290         with MatitaTypes.Cancel -> ()
 291       in
 292       let newScript () =
 293         (s ())#reset ();
 294         (s ())#template ();
 295         disableSave ();
 296         script_fname <- None
 297       in
 298       let cursor () =
 299         source_buffer#place_cursor
 300           (source_buffer#get_iter_at_mark (`NAME "locked"))
 301       in
 302       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
 303       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
 304       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
 305       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
 306       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
 307       let connect_key sym f =
 308         connect_key self#main#mainWinEventBox#event
 309           ~modifiers:[`CONTROL] ~stop:true sym f;
 310         connect_key self#sourceView#event
 311           ~modifiers:[`CONTROL] ~stop:true sym f
 312       in
 313         (* quit *)
 314       self#setQuitCallback (fun () ->
 315         let status = (MatitaScript.instance ())#status in
 316         if source_view#buffer#modified then
 317           begin
 318             let rc = ask_unsaved main#toplevel in
 319             try
 320               match rc with
 321               | `YES -> saveScript ();
 322                         if not source_view#buffer#modified then
 323                           begin
 324                             (match script_fname with
 325                             | None -> ()
 326                             | Some fname ->
 327                                ask_and_save_moo_if_needed
 328                                  main#toplevel fname status);
 329                           GMain.Main.quit ()
 330                           end
 331               | `NO -> GMain.Main.quit ()
 332               | `CANCEL -> raise MatitaTypes.Cancel
 333             with MatitaTypes.Cancel -> ()
 334           end
 335         else
 336           begin
 337             (match script_fname with
 338             | None -> clean_current_baseuri status; GMain.Main.quit ()
 339             | Some fname ->
 340                 try
 341                   ask_and_save_moo_if_needed main#toplevel fname status;
 342                   GMain.Main.quit ()
 343                 with MatitaTypes.Cancel -> ())
 344           end);
 345       connect_button self#main#scriptAdvanceButton advance;
 346       connect_button self#main#scriptRetractButton retract;
 347       connect_button self#main#scriptTopButton top;
 348       connect_button self#main#scriptBottomButton bottom;
 349       connect_key GdkKeysyms._Down advance;
 350       connect_key GdkKeysyms._Up retract;
 351       connect_key GdkKeysyms._Home top;
 352       connect_key GdkKeysyms._End bottom;
 353       connect_button self#main#scriptJumpButton jump;
 354       connect_menu_item self#main#openMenuItem   loadScript;
 355       connect_menu_item self#main#saveMenuItem   saveScript;
 356       connect_menu_item self#main#saveAsMenuItem saveAsScript;
 357       connect_menu_item self#main#newMenuItem    newScript;
 358       connect_key GdkKeysyms._period
 359         (fun () ->
 360           source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
 361             ".\n";
 362           advance ());
 363       connect_key GdkKeysyms._Return
 364         (fun () ->
 365           source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
 366             "\n";
 367           advance ());
 368          (* script monospace font stuff *)
 369       self#updateFontSize ();
 370         (* debug menu *)
 371       self#main#debugMenu#misc#hide ();
 372         (* status bar *)
 373       self#main#hintLowImage#set_file (image_path "matita-bulb-low.png");
 374       self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
 375       self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
 376         (* focus *)
 377       self#sourceView#misc#grab_focus ();
 378         (* main win dimension *)
 379       let width = Gdk.Screen.width () in
 380       let height = Gdk.Screen.height () in
 381       let main_w = width * 90 / 100 in
 382       let main_h = height * 80 / 100 in
 383       let script_w = main_w * 6 / 10 in
 384       self#main#toplevel#resize ~width:main_w ~height:main_h;
 385       self#main#hpaneScriptSequent#set_position script_w
 386
 387     method loadScript file =
 388       let script = MatitaScript.instance () in
 389       script#reset ();
 390       script#assignFileName file;
 391       script#loadFromFile ();
 392       console#message ("'"^file^"' loaded.");
 393       self#_enableSaveTo file
 394
 395     method setStar name b =
 396       let l = main#scriptLabel in
 397       if b then
 398         l#set_text (name ^  " *")
 399       else
 400         l#set_text (name)
 401
 402     method private _enableSaveTo file =
 403       script_fname <- Some file;
 404       self#main#saveMenuItem#misc#set_sensitive true
 405
 406
 407     method console = console
 408     method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
 409     method about = about
 410     method fileSel = fileSel
 411     method main = main
 412
 413     method newBrowserWin () =
 414       object (self)
 415         inherit browserWin ()
 416         val combo = GEdit.combo_box_entry ()
 417         initializer
 418           self#check_widgets ();
 419           let combo_widget = combo#coerce in
 420           uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
 421           combo#entry#misc#grab_focus ()
 422         method browserUri = combo
 423       end
 424
 425     method newUriDialog () =
 426       let dialog = new uriChoiceDialog () in
 427       dialog#check_widgets ();
 428       dialog
 429
 430     method newInterpDialog () =
 431       let dialog = new interpChoiceDialog () in
 432       dialog#check_widgets ();
 433       dialog
 434
 435     method newConfirmationDialog () =
 436       let dialog = new confirmationDialog () in
 437       dialog#check_widgets ();
 438       dialog
 439
 440     method newEmptyDialog () =
 441       let dialog = new emptyDialog () in
 442       dialog#check_widgets ();
 443       dialog
 444
 445     method private addKeyBinding key callback =
 446       List.iter (fun evbox -> add_key_binding key callback evbox)
 447         keyBindingBoxes
 448
 449     method setQuitCallback callback =
 450       ignore (main#quitMenuItem#connect#activate callback);
 451       ignore (main#toplevel#event#connect#delete
 452         (fun _ -> callback ();true));
 453       self#addKeyBinding GdkKeysyms._q callback
 454
 455     method chooseFile ?(ok_not_exists = false) () =
 456       _ok_not_exists <- ok_not_exists;
 457       fileSel#fileSelectionWin#show ();
 458       GtkThread.main ();
 459       chosen_file
 460
 461     method askText ?(title = "") ?(msg = "") () =
 462       let dialog = new textDialog () in
 463       dialog#textDialog#set_title title;
 464       dialog#textDialogLabel#set_label msg;
 465       let text = ref None in
 466       let return v =
 467         text := v;
 468         dialog#textDialog#destroy ();
 469         GMain.Main.quit ()
 470       in
 471       ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
 472       connect_button dialog#textDialogCancelButton (fun _ -> return None);
 473       connect_button dialog#textDialogOkButton (fun _ ->
 474         let text = dialog#textDialogTextView#buffer#get_text () in
 475         return (Some text));
 476       dialog#textDialog#show ();
 477       GtkThread.main ();
 478       !text
 479
 480     method private updateFontSize () =
 481       self#sourceView#misc#modify_font_by_name
 482         (sprintf "%s %d" BuildTimeConf.script_font font_size)
 483
 484     method increaseFontSize () =
 485       font_size <- font_size + 1;
 486       self#updateFontSize ()
 487
 488     method decreaseFontSize () =
 489       font_size <- font_size - 1;
 490       self#updateFontSize ()
 491
 492     method resetFontSize () =
 493       font_size <- default_font_size;
 494       self#updateFontSize ()
 495
 496   end
 497
 498 let gui () =
 499   let g = new gui () in
 500   gui_instance := Some g;
 501   g
 502
 503 let instance = singleton gui
 504
 505 let non p x = not (p x)
 506
 507 (* this is a shit and should be changed :-{ *)
 508 let interactive_uri_choice
 509   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
 510   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
 511   ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
 512   ?copy_cb ()
 513   ~id uris
 514 =
 515   let gui = instance () in
 516   let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
 517   if (selection_mode <> `SINGLE) &&
 518     (Helm_registry.get_bool "matita.auto_disambiguation")
 519   then
 520     Lazy.force nonvars_uris
 521   else begin
 522     let dialog = gui#newUriDialog () in
 523     if hide_uri_entry then
 524       dialog#uriEntryHBox#misc#hide ();
 525     if hide_try then
 526       begin
 527       dialog#uriChoiceSelectedButton#misc#hide ();
 528       dialog#uriChoiceConstantsButton#misc#hide ();
 529       end;
 530     dialog#okLabel#set_label ok_label;
 531     dialog#uriChoiceTreeView#selection#set_mode
 532       (selection_mode :> Gtk.Tags.selection_mode);
 533     let model = new stringListModel dialog#uriChoiceTreeView in
 534     let choices = ref None in
 535     let nonvars = ref false in
 536     (match copy_cb with
 537     | None -> ()
 538     | Some cb ->
 539         dialog#copyButton#misc#show ();
 540         connect_button dialog#copyButton
 541         (fun _ ->
 542           match model#easy_selection () with
 543           | [u] -> (cb u)
 544           | _ -> ()));
 545     dialog#uriChoiceDialog#set_title title;
 546     dialog#uriChoiceLabel#set_text msg;
 547     List.iter model#easy_append (List.map UriManager.string_of_uri uris);
 548     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
 549     let return v =
 550       choices := v;
 551       dialog#uriChoiceDialog#destroy ();
 552       GMain.Main.quit ()
 553     in
 554     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
 555     connect_button dialog#uriChoiceConstantsButton (fun _ ->
 556       return (Some (Lazy.force nonvars_uris)));
 557     if ok_action = `AUTO then
 558       connect_button dialog#uriChoiceAutoButton (fun _ ->
 559         Helm_registry.set_bool "matita.auto_disambiguation" true;
 560         return (Some (Lazy.force nonvars_uris)))
 561     else
 562       connect_button dialog#uriChoiceAutoButton (fun _ ->
 563         match model#easy_selection () with
 564         | [] -> ()
 565         | uris -> return (Some (List.map UriManager.uri_of_string uris)));
 566     connect_button dialog#uriChoiceSelectedButton (fun _ ->
 567       match model#easy_selection () with
 568       | [] -> ()
 569       | uris -> return (Some (List.map UriManager.uri_of_string uris)));
 570     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
 571     dialog#uriChoiceDialog#show ();
 572     GtkThread.main ();
 573     (match !choices with
 574     | None -> raise MatitaTypes.Cancel
 575     | Some uris -> uris)
 576   end
 577
 578 class interpModel =
 579   let cols = new GTree.column_list in
 580   let id_col = cols#add Gobject.Data.string in
 581   let dsc_col = cols#add Gobject.Data.string in
 582   let interp_no_col = cols#add Gobject.Data.int in
 583   let tree_store = GTree.tree_store cols in
 584   let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
 585   let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
 586   let id_view_col = GTree.view_column ~renderer:id_renderer () in
 587   let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
 588   fun tree_view choices ->
 589     object
 590       initializer
 591         tree_view#set_model (Some (tree_store :> GTree.model));
 592         ignore (tree_view#append_column id_view_col);
 593         ignore (tree_view#append_column dsc_view_col);
 594         let name_of_interp =
 595           (* try to find a reasonable name for an interpretation *)
 596           let idx = ref 0 in
 597           fun interp ->
 598             try
 599               List.assoc "0" interp
 600             with Not_found ->
 601               incr idx; string_of_int !idx
 602         in
 603         tree_store#clear ();
 604         let idx = ref ~-1 in
 605         List.iter
 606           (fun interp ->
 607             incr idx;
 608             let interp_row = tree_store#append () in
 609             tree_store#set ~row:interp_row ~column:id_col
 610               (name_of_interp interp);
 611             tree_store#set ~row:interp_row ~column:interp_no_col !idx;
 612             List.iter
 613               (fun (id, dsc) ->
 614                 let row = tree_store#append ~parent:interp_row () in
 615                 tree_store#set ~row ~column:id_col id;
 616                 tree_store#set ~row ~column:dsc_col dsc;
 617                 tree_store#set ~row ~column:interp_no_col !idx)
 618               interp)
 619           choices
 620
 621       method get_interp_no tree_path =
 622         let iter = tree_store#get_iter tree_path in
 623         tree_store#get ~row:iter ~column:interp_no_col
 624     end
 625
 626 let interactive_interp_choice () choices =
 627   let gui = instance () in
 628   assert (choices <> []);
 629   let dialog = gui#newInterpDialog () in
 630   let model = new interpModel dialog#interpChoiceTreeView choices in
 631   let interp_len = List.length (List.hd choices) in
 632   dialog#interpChoiceDialog#set_title "Interpretation choice";
 633   dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
 634   let interp_no = ref None in
 635   let return _ =
 636     dialog#interpChoiceDialog#destroy ();
 637     GMain.Main.quit ()
 638   in
 639   let fail _ = interp_no := None; return () in
 640   ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
 641   connect_button dialog#interpChoiceOkButton (fun _ ->
 642     match !interp_no with None -> () | Some _ -> return ());
 643   connect_button dialog#interpChoiceCancelButton fail;
 644   ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
 645     interp_no := Some (model#get_interp_no path);
 646     return ()));
 647   let selection = dialog#interpChoiceTreeView#selection in
 648   ignore (selection#connect#changed (fun _ ->
 649     match selection#get_selected_rows with
 650     | [path] ->
 651         MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
 652         interp_no := Some (model#get_interp_no path)
 653     | _ -> assert false));
 654   dialog#interpChoiceDialog#show ();
 655   GtkThread.main ();
 656   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
 657