milestone in basic_2, λδ-2A reconstructed

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 3a57745a48af9dcfd6ba76290cbd479c857b24de..4738a38f673dd55bd6b6496358b655194007a32f 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -393,6 +393,39 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
       [status, parsed_text], "", parsed_text_length
+  | TA.NIntroGuess _loc ->
+      let names_ref = ref [] in
+      let s = 
+        NTactics.intros_tac ~names_ref [] script#grafite_status 
+      in
+      let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+      let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+      [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+  | TA.NAutoInteractive (_loc, (None,a)) -> 
+      let trace_ref = ref [] in
+      let s = 
+        NnAuto.auto_tac 
+          ~params:(None,a) ~trace_ref script#grafite_status 
+      in
+      let depth = 
+        try List.assoc "depth" a
+        with Not_found -> ""
+      in
+      let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+      let thms = 
+        match !trace_ref with
+        | [] -> "{}"
+        | thms -> 
+           String.concat ", "  
+             (HExtlib.filter_map (function 
+               | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) 
+               | _ -> None) 
+             thms)
+      in
+      let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+      let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+      [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+  | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let module MQ = MetadataQuery in
@@ -400,7 +433,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
-  let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
+  let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) ->