X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=94e3e751db0f046b2f27cf01f36ca761b8fb202e;hb=a4ba77d9df157e443e6fb39dc7376996faea9973;hp=5217abeb252588fd91f9491803a50d039902df91;hpb=f3d0ba1e75bc3383d766f3a33a19352db19854df;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 5217abeb2..94e3e751d 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -35,15 +35,74 @@ exception Found of int
 
 let all_disambiguation_passes = ref false
 
-let gui_instance = ref None
+(* this is a shit and should be changed :-{ *)
+let interactive_uri_choice
+  ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
+  ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
+  ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) 
+  ?copy_cb ()
+  ~id uris
+=
+  if (selection_mode <> `SINGLE) &&
+    (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
+  then
+    uris
+  else begin
+    let dialog = new uriChoiceDialog () in
+    if hide_uri_entry then
+      dialog#uriEntryHBox#misc#hide ();
+    if hide_try then
+      begin
+      dialog#uriChoiceSelectedButton#misc#hide ();
+      dialog#uriChoiceConstantsButton#misc#hide ();
+      end;
+    dialog#okLabel#set_label ok_label;  
+    dialog#uriChoiceTreeView#selection#set_mode
+      (selection_mode :> Gtk.Tags.selection_mode);
+    let model = new stringListModel dialog#uriChoiceTreeView in
+    let choices = ref None in
+    (match copy_cb with
+    | None -> ()
+    | Some cb ->
+        dialog#copyButton#misc#show ();
+        connect_button dialog#copyButton 
+        (fun _ ->
+          match model#easy_selection () with
+          | [u] -> (cb u)
+          | _ -> ()));
+    dialog#uriChoiceDialog#set_title title;
+    dialog#uriChoiceLabel#set_text msg;
+    List.iter model#easy_append (List.map NReference.string_of_reference uris);
+    dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+    let return v =
+      choices := v;
+      dialog#uriChoiceDialog#destroy ();
+      GMain.Main.quit ()
+    in
+    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+    connect_button dialog#uriChoiceConstantsButton (fun _ ->
+      return (Some uris));
+    if ok_action = `AUTO then
+      connect_button dialog#uriChoiceAutoButton (fun _ ->
+        Helm_registry.set_bool "matita.auto_disambiguation" true;
+        return (Some uris))
+    else
+      connect_button dialog#uriChoiceAutoButton (fun _ ->
+        match model#easy_selection () with
+        | [] -> ()
+        | uris -> return (Some (List.map NReference.reference_of_string uris)));
+    connect_button dialog#uriChoiceSelectedButton (fun _ ->
+      match model#easy_selection () with
+      | [] -> ()
+      | uris -> return (Some (List.map NReference.reference_of_string uris)));
+    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+    dialog#uriChoiceDialog#show ();
+    GtkThread.main ();
+    (match !choices with 
+    | None -> raise MatitaTypes.Cancel
+    | Some uris -> uris)
+  end
 
