X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=d86871963437efbac813b5e63b590f98573af5ff;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=6bf9e5e026ed6dc97a101c9ecde6a219e624c12c;hpb=2912d9bd61bc451c1135ca0a123cc30f203e93c9;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 6bf9e5e02..d86871963 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -121,7 +121,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
             ctx in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
-          status None ctx menv subst (parsed_text,parsed_text_length,
+          status `XTNone ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
@@ -132,7 +132,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
       let s = NTactics.intros_tac ~names_ref [] script#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
+      [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#status in
@@ -140,10 +140,10 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
         try List.assoc "depth" a
         with Not_found -> ""
       in
-      let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " 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 
@@ -153,7 +153,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
       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
+      [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length
   | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_executable include_paths (buffer : GText.buffer)