alias diffing/insertion is now handled by matitaEngine (invoked both

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index ffa356b536f1e3f9f437771089da85bc94c5629c..e4b1544f9097b764c5b1c7de285208dc8b0cd14b 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -113,49 +113,41 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
         [ grafite_status,
           initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
       | _ -> initial_space,grafite_status,[] in *)
-  let new_lexicon_status,new_grafite_status = 
+  let enriched_history_fragment =
    MatitaEngine.eval_ast ~do_heavy_checks:true
     new_lexicon_status new_grafite_status st
   in
-  let new_aliases =
-   LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
-  (* we remove the defined object since we consider them "automatic aliases" *)
-  let dummy_st =
-    TA.Comment (HExtlib.dummy_floc, TA.Note (HExtlib.dummy_floc, ""))
-  in
-  let initial_space,lexicon_status,new_status_and_text_list_rev = 
+  let _,new_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
-    let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in
-    List.fold_left (
-      fun (initial_space,lexicon_status,acc) (k,((v,_) as value)) -> 
-        let b =
-         try
-          UM.buri_of_uri (UM.uri_of_string v) = baseuri
-         with
-          UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
-        in
-        if b then 
-          initial_space,lexicon_status,acc
-        else
-         let new_text =
-          let initial_space =
-           if initial_space = "" then "\n" else initial_space in
-            initial_space ^
-             DisambiguatePp.pp_environment
-              (DisambiguateTypes.Environment.add k value
-                DisambiguateTypes.Environment.empty) in
-         let new_lexicon_status =
-          LexiconEngine.set_proof_aliases lexicon_status [k,value]
-         in
-          "\n",new_lexicon_status,(((new_grafite_status,new_lexicon_status), (new_text, Some dummy_st))::acc)
-    ) (initial_space,lexicon_status,[]) new_aliases 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_grafite_status,new_lexicon_status),(parsed_text, Some st)]
+    List.fold_right (
+      fun (_,alias) (initial_space,acc) ->
+       match alias with
+          None -> initial_space,initial_space::acc
+        | Some (k,((v,_) as value)) ->
+           let new_text =
+            let initial_space =
+             if initial_space = "" then "\n" else initial_space
+            in
+             initial_space ^
+              DisambiguatePp.pp_environment
+               (DisambiguateTypes.Environment.add k value
+                 DisambiguateTypes.Environment.empty)
+           in
+            "\n",new_text::acc
+    ) enriched_history_fragment (initial_space,[]) in
+  let new_text_list_rev =
+   match enriched_history_fragment,new_text_list_rev with
+      (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl
+    | _,_ -> assert false
   in
-   res,parsed_text_length
+   let res =
+    try
+     List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev
+    with
+     Invalid_argument _ -> assert false
+   in
+    res,parsed_text_length
 
 let eval_with_engine
      guistuff lexicon_status grafite_status user_goal parsed_text st
@@ -305,12 +297,14 @@ let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text pa
                 TA.Apply (loc, CicNotationPt.Uri (suri, None))),
                 Some (TA.Dot loc))))
           in
+(*
         let new_lexicon_status,new_grafite_status =
          MatitaEngine.eval_ast lexicon_status grafite_status ast in
         let extra_text = 
           comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
         [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ],
          parsed_text_length
+*) assert false (* implementarla con una ricorsione *)
       | _ -> 
           HLog.error 
             "The result of the urichooser should be only 1 uri, not:\n";
@@ -416,7 +410,7 @@ let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
   match st with
   | GrafiteParser.LNone loc ->
       let parsed_text, parsed_text_length = text_of_loc loc in
-       [(grafite_status,lexicon_status),(parsed_text,None)],
+       [(grafite_status,lexicon_status),parsed_text],
         parsed_text_length
   | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
       let parsed_text, parsed_text_length = text_of_loc loc in
@@ -435,9 +429,8 @@ let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
               (offset+parsed_text_length, errorll))
       in
       (match s with
-      | (statuses,(text, ast)) :: tl ->
-          (statuses,(parsed_text ^ text, ast))::tl,
-           parsed_text_length + len
+      | (statuses,text)::tl ->
+         (statuses,parsed_text ^ text)::tl,parsed_text_length + len
       | [] -> [], 0)
   | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
@@ -524,15 +517,14 @@ object (self)
         eval_statement buffer guistuff self#lexicon_status self#grafite_status
          userGoal self st
       in
-      let (new_statuses, new_statements, new_asts) =
-        let statuses, statements = List.split entries in
-        let texts, asts = List.split statements in
-        statuses, texts, asts
+      let new_statuses, new_statements =
+        let statuses, texts = List.split entries in
+        statuses, texts
       in
-      history <- List.rev new_statuses @ history;
-      statements <- List.rev new_statements @ statements;
+      history <- new_statuses @ history;
+      statements <- new_statements @ statements;
       let start = buffer#get_iter_at_mark (`MARK locked_mark) in
-      let new_text = String.concat "" new_statements in
+      let new_text = String.concat "" (List.rev new_statements) in
       if statement <> None then
         buffer#insert ~iter:start new_text
       else begin