X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=d243ebb2ead2ad2c5f65708646cf25c02137e363;hb=6a1f139f8255ee861d8a30779555d72a708478ec;hp=188726d9510879720ff984782cd5d8e26fe558d6;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 188726d95..d243ebb2e 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -42,7 +42,7 @@ let safe_substring s i j =
   try String.sub s i j with Invalid_argument _ -> assert false
 
 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
-let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)((.|\n)*)"
+let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)"
 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
 let newline_RE = Pcre.regexp "\n"
@@ -84,7 +84,10 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let initial_space,parsed_text =
    try
     let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
-     pieces.(1), pieces.(2)
+    let p1 = pieces.(1) in
+    let p1_len = String.length p1 in
+    let rest = String.sub parsed_text p1_len (parsed_text_length - p1_len) in
+     p1, rest
    with
     Not_found -> "", parsed_text in
   let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
@@ -414,7 +417,7 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
-let initial_statuses =
+let initial_statuses () =
  (* these include_paths are used only to load the initial notation *)
  let include_paths =
   Helm_registry.get_list Helm_registry.string "matita.includes" in
@@ -455,7 +458,7 @@ object (self)
 
   val mutable statements = []    (** executed statements *)
 
-  val mutable history = [ initial_statuses ]
+  val mutable history = [ initial_statuses () ]
     (** list of states before having executed statements. Head element of this
       * list is the current state, last element is the state at the beginning of
       * the script.
@@ -645,7 +648,7 @@ object (self)
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ initial_statuses ];
+    history <- [ initial_statuses () ];
     userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -800,6 +803,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status s
     with 
+    | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true