First steps towards a multi-document interface.

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index f7be5eab3e6a4f19eb2c4b32d6648125660a497d..6d4b5967209bb58831d39c8f8e8b5895f6e36a26 100644 (file)
--- a/matita/matita/matita.glade
+++ b/matita/matita/matita.glade
@@ -1679,7 +1679,7 @@
                               <widget class="GtkNotebook" id="scriptNotebook">
                                 <property name="visible">True</property>
                                 <property name="can_focus">True</property>
-                                <property name="tab_pos">bottom</property>
+                                <property name="scrollable">True</property>
                                 <child>
                                   <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
                                     <property name="visible">True</property>
@@ -1702,35 +1702,11 @@
                                   </packing>
                                 </child>
                                 <child>
-                                  <widget class="GtkScrolledWindow" id="scrolledwindow8">
-                                    <property name="visible">True</property>
-                                    <property name="can_focus">True</property>
-                                    <property name="hscrollbar_policy">automatic</property>
-                                    <property name="vscrollbar_policy">automatic</property>
-                                    <child>
-                                      <widget class="GtkViewport" id="viewport1">
-                                        <property name="visible">True</property>
-                                        <child>
-                                          <widget class="GtkLabel" id="label25">
-                                            <property name="visible">True</property>
-                                            <property name="label" translatable="yes">Not implemented.</property>
-                                          </widget>
-                                        </child>
-                                      </widget>
-                                    </child>
-                                  </widget>
-                                  <packing>
-                                    <property name="position">1</property>
-                                  </packing>
+                                  <placeholder/>
                                 </child>
                                 <child>
-                                  <widget class="GtkLabel" id="label13">
-                                    <property name="visible">True</property>
-                                    <property name="label" translatable="yes">outline</property>
-                                  </widget>
+                                  <placeholder/>
                                   <packing>
-                                    <property name="position">1</property>
-                                    <property name="tab_fill">False</property>
                                     <property name="type">tab</property>
                                   </packing>
                                 </child>
@@ -1761,6 +1737,7 @@
                           <widget class="GtkNotebook" id="sequentsNotebook">
                             <property name="visible">True</property>
                             <property name="can_focus">True</property>
+                            <property name="scrollable">True</property>
                           </widget>
                           <packing>
                             <property name="resize">False</property>

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index 4b8548f1932386d13f024f2f82e5789479b0409b..ee20eda897c22d9f598f5d7cf0f987d1da834fcf 100644 (file)
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -59,7 +59,6 @@ let script =
           ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
           () ~id:"boh?" uris
         with MatitaTypes.Cancel -> [])
