# HG changeset patch # User wenzelm # Date 1219597063 -7200 # Node ID 26e1a7a6695d745adf2a8782bbe4fb333d1812cc # Parent fb774d10ea4c522f9a99c62b9655272aaec7fbc2 init_message: class markup in message body, not header; diff -r fb774d10ea4c -r 26e1a7a6695d src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Sun Aug 24 18:11:20 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.ML Sun Aug 24 18:57:43 2008 +0200 @@ -85,11 +85,10 @@ fun init_message () = let - val class = (Markup.classN, Markup.initN); val pid = (Markup.pidN, string_of_pid (Posix.ProcEnv.getpid ())); val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown"); - val props = message_props [class, pid, session]; - in Output.writeln_default (special "H" ^ props ^ Session.welcome () ^ special_end) end; + val text = message_text Markup.initN [XML.Text (Session.welcome ())]; + in Output.writeln_default (special "H" ^ message_props [pid, session] ^ text ^ special_end) end; end;