From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Dec 2010 15:13:41 +0000 (+0000)
Subject: Implemented standard semantics of Load in MTI: loading a file when the current
X-Git-Tag: make_still_working~2622
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4b3a9a15edbab7a3aa819155dc1ac1eec1ddb0a3;p=helm.git

Implemented standard semantics of Load in MTI: loading a file when the current
one is unnamed and not modified does not open a new tab.
---

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 9b32cf0b5..489afc283 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -1031,7 +1031,10 @@ class gui () =
         script#addObserver browser_observer
 
     method loadScript file =       
-     self#newScript ();
+     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 ();