misc tuning -- keep name space more clean;

--- a/src/Doc/Implementation/Logic.thy	Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Wed Apr 01 22:40:07 2015 +0200
@@ -982,7 +982,7 @@
 theorem (in empty) false: False
   using bad by blast
 
-ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
+ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
 
 text \<open>Thanks to the inference kernel managing sort hypothesis
   according to their logical significance, this example is merely an

--- a/src/Doc/Implementation/ML.thy	Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/ML.thy	Wed Apr 01 22:40:07 2015 +0200
@@ -736,7 +736,7 @@
 text %mlex \<open>The following artificial examples show how to produce
   adhoc output of ML values for debugging purposes.\<close>
 
-ML \<open>
+ML_val \<open>
   val x = 42;
   val y = true;
 
@@ -928,7 +928,7 @@
   list.
 \<close>
 
-ML \<open>
+ML_val \<open>
   val s =
     Buffer.empty
     |> Buffer.add "digits: "
@@ -1093,6 +1093,25 @@
     "The frumious Bandersnatch!"]);
 \<close>
 
+text \<open>
+  \medskip An alternative is to make a paragraph of freely-floating words as
+  follows.
+\<close>
+
+ML_command \<open>
+  warning (Pretty.string_of (Pretty.para
+    "Beware the Jabberwock, my son! \
+    \The jaws that bite, the claws that catch! \
+    \Beware the Jubjub Bird, and shun \
+    \The frumious Bandersnatch!"))
+\<close>
+
+text \<open>
+  This has advantages with variable window / popup sizes, but might make it
+  harder to search for message content systematically, e.g.\ by other tools or
+  by humans expecting the ``verse'' of a formal message in a fixed layout.
+\<close>
+
 
 section \<open>Exceptions \label{sec:exceptions}\<close>
 
@@ -1551,7 +1570,7 @@
   prevented.
 \<close>
 
-ML \<open>
+ML_val \<open>
   val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
 
   val list1 = fold cons items [];
@@ -1564,7 +1583,7 @@
 text \<open>The subsequent example demonstrates how to \emph{merge} two
   lists in a natural way.\<close>
 
-ML \<open>
+ML_val \<open>
   fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
 \<close>
 
@@ -1817,7 +1836,7 @@
   temporary file names.
 \<close>
 
-ML \<open>
+ML_val \<open>
   val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   @{assert} (tmp1 <> tmp2);
@@ -1878,7 +1897,7 @@
   positive integers that are unique over the runtime of the Isabelle
   process:\<close>
 
-ML \<open>
+ML_val \<open>
   local
     val counter = Synchronized.var "counter" 0;
   in
@@ -1888,9 +1907,7 @@
           let val j = i + 1
           in SOME (j, j) end);
   end;
-\<close>
-
-ML \<open>
+
   val a = next ();
   val b = next ();
   @{assert} (a <> b);

--- a/src/Doc/Implementation/Prelim.thy	Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 01 22:40:07 2015 +0200
@@ -501,6 +501,9 @@
   value can be modified within Isar text like this:
 \<close>
 
+experiment
+begin
+
 declare [[show_types = false]]
   -- \<open>declaration within (local) theory context\<close>
 
@@ -516,6 +519,8 @@
     ..
 end
 
+end
+
 text \<open>Configuration options that are not set explicitly hold a
   default value that can depend on the application context.  This
   allows to retrieve the value from another slot within the context,
@@ -720,7 +725,7 @@
 text %mlex \<open>The following simple examples demonstrate how to produce
   fresh names from the initial @{ML Name.context}.\<close>
 
-ML \<open>
+ML_val \<open>
   val list1 = Name.invent Name.context "a" 5;
   @{assert} (list1 = ["a", "b", "c", "d", "e"]);
 
@@ -732,10 +737,10 @@
 text \<open>\medskip The same works relatively to the formal context as
   follows.\<close>
 
-locale ex = fixes a b c :: 'a
+experiment fixes a b c :: 'a
 begin
 
-ML \<open>
+ML_val \<open>
   val names = Variable.names_of @{context};
 
   val list1 = Name.invent names "a" 5;
@@ -1043,7 +1048,7 @@
   concrete binding inlined into the text:
 \<close>
 
-ML \<open>Binding.pos_of @{binding here}\<close>
+ML_val \<open>Binding.pos_of @{binding here}\<close>
 
 text \<open>\medskip That position can be also printed in a message as
   follows:\<close>

--- a/src/Doc/Implementation/Proof.thy	Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/Proof.thy	Wed Apr 01 22:40:07 2015 +0200
@@ -162,7 +162,7 @@
 text %mlex \<open>The following example shows how to work with fixed term
   and type parameters and with type-inference.\<close>
 
-ML \<open>
+ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = @{context};
 
@@ -188,7 +188,7 @@
   Alternatively, fixed parameters can be renamed explicitly as
   follows:\<close>
 
-ML \<open>
+ML_val \<open>
   val ctxt0 = @{context};
   val ([x1, x2, x3], ctxt1) =
     ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
@@ -325,7 +325,7 @@
   here for testing purposes.
 \<close>
 
-ML \<open>
+ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = @{context};
 

--- a/src/Doc/Implementation/Tactic.thy	Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Wed Apr 01 22:40:07 2015 +0200
@@ -709,7 +709,7 @@
   \end{warn}
 \<close>
 
-ML \<open>
+ML_val \<open>
   (*BAD -- does not terminate!*)
   fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
 \<close>