-class type browserWin =
-  (* this class exists only because GEdit.combo_box_entry is not supported by
-   * lablgladecc :-(((( *)
-object
-  inherit MatitaGeneratedGui.browserWin
-  method browserUri: GEdit.entry
-end
 
 class console ~(buffer: GText.buffer) () =
   object (self)
@@ -66,24 +125,28 @@ class console ~(buffer: GText.buffer) () =
       | `Warning -> self#warning (s ^ "\n")
   end
         
-let clean_current_baseuri grafite_status = 
-  LibraryClean.clean_baseuris [grafite_status#baseuri]
+let clean_current_baseuri status = 
+  LibraryClean.clean_baseuris [status#baseuri]
 
-let save_moo grafite_status = 
-  let script = MatitaScript.current () in
-  let baseuri = grafite_status#baseuri in
+let save_moo0 ~do_clean script status = 
+  let baseuri = status#baseuri in
   match script#bos, script#eos with
   | true, _ -> ()
   | _, true ->
      GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-      grafite_status
-  | _ -> clean_current_baseuri grafite_status 
+      status
+  | _ -> if do_clean then clean_current_baseuri status 
+;;
+
+let save_moo status = 
+ let script = MatitaScript.current () in
+  save_moo0 ~do_clean:true script status
 ;;
     
-let ask_unsaved parent =
+let ask_unsaved parent filename =
   MatitaGtkMisc.ask_confirmation 
     ~parent ~title:"Unsaved work!" 
-    ~message:("Your work is <b>unsaved</b>!\n\n"^
+    ~message:("Script <b>" ^ filename ^ "</b> is modified.!\n\n"^
          "<i>Do you want to save the script before continuing?</i>")
     ()
 
@@ -256,7 +319,6 @@ let interactive_error_interp ~all_passes
             (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
-       dialog#check_widgets ();
        if all_passes then
         dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
        let model = new interpErrorModel dialog#treeview choices in
@@ -345,34 +407,36 @@ let interactive_error_interp ~all_passes
 class gui () =
     (* creation order _is_ relevant for windows placement *)
   let main = new mainWin () in
+  let sequents_viewer =
+   MatitaMathView.sequentsViewer_instance main#sequentsNotebook in
   let fileSel = new fileSelectionWin () in
   let findRepl = new findReplWin () in
   let keyBindingBoxes = (* event boxes which should receive global key events *)
     [ main#mainWinEventBox ]
   in
   let console = new console ~buffer:main#logTextView#buffer () in
-  let source_view () = (MatitaScript.current ())#source_view in
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
     val mutable _only_directory = false
+    val mutable current_page = -1
       
     initializer
       let s () = MatitaScript.current () in
-        (* glade's check widgets *)
-      List.iter (fun w -> w#check_widgets ())
-        (let c w = (w :> <check_widgets: unit -> unit>) in
-        [ c fileSel; c main; c findRepl]);
         (* key bindings *)
       List.iter (* global key bindings *)
-        (fun (key, callback) -> self#addKeyBinding key callback)
+        (fun (key, modifiers, callback) -> 
+                self#addKeyBinding key ~modifiers callback)
 (*
         [ GdkKeysyms._F3,
             toggle_win ~check:main#showProofMenuItem proof#proofWin;
           GdkKeysyms._F4,
             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 *)
-        [ ];
+        [ 
+          GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page;
+          GdkKeysyms._Page_Up,   [`CONTROL], main#scriptNotebook#previous_page
+        ];
         (* about win *)
       let parse_txt_file file =
        let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
@@ -420,7 +484,7 @@ class gui () =
       in
       let hide_find_Repl () = findRepl#toplevel#misc#hide () in
       let find_forward _ = 
-          let source_view = source_view () in
+          let source_view = (s ())#source_view in
           let highlight start end_ =
             source_view#source_buffer#move_mark `INSERT ~where:start;
             source_view#source_buffer#move_mark `SEL_BOUND ~where:end_;
@@ -436,7 +500,7 @@ class gui () =
           | Some (start,end_) -> highlight start end_ 
       in
       let replace _ =
-        let source_view = source_view () in
+        let source_view = (s ())#source_view in
         let text = findRepl#replaceEntry#text in
         let ins = source_view#source_buffer#get_iter `INSERT in
         let sel = source_view#source_buffer#get_iter `SEL_BOUND in
@@ -485,7 +549,7 @@ class gui () =
       connect_menu_item main#pastePatternMenuItem
          (fun () -> (MatitaScript.current ())#pastePattern ());
       connect_menu_item main#selectAllMenuItem (fun () ->
-       let source_view = source_view () in
+       let source_view = (s ())#source_view in
         source_view#source_buffer#move_mark `INSERT source_view#source_buffer#start_iter;
         source_view#source_buffer#move_mark `SEL_BOUND source_view#source_buffer#end_iter);
       connect_menu_item main#findReplMenuItem show_find_Repl;
@@ -495,13 +559,13 @@ class gui () =
       ignore (findRepl#findEntry#connect#activate find_forward);
         (* interface lockers *)
       let lock_world _ =
-       let source_view = source_view () in
+       let source_view = (s ())#source_view in
         main#buttonsToolbar#misc#set_sensitive false;
         main#scriptMenu#misc#set_sensitive false;
         source_view#set_editable false
       in
       let unlock_world _ =
-       let source_view = source_view () in
+       let source_view = (s ())#source_view in
         main#buttonsToolbar#misc#set_sensitive true;
         main#scriptMenu#misc#set_sensitive true;
         source_view#set_editable true;
@@ -534,7 +598,7 @@ class gui () =
                match !id with
                | None -> assert false (* a race condition occurred *)
                | Some id ->
-                   (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id));
+                   source_view#source_buffer#misc#disconnect id));
              source_view#source_buffer#place_cursor
               (source_view#source_buffer#get_iter (`OFFSET x'));
         end;
@@ -643,48 +707,48 @@ class gui () =
           else main#tacticsButtonsHandlebox#misc#hide ())
         ~check:main#menuitemPalette;
       connect_button main#butImpl_intro
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (⇒#i […] (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⇒#i […] (…));\n");
       connect_button main#butAnd_intro
-        (fun () -> (source_view ())#source_buffer#insert 
+        (fun () -> (s ())#source_view#source_buffer#insert 
           "apply rule (∧#i (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butOr_intro_left
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#i_l (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∨#i_l (…));\n");
       connect_button main#butOr_intro_right
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#i_r (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∨#i_r (…));\n");
       connect_button main#butNot_intro
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (¬#i […] (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (¬#i […] (…));\n");
       connect_button main#butTop_intro
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (⊤#i);\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⊤#i);\n");
       connect_button main#butImpl_elim
-        (fun () -> (source_view ())#source_buffer#insert 
+        (fun () -> (s ())#source_view#source_buffer#insert 
           "apply rule (⇒#e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butAnd_elim_left
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#e_l (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∧#e_l (…));\n");
       connect_button main#butAnd_elim_right
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#e_r (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∧#e_r (…));\n");
       connect_button main#butOr_elim
-        (fun () -> (source_view ())#source_buffer#insert 
+        (fun () -> (s ())#source_view#source_buffer#insert 
           "apply rule (∨#e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
       connect_button main#butNot_elim
-        (fun () -> (source_view ())#source_buffer#insert 
+        (fun () -> (s ())#source_view#source_buffer#insert 
           "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butBot_elim
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (⊥#e (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⊥#e (…));\n");
       connect_button main#butRAA
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (RAA […] (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (RAA […] (…));\n");
       connect_button main#butUseLemma
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (lem #premises name …);\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (lem #premises name …);\n");
       connect_button main#butDischarge
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (discharge […]);\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (discharge […]);\n");
       
       connect_button main#butForall_intro
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∀#i {…} (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∀#i {…} (…));\n");
       connect_button main#butForall_elim
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∀#e {…} (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∀#e {…} (…));\n");
       connect_button main#butExists_intro
-        (fun () -> (source_view ())#source_buffer#insert "apply rule (∃#i {…} (…));\n");
+        (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∃#i {…} (…));\n");
       connect_button main#butExists_elim
-        (fun () -> (source_view ())#source_buffer#insert 
+        (fun () -> (s ())#source_view#source_buffer#insert 
           "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
 
     
@@ -697,10 +761,9 @@ class gui () =
       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
         ~callback:(function b ->
           let s = s () in
-          let status =
-           Interpretations.toggle_active_interpretations s#grafite_status b
+          let _status = Interpretations.toggle_active_interpretations s#status b
           in
-           assert false (* MATITA1.0 ???
+           assert false (* MATITA 1.0 ???
            s#set_grafite_status status*)
          );
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
@@ -711,77 +774,25 @@ class gui () =
       main#unicodeAsTexMenuItem#set_active
         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
-      HLog.set_log_callback self#console#log_callback;
+      HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg);
       GtkSignal.user_handler :=
         (function 
         | MatitaScript.ActionCancelled s -> HLog.error s
         | exn ->
           if not (Helm_registry.get_bool "matita.debug") then
-           (*CSC: MatitaScript.current ??? *)
+           (* MatitaScript.current is problably wrong, but what else
+              can we do? *)
            notify_exn (MatitaScript.current ())#source_view exn
           else raise exn);
-      let disableSave () =
-        (s())#assignFileName None;
-        main#saveMenuItem#misc#set_sensitive false
-      in
-      let saveAsScript () =
-        let script = s () in
-        match self#chooseFile ~ok_not_exists:true () with
-        | Some f -> 
-              HExtlib.touch f;
-              script#assignFileName (Some f);
-              script#saveToFile (); 
-              console#message ("'"^f^"' saved.\n");
-              self#_enableSaveTo f
-        | None -> ()
-      in
-      let saveScript () =
-        let script = s () in
-        if script#has_name then 
-          (script#saveToFile (); 
-          console#message ("'"^script#filename^"' saved.\n"))
-        else saveAsScript ()
-      in
-      let abandon_script () =
-       let source_view = source_view () in
-        let grafite_status = (s ())#grafite_status in
-        if source_view#buffer#modified then
-          (match ask_unsaved main#toplevel with
-          | `YES -> saveScript ()
-          | `NO -> ()
-          | `CANCEL -> raise MatitaTypes.Cancel);
-        save_moo grafite_status
-      in
       let loadScript () =
-        let source_view = source_view () in
-        let script = s () in 
         try 
           match self#chooseFile () with
-          | Some f -> 
-              abandon_script ();
-              script#reset (); 
-              script#assignFileName (Some f);
-              source_view#source_buffer#begin_not_undoable_action ();
-              script#loadFromFile f; 
-              source_view#source_buffer#end_not_undoable_action ();
-              source_view#buffer#move_mark `INSERT source_view#buffer#start_iter;
-              source_view#buffer#place_cursor source_view#buffer#start_iter;
-              console#message ("'"^f^"' loaded.\n");
-              self#_enableSaveTo f
+          | Some f -> self#loadScript f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
-      let newScript () = 
-        let source_view = source_view () in
-        abandon_script ();
-        source_view#source_buffer#begin_not_undoable_action ();
-        (s ())#reset (); 
-        (s ())#template (); 
-        source_view#source_buffer#end_not_undoable_action ();
-        disableSave ()
-      in
       let cursor () =
-       let source_view = source_view () in
+       let source_view = (s ())#source_view in
         source_view#source_buffer#place_cursor
           (source_view#source_buffer#get_iter_at_mark (`NAME "locked")) in
       let advance (script: MatitaScript.script) = script#advance (); cursor () in
@@ -796,19 +807,14 @@ class gui () =
       let jump () = locker (keep_focus jump) (MatitaScript.current ()) in
         (* quit *)
       self#setQuitCallback (fun () -> 
-(*CSC: iterare su tutti gli script! 
-        let script = MatitaScript.current () in
-        if source_view#buffer#modified then
-          match ask_unsaved main#toplevel with
-          | `YES -> 
-               saveScript ();
-               save_moo script#grafite_status;
-               GMain.Main.quit ()
-          | `NO -> GMain.Main.quit ()
-          | `CANCEL -> ()
-        else 
-          (save_moo script#grafite_status;
-          GMain.Main.quit ())*) assert false);
+       let cancel = ref false in
+        MatitaScript.iter_scripts
+         (fun script ->
+           if not !cancel then
+            if not (self#closeScript0 script) then
+             cancel := true);
+        if not !cancel then
+         GMain.Main.quit ());
       connect_button main#scriptAdvanceButton advance;
       connect_button main#scriptRetractButton retract;
       connect_button main#scriptTopButton top;
@@ -821,25 +827,20 @@ class gui () =
       connect_menu_item main#scriptBottomMenuItem bottom;
       connect_menu_item main#scriptJumpMenuItem jump;
       connect_menu_item main#openMenuItem   loadScript;
-      connect_menu_item main#saveMenuItem   saveScript;
-      connect_menu_item main#saveAsMenuItem saveAsScript;
-      connect_menu_item main#newMenuItem    newScript;
+      connect_menu_item main#saveMenuItem 
+       (fun () -> self#saveScript (MatitaScript.current ()));
+      connect_menu_item main#saveAsMenuItem
+       (fun () -> self#saveAsScript (MatitaScript.current ()));
+      connect_menu_item main#newMenuItem self#newScript;
+      connect_menu_item main#closeMenuItem self#closeCurrentScript;
       connect_menu_item main#showCoercionsGraphMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Coercions));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions)));
       connect_menu_item main#showHintsDbMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Hints));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints)));
       connect_menu_item main#showTermGrammarMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Grammar));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar)));
       connect_menu_item main#showUnicodeTable
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `TeX));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX)));
         (* debug menu *)
       main#debugMenu#misc#hide ();
         (* HBUGS *)
@@ -862,16 +863,23 @@ class gui () =
       main#hpaneScriptSequent#set_position script_w;
       (* math view handling *)
       connect_menu_item main#newCicBrowserMenuItem (fun () ->
-        ignore(MatitaMathView.cicBrowser ()));
+        ignore(MatitaMathView.cicBrowser None));
       connect_menu_item main#increaseFontSizeMenuItem
         MatitaMisc.increase_font_size;
       connect_menu_item main#decreaseFontSizeMenuItem
         MatitaMisc.decrease_font_size;
       connect_menu_item main#normalFontSizeMenuItem
         MatitaMisc.reset_font_size;
+      ignore (main#scriptNotebook#connect#switch_page (fun page ->
+        self#save_page ();
+        current_page <- page;
+        let script = MatitaScript.at_page page in
+        script#activate;
+        main#saveMenuItem#misc#set_sensitive script#has_name))
 
     method private externalEditor () =
-     let source_view = source_view () in
+     let script = MatitaScript.current () in
+     let source_view = script#source_view in
       let cmd = Helm_registry.get "matita.external_editor" in
 (* ZACK uncomment to enable interactive ask of external editor command *)
 (*      let cmd =
@@ -884,7 +892,6 @@ class gui () =
         ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false
           ~default:(Helm_registry.get "matita.external_editor") ()
       in *)
-      let script = MatitaScript.current () in
       let fname = script#filename in
       let slice mark =
         source_view#source_buffer#start_iter#get_slice
@@ -927,9 +934,98 @@ class gui () =
       | Exit -> ()
       | Invalid_argument _ -> script#goto `Bottom ()
 
+    method private saveAsScript script = 
+     match self#chooseFile ~ok_not_exists:true () with
+     | Some f -> 
+           HExtlib.touch f;
+           script#assignFileName (Some f);
+           script#saveToFile (); 
+           console#message ("'"^f^"' saved.\n");
+           self#_enableSaveTo f
+     | None -> ()
+
+    method private saveScript script = 
+     if script#has_name then 
+       (script#saveToFile (); 
+        console#message ("'"^script#filename^"' saved.\n"))
+     else self#saveAsScript script
+    
+    (* returns false if closure is aborted by the user *)
+    method private closeScript0 script = 
+      if script#source_view#buffer#modified then
+        match
+         ask_unsaved main#toplevel (Filename.basename script#filename)
+        with
+        | `YES -> 
+             self#saveScript script;
+             save_moo script#status;
+             true
+        | `NO -> true
+        | `CANCEL -> false
+      else 
+       (save_moo script#status; true)
+
+    method private closeScript page script = 
+     if self#closeScript0 script then
+      begin
+       MatitaScript.destroy page;
+       ignore (main#scriptNotebook#remove_page page)
+      end
+
+    method private closeCurrentScript () = 
+     let page = main#scriptNotebook#current_page in
+     let script = MatitaScript.at_page page in 
+      self#closeScript page script
+
+    method private save_page () =
+      if current_page >= 0 then
+        let old_script = MatitaScript.at_page current_page in
+        save_moo0 ~do_clean:false old_script old_script#status
+
+    method newScript () = 
+       self#save_page ();
+       let scrolledWindow = GBin.scrolled_window () in
+       let hbox = GPack.hbox () in
+       let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
+       let _ =
+        GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in
+       let closebutton =
+        GButton.button ~relief:`NONE ~packing:hbox#pack () in
+       let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
+       closebutton#set_image image#coerce;
+       let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
+        ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
+         scrolledWindow#coerce);
+        ignore (closebutton#connect#clicked (fun () ->
+         self#closeScript
+          (main#scriptNotebook#page_num scrolledWindow#coerce) script));
+        main#scriptNotebook#goto_page 0;
+        sequents_viewer#reset;
+        sequents_viewer#load_logo;
+        let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+        let sequents_observer status =
+          sequents_viewer#reset;
+          match status#ng_mode with
+             `ProofMode ->
+              sequents_viewer#nload_sequents status;
+              (try
+                let goal =
+                 Continuationals.Stack.find_goal status#stack
+                in
+                 sequents_viewer#goto_sequent status goal
+              with Failure _ -> ());
+           | `CommandMode -> sequents_viewer#load_logo
+        in
+        script#addObserver sequents_observer;
+        script#addObserver browser_observer
+
     method loadScript file =       
-     let source_view = source_view () in
-      let script = MatitaScript.current () in
+     let page = main#scriptNotebook#current_page in
+     let script = MatitaScript.at_page page in
+      if script#source_view#buffer#modified || script#has_name then
+       self#newScript ();
+     let script = MatitaScript.current () in
+     let source_view = script#source_view in
       script#reset (); 
       script#assignFileName (Some file);
       let file = script#filename in
@@ -944,53 +1040,27 @@ class gui () =
       source_view#buffer#place_cursor source_view#buffer#start_iter;
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file
-      
+
     method private _enableSaveTo file =
       self#main#saveMenuItem#misc#set_sensitive true
         
-    method console = console
-    method fileSel = fileSel
-    method findRepl = findRepl
+    method private console = console
+    method private fileSel = fileSel
+    method private findRepl = findRepl
     method main = main
 
-    method newBrowserWin () =
-      object (self)
-        inherit browserWin ()
-        val combo = GEdit.entry ()
-        initializer
-          self#check_widgets ();
-          let combo_widget = combo#coerce in
-          uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
-          combo#misc#grab_focus ()
-        method browserUri = combo
-      end
-
-    method newUriDialog () =
-      let dialog = new uriChoiceDialog () in
-      dialog#check_widgets ();
-      dialog
-
-    method newConfirmationDialog () =
-      let dialog = new confirmationDialog () in
-      dialog#check_widgets ();
-      dialog
-
-    method newEmptyDialog () =
-      let dialog = new emptyDialog () in
-      dialog#check_widgets ();
-      dialog
-
-    method private addKeyBinding key callback =
-      List.iter (fun evbox -> add_key_binding key callback evbox)
+    method private addKeyBinding key ?modifiers callback =
+(*       List.iter (fun evbox -> add_key_binding key callback evbox) *)
+      List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback)
         keyBindingBoxes
 
-    method setQuitCallback callback =
+    method private setQuitCallback callback =
       connect_menu_item main#quitMenuItem callback;
       ignore (main#toplevel#event#connect#delete 
         (fun _ -> callback ();true));
       self#addKeyBinding GdkKeysyms._q callback
 
-    method chooseFile ?(ok_not_exists = false) () =
+    method private chooseFile ?(ok_not_exists = false) () =
       _ok_not_exists <- ok_not_exists;
       _only_directory <- false;
       fileSel#fileSelectionWin#show ();
@@ -1005,106 +1075,19 @@ class gui () =
       (* we should check that this is a directory *)
       chosen_file
   
-    method askText ?(title = "") ?(msg = "") () =
-      let dialog = new textDialog () in
-      dialog#textDialog#set_title title;
-      dialog#textDialogLabel#set_label msg;
-      let text = ref None in
-      let return v =
-        text := v;
-        dialog#textDialog#destroy ();
-        GMain.Main.quit ()
-      in
-      ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
-      connect_button dialog#textDialogCancelButton (fun _ -> return None);
-      connect_button dialog#textDialogOkButton (fun _ ->
-        let text = dialog#textDialogTextView#buffer#get_text () in
-        return (Some text));
-      dialog#textDialog#show ();
-      GtkThread.main ();
-      !text
-
   end
 
 let gui () = 
   let g = new gui () in
-  gui_instance := Some g;
-  MatitaMisc.set_gui g;
-  g
+  let rg = (g :> MatitaGuiTypes.gui) in
+  MatitaMisc.set_gui rg;
+  g#newScript ();
+  rg
   
 let instance = singleton gui
 
 let non p x = not (p x)
 
-(* this is a shit and should be changed :-{ *)
-let interactive_uri_choice
-  ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
-  ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
-  ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) 
-  ?copy_cb ()
-  ~id uris
-=
-  let gui = instance () in
-  if (selection_mode <> `SINGLE) &&
-    (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
-  then
-    uris
-  else begin
-    let dialog = gui#newUriDialog () in
-    if hide_uri_entry then
-      dialog#uriEntryHBox#misc#hide ();
-    if hide_try then
-      begin
-      dialog#uriChoiceSelectedButton#misc#hide ();
-      dialog#uriChoiceConstantsButton#misc#hide ();
-      end;
-    dialog#okLabel#set_label ok_label;  
-    dialog#uriChoiceTreeView#selection#set_mode
-      (selection_mode :> Gtk.Tags.selection_mode);
-    let model = new stringListModel dialog#uriChoiceTreeView in
-    let choices = ref None in
-    (match copy_cb with
-    | None -> ()
-    | Some cb ->
-        dialog#copyButton#misc#show ();
-        connect_button dialog#copyButton 
-        (fun _ ->
-          match model#easy_selection () with
-          | [u] -> (cb u)
-          | _ -> ()));
-    dialog#uriChoiceDialog#set_title title;
-    dialog#uriChoiceLabel#set_text msg;
-    List.iter model#easy_append (List.map NReference.string_of_reference uris);
-    dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
-    let return v =
-      choices := v;
-      dialog#uriChoiceDialog#destroy ();
-      GMain.Main.quit ()
-    in
-    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
-    connect_button dialog#uriChoiceConstantsButton (fun _ ->
-      return (Some uris));
-    if ok_action = `AUTO then
-      connect_button dialog#uriChoiceAutoButton (fun _ ->
-        Helm_registry.set_bool "matita.auto_disambiguation" true;
-        return (Some uris))
-    else
-      connect_button dialog#uriChoiceAutoButton (fun _ ->
-        match model#easy_selection () with
-        | [] -> ()
-        | uris -> return (Some (List.map NReference.reference_of_string uris)));
-    connect_button dialog#uriChoiceSelectedButton (fun _ ->
-      match model#easy_selection () with
-      | [] -> ()
-      | uris -> return (Some (List.map NReference.reference_of_string uris)));
-    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
-    dialog#uriChoiceDialog#show ();
-    GtkThread.main ();
-    (match !choices with 
-    | None -> raise MatitaTypes.Cancel
-    | Some uris -> uris)
-  end
-
 class interpModel =
   let cols = new GTree.column_list in
   let id_col = cols#add Gobject.Data.string in
@@ -1157,66 +1140,65 @@ class interpModel =
 let interactive_string_choice 
   text prefix_len ?(title = "") ?(msg = "") () ~id locs uris 
 = 
-  let gui = instance () in
-    let dialog = gui#newUriDialog () in
-    dialog#uriEntryHBox#misc#hide ();
-    dialog#uriChoiceSelectedButton#misc#hide ();
-    dialog#uriChoiceAutoButton#misc#hide ();
-    dialog#uriChoiceConstantsButton#misc#hide ();
-    dialog#uriChoiceTreeView#selection#set_mode
-      (`SINGLE :> Gtk.Tags.selection_mode);
-    let model = new stringListModel dialog#uriChoiceTreeView in
-    let choices = ref None in
-    dialog#uriChoiceDialog#set_title title; 
-    let hack_len = MatitaGtkMisc.utf8_string_length text in
-    let rec colorize acc_len = function
-      | [] -> 
-          let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
-          escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
-      | he::tl -> 
-          let start, stop =  HExtlib.loc_of_floc he in
-          let floc1 = HExtlib.floc_of_loc (acc_len,start) in
-          let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
-          let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
-          escape_pango_markup str1 ^ "<b>" ^ 
-          escape_pango_markup str2 ^ "</b>" ^ 
-          colorize stop tl
-    in
+ let dialog = new uriChoiceDialog () in
+ dialog#uriEntryHBox#misc#hide ();
+ dialog#uriChoiceSelectedButton#misc#hide ();
+ dialog#uriChoiceAutoButton#misc#hide ();
+ dialog#uriChoiceConstantsButton#misc#hide ();
+ dialog#uriChoiceTreeView#selection#set_mode
+   (`SINGLE :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ dialog#uriChoiceDialog#set_title title; 
+ let hack_len = MatitaGtkMisc.utf8_string_length text in
+ let rec colorize acc_len = function
+   | [] -> 
+       let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
+       escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
+   | he::tl -> 
+       let start, stop =  HExtlib.loc_of_floc he in
+       let floc1 = HExtlib.floc_of_loc (acc_len,start) in
+       let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
+       let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
+       escape_pango_markup str1 ^ "<b>" ^ 
+       escape_pango_markup str2 ^ "</b>" ^ 
+       colorize stop tl
+ in
 (*     List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
-                Printf.eprintf "(%d,%d)" start stop) locs; *)
-    let locs = 
-      List.sort 
-        (fun loc1 loc2 -> 
-          fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) 
-        locs 
-    in
+              Printf.eprintf "(%d,%d)" start stop) locs; *)
+  let locs = 
+    List.sort 
+      (fun loc1 loc2 -> 
+        fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) 
+      locs 
+  in
 (*     prerr_endline "XXXXXXXXXXXXXXXXXXXX";
-    List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
-                Printf.eprintf "(%d,%d)" start stop) locs;
-    prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
-    dialog#uriChoiceLabel#set_use_markup true;
-    let txt = colorize 0 locs in
-    let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
-      (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
-    in
-    dialog#uriChoiceLabel#set_label txt;
-    List.iter model#easy_append uris;
-    let return v =
-      choices := v;
-      dialog#uriChoiceDialog#destroy ();
-      GMain.Main.quit ()
-    in
-    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
-    connect_button dialog#uriChoiceForwardButton (fun _ ->
-      match model#easy_selection () with
-      | [] -> ()
-      | uris -> return (Some uris));
-    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
-    dialog#uriChoiceDialog#show ();
-    GtkThread.main ();
-    (match !choices with 
-    | None -> raise MatitaTypes.Cancel
-    | Some uris -> uris)
+  List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
+              Printf.eprintf "(%d,%d)" start stop) locs;
+  prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
+  dialog#uriChoiceLabel#set_use_markup true;
+  let txt = colorize 0 locs in
+  let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
+    (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
+  in
+  dialog#uriChoiceLabel#set_label txt;
+  List.iter model#easy_append uris;
+  let return v =
+    choices := v;
+    dialog#uriChoiceDialog#destroy ();
+    GMain.Main.quit ()
+  in
+  ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+  connect_button dialog#uriChoiceForwardButton (fun _ ->
+    match model#easy_selection () with
+    | [] -> ()
+    | uris -> return (Some uris));
+  connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+  dialog#uriChoiceDialog#show ();
+  GtkThread.main ();
+  (match !choices with 
+  | None -> raise MatitaTypes.Cancel
+  | Some uris -> uris)
 
 let interactive_interp_choice () text prefix_len choices =
 (*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)