src/Pure/Tools/proof_general.ML
changeset 56333 38f1422ef473
parent 56208 06cc31dff138
--- 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.";