From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Nov 2011 15:00:42 +0000 (+0000)
Subject: The macro /by _/ now expands again to something parsable.
X-Git-Tag: make_still_working~2089
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a370b14d9f897943efe564fd1b36daa3421735b;p=helm.git

The macro /by _/ now expands again to something parsable.
---

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index bf8da8eb4..74a95bb10 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -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)