From 0c04e1f673d69ac652c15705863931c45e107515 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Jul 2005 13:24:23 +0000 Subject: [PATCH] Nicer handling of automatic text insertion. --- helm/matita/matitaScript.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index bd0441bc3..7e4dcb9fc 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -57,7 +57,7 @@ let prepend_text header base = if Pcre.pmatch ~rex:heading_nl_RE base then sprintf "\n%s%s" header base else - sprintf "%s\n%s" header base + sprintf "\n%s\n%s" header base (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) let goal_ast n = @@ -130,7 +130,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = if DisambiguateTypes.Environment.is_empty new_aliases then parsed_text else - prepend_text ("\n" ^ DisambiguatePp.pp_environment new_aliases) + prepend_text (DisambiguatePp.pp_environment new_aliases) parsed_text in let new_text = -- 2.39.2