diff -r 3e62e68fb342 -r 38f1422ef473 src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Sun Mar 30 21:24:59 2014 +0200 +++ b/src/Pure/Tools/proof_general.ML Mon Mar 31 10:28:08 2014 +0200 @@ -258,8 +258,8 @@ (* hooks *) -fun message bg en prfx text = - (case render text of +fun message bg en prfx body = + (case render (implode body) of "" => () | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s))); @@ -276,7 +276,7 @@ (* notification *) -val emacs_notify = message (special "I") (special "J") ""; +fun emacs_notify s = message (special "I") (special "J") "" [s]; fun tell_clear_goals () = emacs_notify "Proof General, please clear the goals buffer.";