]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaScript.ml
fix
[helm.git] / helm / matita / matitaScript.ml
index da2c5b2fa168a85080812a7e329004d38f2a2c4d..c8411d5cf4e0d5b40d45492bf6e5cfb627af02cd 100644 (file)
@@ -83,6 +83,9 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | None -> []
         | Some devel -> [MatitamakeLib.root_for_development devel ]
   in
+  let include_ =
+    include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+  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
@@ -226,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
@@ -236,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) -> 
@@ -251,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) ->
@@ -267,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 *)
@@ -300,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 
@@ -500,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 *)