# HG changeset patch
# User wenzelm
# Date 1287518494 -3600
# Node ID 2b88d00d67901c55d5f616f4646c5112be30e33a
# Parent  b905971407a11d59927ee36fe233eec2c8bd5c8f
more on messages;

diff -r b905971407a1 -r 2b88d00d6790 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 19 19:46:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 19 21:01:34 2010 +0100
@@ -278,7 +278,8 @@
   Isar command.  This enables the front-end to manage commands and
   resulting messages together.  For example, after deleting a command
   from a given theory document version, the corresponding message
-  output can be retracted from the display.  *}
+  output can be retracted from the display.
+*}
 
 text %mlref {*
   \begin{mldecls}
@@ -338,6 +339,26 @@
   channels, there is no proper way to retract output when Isar command
   transactions are reset.
   \end{warn}
+
+  \begin{warn}
+  The message channels should be used in a message-oriented manner.
+  This means that multi-line output that logically belongs together
+  needs to be issued by a \emph{single} invocation of @{ML writeln}
+  etc.  with the functional concatenation of all message constituents.
+  \end{warn}
+*}
+
+text %mlex {* The following example demonstrates a multi-line
+  warning.  Note that in some situations the user sees only the first
+  line, so the most important point should be made first.
+*}
+
+ML_command {*
+  warning (cat_lines
+   ["Beware the Jabberwock, my son!",
+    "The jaws that bite, the claws that catch!",
+    "Beware the Jubjub Bird, and shun",
+    "The frumious Bandersnatch!"]);
 *}