Management of automatic insertion of aliases and "goal" commands reimplemented

almost from scratch. The new commands inserted are now distinct entities in
the history. As a consequence going up in the script is now a step by step
operation and going up and going down are invertible operations, as they
should be.

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 9f05b28e0e431d9c4a95369db16e02e0dbe98527..4200a4e95e66355376b9558871596ca24cb05dd7 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -47,10 +47,6 @@ TODO
 
   GUI GRAFICA
   - integrare il famoso logo mancante (anche nell'About dialog)
-  - invertibilita' dell'inserimento automatico di alias: quando si torna
-    su bisognerebbe tornare su di un passo e non fare undo degli alias
-    (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
-    script uno stato appartiene)
   - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
     finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
     codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
@@ -94,6 +90,10 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
 DONE
+- invertibilita' dell'inserimento automatico di alias: quando si torna
+  su bisognerebbe tornare su di un passo e non fare undo degli alias
+  (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
+  script uno stato appartiene) -> CSC
 - bug di refresh del widget quando si avanza ("swap" tra la finestra dei
   sequenti e la finestra dello script) -> CSC
 - sensitiveness per goto begin/end/etc. (???) -> Gares

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index bcb715f2dcd8019cd6c70f0a9fe678306495c036..7f73e2ec4d3139a14c9134aff80afd95272964c7 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -36,6 +36,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*)(.*)"
 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
 let newline_RE = Pcre.regexp "\n"
@@ -53,12 +54,6 @@ 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
@@ -87,20 +82,29 @@ 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 goal_changed = ref false in
-  let status =
+    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 status.proof_status with
       | Incomplete_proof (_, goal) when goal <> user_goal ->
-          goal_changed := true;
+         let status =
           MatitaEngine.eval_ast ~include_paths:include_
-            ~do_heavy_checks:true status (goal_ast user_goal)
-      | _ -> status
-  in
+            ~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
   let new_status = 
     MatitaEngine.eval_ast 
-      ~include_paths:include_ ~do_heavy_checks:true status st 
+      ~include_paths:include_ ~do_heavy_checks:true new_status st 
   in
   let new_aliases =
     match ex with
@@ -109,11 +113,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 new_aliases = 
+  let initial_space,status,new_status_and_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
     DTE.fold (
-      fun k ((v,_) as value) acc -> 
+      fun k ((v,_) as value) (initial_space,status,acc) -> 
         let b = 
           try
             let v = UM.strip_xpointer (UM.uri_of_string v) in
@@ -121,27 +125,24 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           with UM.IllFormedUri _ -> false
         in
         if b then 
-          acc
+          initial_space,status,acc
         else
-          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
+         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]
   in
-    [ new_status, new_text ], parsed_text_length
+   res,parsed_text_length
 
 let eval_with_engine guistuff status user_goal parsed_text st =
   try