Implemented standard semantics of Load in MTI: loading a file when the current

[helm.git] / matita / matita / matitaGui.ml

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 9b32cf0b57984dcf4323bdfbcd772fd9fe79d2c3..489afc2838507c3c4b0fd5ada1f0dd21664a995e 100644 (file)
--- 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 ();