-      ~set_star:gui#setStar
       ~ask_confirmation:
         (fun ~title ~message -> 
             MatitaGtkMisc.ask_confirmation ~title ~message 

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index cd9603f85291ea19b45874d3715122422ac08b06..7589f19f8089a878f6e6b0467f917264f967dd18 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -839,10 +839,6 @@ class gui () =
           "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
 
     
-      (* TO BE REMOVED *)
-      main#scriptNotebook#remove_page 1;
-      main#scriptNotebook#set_show_tabs false;
-      (* / TO BE REMOVED *)
       let module Hr = Helm_registry in
       MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
@@ -934,8 +930,7 @@ class gui () =
         (s ())#reset (); 
         (s ())#template (); 
         source_view#source_buffer#end_not_undoable_action ();
-        disableSave ();
-        (s ())#assignFileName None
+        disableSave ()
       in
       let cursor () =
         source_buffer#place_cursor
@@ -1262,17 +1257,6 @@ class gui () =
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file
       
-    method setStar b =
-      let s = MatitaScript.current () in
-      let w = main#toplevel in
-      let set x = w#set_title x in
-      let name = 
-        "Matita - " ^ Filename.basename s#filename ^ 
-        (if b then "*" else "") ^
-        " in " ^ s#buri_of_current_file 
-      in
-        set name
-        
     method private _enableSaveTo file =
       self#main#saveMenuItem#misc#set_sensitive true
         

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index 9b2ed087c28f4bdb6cbbdb37f463867e1779b77e..f10c0201bd863ff8cda57d48f2212d99418adf8e 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -90,7 +90,6 @@ object
   method askText: ?title:string -> ?msg:string -> unit -> string option
 
   method loadScript: string -> unit
-  method setStar: bool -> unit
 
     (** {3 Fonts} *)
   method increaseFontSize: unit -> unit

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 02f9a23b00ad504106b65387763e31361a56f5cd..75d995f780305b1db7a74d65333badc0296bb7e2 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -246,7 +246,6 @@ let fresh_script_id =
   fun () -> incr i; !i
 
 class script  ~(source_view: GSourceView2.source_view)
-              ~set_star
               ~ask_confirmation
               ~urichooser 
               () =
@@ -323,7 +322,7 @@ object (self)
     ignore (GMain.Timeout.add ~ms:300000 
        ~callback:(fun _ -> self#_saveToBackupFile ();true));
     ignore (buffer#connect#modified_changed 
-      (fun _ -> set_star buffer#modified))
+      (fun _ -> self#set_star buffer#modified))
 
   val mutable statements = []    (** executed statements *)
 
@@ -511,17 +510,26 @@ object (self)
     buffer#set_modified false
 
   method assignFileName file =
-    let file = 
-      match file with 
-      | Some f -> Some (Librarian.absolutize f)
-      | None -> None
-    in
-    filename_ <- file; 
-    include_paths_ <- 
-      (match file with Some file -> read_include_paths file | None -> []);
-    self#reset_buffer;
-    Sys.chdir self#curdir;
-    HLog.debug ("Moving to " ^ Sys.getcwd ())
+   match file with
+      None ->
+       (MatitaMisc.get_gui ())#main#scriptLabel#set_text default_fname;
+       filename_ <- None;
+       include_paths_ <- [];
+       self#reset_buffer
+    | Some file ->
+       let f = Librarian.absolutize file in
+        (MatitaMisc.get_gui ())#main#scriptLabel#set_text (Filename.basename f);
+        filename_ <- Some f;
+        include_paths_ <- read_include_paths f;
+        self#reset_buffer;
+        Sys.chdir self#curdir;
+        HLog.debug ("Moving to " ^ Sys.getcwd ())
+
+  method set_star b =
+   let label = (MatitaMisc.get_gui ())#main#scriptLabel in
+   label#set_text ((if b then "*" else "") ^ Filename.basename self#filename);
+   label#misc#set_tooltip_text
+    ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename)
     
   method saveToFile () =
     if self#has_name then
@@ -529,7 +537,7 @@ object (self)
       output_string oc (buffer#get_text ~start:buffer#start_iter
                         ~stop:buffer#end_iter ());
       close_out oc;
-      set_star false;
+      self#set_star false;
       buffer#set_modified false
     else
       HLog.error "Can't save, no filename selected"
@@ -564,7 +572,7 @@ object (self)
     let template = HExtlib.input_file BuildTimeConf.script_template in 
     buffer#insert ~iter:(buffer#get_iter `START) template;
     buffer#set_modified false;
-    set_star false
+    self#set_star false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
   try  
@@ -694,9 +702,9 @@ end
 
 let _script = ref None
 
-let script ~source_view ~urichooser ~ask_confirmation ~set_star ()
+let script ~source_view ~urichooser ~ask_confirmation ()
 =
-  let s = new script ~source_view ~ask_confirmation ~urichooser ~set_star () in
+  let s = new script ~source_view ~ask_confirmation ~urichooser () in
   _script := Some s;
   s
 

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index de95aac52ce9618500c05f5ed030aa5292a01843..02e06d2d14b2a129b57929daa4c7c81ec0a8155a 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -59,7 +59,6 @@ object
   method loadFromFile : string -> unit
   method loadFromString : string -> unit
   method saveToFile : unit -> unit
-  method filename : string
 
   (** {2 Current proof} (if any) *)
 
@@ -74,6 +73,7 @@ object
 
   (** misc *)
   method clean_dirty_lock: unit
+  method set_star: bool -> unit
   
   (* debug *)
   method dump : unit -> unit
@@ -81,14 +81,11 @@ object
 
 end
 
-  (** @param set_star callback used to set the modified symbol (usually a star
-   * "*") on the side of a script name *)
 val script: 
   source_view:GSourceView2.source_view -> 
   urichooser: (NReference.reference list -> NReference.reference list) -> 
   ask_confirmation: 
     (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> 
-  set_star: (bool -> unit) ->
   unit -> 
     script