REVERT OF MY PREVIOUS COMMIT THAT INTRODUCES A CRITICAL BUG (some lines

are automatically _removed_ from the script). I will commit again as soon
as I fix the bug.

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 7f73e2ec4d3139a14c9134aff80afd95272964c7..bcb715f2dcd8019cd6c70f0a9fe678306495c036 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -36,7 +36,6 @@ 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*)(.*)"
 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
 let newline_RE = Pcre.regexp "\n"
@@ -54,6 +53,12 @@ let first_line s =
     String.sub s 0 nl_pos
   with Not_found -> s
 
+let prepend_text header base =
+  if Pcre.pmatch ~rex:heading_nl_RE base then
+    sprintf "\n%s%s" header base
+  else
+    sprintf "\n%s\n%s" header base
+
   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
 let goal_ast n =
   let module A = GrafiteAst in
@@ -82,29 +87,20 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   in
   let parsed_text_length = String.length parsed_text in
   let loc, ex = 
-    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
-  let initial_space,parsed_text =
-   try
-    let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
-     pieces.(1), pieces.(2)
-   with
-    Not_found -> "", parsed_text in
-  (* we add the goal command if needed *)
-  let inital_space,new_status,new_status_and_text_list' =
+    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false 
+  in
+  let goal_changed = ref false in
+  let status =
     match status.proof_status with
       | Incomplete_proof (_, goal) when goal <> user_goal ->
-         let status =
+          goal_changed := true;
           MatitaEngine.eval_ast ~include_paths:include_
-            ~do_heavy_checks:true status (goal_ast user_goal) in
-         let initial_space =
-          if initial_space = "" then "\n" else initial_space
-         in
-          "\n", status,
-           [status, initial_space ^ TAPp.pp_tactic (TA.Goal (loc, user_goal))]
-      | _ -> initial_space,status,[] in
+            ~do_heavy_checks:true status (goal_ast user_goal)
+      | _ -> status
+  in
   let new_status = 
     MatitaEngine.eval_ast 
-      ~include_paths:include_ ~do_heavy_checks:true new_status st 
+      ~include_paths:include_ ~do_heavy_checks:true status st 
   in
   let new_aliases =
     match ex with
@@ -113,11 +109,11 @@ let eval_with_engine guistuff status user_goal parsed_text st =
       | _ -> MatitaSync.alias_diff ~from:status new_status
   in
   (* we remove the defined object since we consider them "automatic aliases" *)
-  let initial_space,status,new_status_and_text_list_rev = 
+  let new_aliases = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
     DTE.fold (
-      fun k ((v,_) as value) (initial_space,status,acc) -> 
+      fun k ((v,_) as value) acc -> 
         let b = 
           try
             let v = UM.strip_xpointer (UM.uri_of_string v) in
@@ -125,24 +121,27 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           with UM.IllFormedUri _ -> false
         in
         if b then 
-          initial_space,status,acc
+          acc
         else
-         let new_text =
-          let initial_space =
-           if initial_space = "" then "\n" else initial_space in
-            initial_space ^
-             DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in
-         let new_status =
-          {status with aliases = DTE.add k value status.aliases}
-         in
-          "\n",new_status,((new_status, new_text)::acc)
-    ) new_aliases (initial_space,status,[]) in
-  let parsed_text = initial_space ^ parsed_text in
-  let res =
-   List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
-    [new_status, parsed_text]
+          DTE.add k value acc
+    ) new_aliases DTE.empty
+  in
+  let new_text =
+    if DisambiguateTypes.Environment.is_empty new_aliases then
+      parsed_text
+    else
+      prepend_text (DisambiguatePp.pp_environment new_aliases)
+        parsed_text
+  in
+  let new_text =
+    if !goal_changed then
+      prepend_text
+        (TAPp.pp_tactic (TA.Goal (loc, user_goal))(* ^ "\n"*))
+        new_text
+    else
+      new_text
   in
-   res,parsed_text_length
+    [ new_status, new_text ], parsed_text_length
 
 let eval_with_engine guistuff status user_goal parsed_text st =
   try