X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=c8411d5cf4e0d5b40d45492bf6e5cfb627af02cd;hb=64e9baf5488aa0ad2e2d356ef6eb72b8ecb9fca0;hp=c14bd77101628212a200e1066d31252c9c9792b5;hpb=7ecd356fa7f7227d10f27ce195ea21b6508ba6ee;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c14bd7710..c8411d5cf 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -229,6 +229,10 @@ let disambiguate_macro_term term status user_goal =
   match interps with 
   | [_,_,x,_], _ -> x
   | _ -> assert false
+
+let pp_eager_statement_ast =
+  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
  
 let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   let module TAPp = GrafiteAstPp in
@@ -239,6 +243,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
+  (* XXX use a real CIC -> string pretty printer *)
+  let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
@@ -254,12 +260,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   | TA.WInstance (loc, term) ->
       let term = disambiguate_macro_term term status user_goal in
       let l = Whelp.instance ~dbd term in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WLocate (loc, s) -> 
       let l = Whelp.locate ~dbd s in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+      let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WElim (loc, term) ->
@@ -270,14 +276,14 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
         | _ -> failwith "Not a MutInd"
       in
       let l = Whelp.elim ~dbd uri in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WHint (loc, term) ->
       let term = disambiguate_macro_term term status user_goal in
       let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   (* REAL macro *)
@@ -303,9 +309,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
           status ast in
         let extra_text = 
-          comment parsed_text ^ 
-          "\n" ^ TAPp.pp_statement ast
-        in
+          comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
         [ new_status , (extra_text, ast) ], parsed_text_length
       | _ -> 
           HLog.error 
@@ -503,15 +507,14 @@ object (self)
       let start = buffer#get_iter_at_mark (`MARK locked_mark) in
       let new_text = String.concat "" new_statements in
       if statement <> None then
-       buffer#insert ~iter:start new_text
-      else
+        buffer#insert ~iter:start new_text
+      else begin
         let s = match st with `Raw s | `Ast (_, s) -> s in
-        if new_text <> String.sub s 0 parsed_len then
-        begin
-          let stop = start#copy#forward_chars parsed_len in
-          buffer#delete ~start ~stop;
+        if new_text <> String.sub s 0 parsed_len then begin
+          buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
           buffer#insert ~iter:start new_text;
         end;
+      end;
       self#moveMark (String.length new_text);
       (*
       (match List.rev new_asts with (* advance again on punctuation *)