From 7a370b14d9f897943efe564fd1b36daa3421735b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 15:00:42 +0000 Subject: [PATCH] The macro /by _/ now expands again to something parsable. --- matita/matita/matitaScript.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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) -- 2.39.2