Fixed bad newlines in output for std output and emacs.

I added a emacs_logger.
Still need to cleanup std_logger.

3 files changed, 17 insertions, 8 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index fa21506b33..d9d5e87f45 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -76,8 +76,6 @@ open Pp_control
    an option without creating a circularity: [Flags] -> [Util] ->
    [Pp] -> [Flags] *)
 let print_emacs = ref false
-let make_pp_emacs() = print_emacs:=true
-let make_pp_nonemacs() = print_emacs:=false
 
 (* The different kinds of blocks are:
    \begin{description}
@@ -378,7 +376,7 @@ let emacs_quote g =
   else hov 0 g
 
 let emacs_quote_info g =
-  if !print_emacs then str emacs_quote_info_start ++ hov 0 g ++ str emacs_quote_info_end
+  if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end
   else hov 0 g
 
 
@@ -445,13 +443,24 @@ let infobody strm = emacs_quote_info strm
 
 let std_logger ~id:_ level msg = match level with
 | Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (infobody (hov 0 msg))
+| Info -> msgnl (hov 0 msg)
 | Notice -> msgnl msg
 | Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
 | Error -> msgnl_with !err_ft (errorbody msg)
 
+let emacs_logger ~id:_ level mesg = match level with
+| Debug _ -> msgnl (debugbody mesg)
+| Info -> msgnl (infobody mesg)
+| Notice -> msgnl mesg
+| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) ()
+| Error -> msgnl_with !err_ft (errorbody mesg)
+
 let logger = ref std_logger
 
+let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
+let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
+
+
 let feedback_id = ref (Feedback.Edit 0)
 let feedback_route = ref Feedback.default_route
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 7dfcde3edb..38b5e0bfdd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -619,15 +619,15 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
           | [] , [] , _ ->
 	     msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them.");
-	     fnl () ++ fnl ()
+	     fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
           | [] , _ , _ ->
 	    msg_info (str "All the remaining goals are on the shelf.");
-	    fnl () ++ fnl ()
+	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
 	  | _ , _, _ ->
 	     msg_info (str "This subproof is complete, but there are still unfocused goals.");
-	    fnl () ++ fnl ()
+	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals
 	  end
   | _ -> pr_subgoals None sigma seeds shelf stack goals
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index dd937cf6a1..bbeb23c781 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1125,7 +1125,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let msgnl =
         let open Ftactic in
         interp_message ist s >>= fun msg ->
-        return (hov 0 msg , hov 0 msg ++ fnl ())
+        return (hov 0 msg , hov 0 msg)
       in
       let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in
       let log (msg,_) = Proofview.Trace.log (fun () -> msg) in