new intro:

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 4449d3b1df8757728de30a7aafef143700efb1ab..1e63cc3d18c9d3e2af250576bf25b20e428e5aab 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -393,6 +393,14 @@ 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 =