X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=c29e15533ef1c6a71a10c06b04a46cec6f95481a;hb=refs%2Fheads%2F0.4.95;hp=69e92518d601bfd6aadf8ef49c05af6e1da5d0c5;hpb=871d9b1d66f79445e7afa6d42205aaf33576c4f0;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 69e92518d..c29e15533 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -402,14 +402,20 @@ let cic2grafite context menv t =
       let pres_term = TermContentPres.pp_ast content_term in
       let dummy_tbl = Hashtbl.create 1 in
       let markup = CicNotationPres.render dummy_tbl pres_term in
-      let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in
+      let s = "(" ^ BoxPp.render_to_string
+       ~map_unicode_to_tex:(Helm_registry.get_bool
+         "matita.paste_unicode_as_tex")
+       List.hd width markup ^ ")" in
       Pcre.substitute 
         ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
     in
     CicNotationPp.set_pp_term term_pp;
     let lazy_term_pp = fun x -> assert false in
     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
-    GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+    GrafiteAstPp.pp_statement
+     ~map_unicode_to_tex:(Helm_registry.get_bool
+       "matita.paste_unicode_as_tex")
+     ~term_pp ~lazy_term_pp ~obj_pp t
   in
   let script = String.concat "" (List.map pp ast) in
   prerr_endline script;
@@ -433,7 +439,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
     let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
     TAPp.pp_macro 
       ~term_pp:(fun x -> 
-        ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x))
+        ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x)
+         ~map_unicode_to_tex:(Helm_registry.get_bool
+           "matita.paste_unicode_as_tex"))
   in
   match mac with
   (* WHELP's stuff *)
@@ -470,7 +478,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], "", parsed_text_length
   (* REAL macro *)
-  | TA.Hint loc -> 
+  | TA.Hint (loc, rewrite) -> 
       let user_goal' =
        match user_goal with
           Some n -> n
@@ -478,35 +486,45 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       in
       let proof = GrafiteTypes.get_current_proof grafite_status in
       let proof_status = proof,user_goal' in
-      let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
-      let selected = guistuff.urichooser l in
-      (match selected with
-      | [] -> [], "", parsed_text_length
-      | [uri] -> 
-          let suri = UriManager.string_of_uri uri in
-          let ast loc =
-            TA.Executable (loc, (TA.Tactic (loc,
-             Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
-             TA.Dot loc))) in
-          let text =
-           comment parsed_text ^ "\n" ^
-            pp_eager_statement_ast (ast HExtlib.dummy_floc) in
-          let text_len = MatitaGtkMisc.utf8_string_length text in
-          let loc = HExtlib.floc_of_loc (0,text_len) in
-          let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
-          let res,_,_parsed_text_len =
-           eval_statement include_paths buffer guistuff lexicon_status
-            grafite_status user_goal script statement
-          in
-           (* we need to replace all the parsed_text *)
-           res,"",String.length parsed_text
-      | _ -> 
-          HLog.error 
-            "The result of the urichooser should be only 1 uri, not:\n";
-          List.iter (
-            fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
-          ) selected;
-          assert false)
+      if rewrite then
+        let l = MQ.equations_for_goal ~dbd proof_status in
+        let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in
+        let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in
+        guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+        [], "", parsed_text_length
+      else
+        let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
+        let selected = guistuff.urichooser l in
+        (match selected with
+        | [] -> [], "", parsed_text_length
+        | [uri] -> 
+            let suri = UriManager.string_of_uri uri in
+            let ast loc =
+              TA.Executable (loc, (TA.Tactic (loc,
+               Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+               TA.Dot loc))) in
+            let text =
+             comment parsed_text ^ "\n" ^
+              pp_eager_statement_ast (ast HExtlib.dummy_floc)
+              ~map_unicode_to_tex:(Helm_registry.get_bool
+                "matita.paste_unicode_as_tex")
+            in
+            let text_len = MatitaGtkMisc.utf8_string_length text in
+            let loc = HExtlib.floc_of_loc (0,text_len) in
+            let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
+            let res,_,_parsed_text_len =
+             eval_statement include_paths buffer guistuff lexicon_status
+              grafite_status user_goal script statement
+            in
+             (* we need to replace all the parsed_text *)
+             res,"",String.length parsed_text
+        | _ -> 
+            HLog.error 
+              "The result of the urichooser should be only 1 uri, not:\n";
+            List.iter (
+              fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
+            ) selected;
+            assert false)
   | TA.Check (_,term) ->
       let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
       let context =