# HG changeset patch
# User wenzelm
# Date 1221686629 -7200
# Node ID dbe9c820e4d244f73d946fdc3c8d43def32eeb5c
# Parent  44664ffc9725899fcf07d9d343e510ceca1215d9
threads work only for Poly/ML 5.2 or later;
global ML bindings are now thread-safe;

diff -r 44664ffc9725 -r dbe9c820e4d2 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Sep 17 23:23:13 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Sep 17 23:23:49 2008 +0200
@@ -107,13 +107,12 @@
 section {* Thread-safe programming *}
 
 text {*
-  Recent versions of Poly/ML (5.1 or later) support multithreaded
-  execution based on native operating system threads of the
-  underlying platform.  Thus threads will actually be executed in
-  parallel on multi-core systems.  A speedup-factor of approximately
-  2--4 can be expected for large well-structured Isabelle sessions,
-  where theories are organized as a graph with sufficiently many
-  independent nodes.
+  Recent versions of Poly/ML (5.2 or later) support multithreaded
+  execution based on native operating system threads of the underlying
+  platform.  Thus threads will actually be executed in parallel on
+  multi-core systems.  A speedup-factor of approximately 2--4 can be
+  expected for large well-structured Isabelle sessions, where theories
+  are organized as a graph with sufficiently many independent nodes.
 
   Threads lack the memory protection of separate processes, but
   operate concurrently on shared heap memory.  This has the advantage
@@ -139,15 +138,17 @@
   independent of the visibility of such mutable values in the toplevel
   scope.}
 
-  \item global ML bindings in the toplevel environment (@{verbatim
-  "type"}, @{verbatim val}, @{verbatim "structure"} etc.) due to
-  run-time invocation of the compiler,
-
   \item direct I/O on shared channels, notably @{text "stdin"}, @{text
   "stdout"}, @{text "stderr"}.
 
   \end{itemize}
 
+  Note that ML bindings within the toplevel environment (@{verbatim
+  "type"}, @{verbatim val}, @{verbatim "structure"} etc.) due to
+  run-time invocation of the compiler are non-critical, because
+  Isabelle/Isar incorporates such bindings within the theory or proof
+  context.
+
   The majority of tools implemented within the Isabelle/Isar framework
   will not require any of these critical elements: nothing special
   needs to be observed when staying in the purely functional fragment
@@ -179,8 +180,8 @@
   significantly.
 
   Despite this potential bottle-neck, we refrain from fine-grained
-  locking mechanisms: the restriction to a single lock prevents
-  deadlocks without demanding further considerations in user programs.
+  locking mechanism within user-code: the restriction to a single lock
+  prevents deadlocks without demanding special precautions.
 
   \paragraph{Good conduct of impure programs.} The following
   guidelines enable non-functional programs to participate in
@@ -231,18 +232,6 @@
   be marked critical as well, to prevent intruding another threads
   local view, and a lost-update in the global scope, too.
 
-  \item Minimize global ML bindings.  Processing theories occasionally
-  affects the global ML environment as well.  While each ML
-  compilation unit is safe, the order of scheduling of independent
-  declarations might cause problems when composing several modules
-  later on, due to hiding of previous ML names.
-
-  This cannot be helped in general, because the ML toplevel lacks the
-  graph structure of the Isabelle theory space.  Nevertheless, some
-  sound conventions of keeping global ML names essentially disjoint
-  (e.g.\ with the help of ML structures) prevents the problem to occur
-  in most practical situations.
-
   \end{itemize}
 
   Recall that in an open ``LCF-style'' system like Isabelle/Isar, the
diff -r 44664ffc9725 -r dbe9c820e4d2 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Sep 17 23:23:13 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Sep 17 23:23:49 2008 +0200
@@ -128,13 +128,12 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Recent versions of Poly/ML (5.1 or later) support multithreaded
-  execution based on native operating system threads of the
-  underlying platform.  Thus threads will actually be executed in
-  parallel on multi-core systems.  A speedup-factor of approximately
-  2--4 can be expected for large well-structured Isabelle sessions,
-  where theories are organized as a graph with sufficiently many
-  independent nodes.
+Recent versions of Poly/ML (5.2 or later) support multithreaded
+  execution based on native operating system threads of the underlying
+  platform.  Thus threads will actually be executed in parallel on
+  multi-core systems.  A speedup-factor of approximately 2--4 can be
+  expected for large well-structured Isabelle sessions, where theories
+  are organized as a graph with sufficiently many independent nodes.
 
   Threads lack the memory protection of separate processes, but
   operate concurrently on shared heap memory.  This has the advantage
@@ -160,13 +159,15 @@
   independent of the visibility of such mutable values in the toplevel
   scope.}
 
-  \item global ML bindings in the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
-  run-time invocation of the compiler,
-
   \item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}.
 
   \end{itemize}
 
+  Note that ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
+  run-time invocation of the compiler are non-critical, because
+  Isabelle/Isar incorporates such bindings within the theory or proof
+  context.
+
   The majority of tools implemented within the Isabelle/Isar framework
   will not require any of these critical elements: nothing special
   needs to be observed when staying in the purely functional fragment
@@ -197,8 +198,8 @@
   significantly.
 
   Despite this potential bottle-neck, we refrain from fine-grained
-  locking mechanisms: the restriction to a single lock prevents
-  deadlocks without demanding further considerations in user programs.
+  locking mechanism within user-code: the restriction to a single lock
+  prevents deadlocks without demanding special precautions.
 
   \paragraph{Good conduct of impure programs.} The following
   guidelines enable non-functional programs to participate in
@@ -246,18 +247,6 @@
   be marked critical as well, to prevent intruding another threads
   local view, and a lost-update in the global scope, too.
 
-  \item Minimize global ML bindings.  Processing theories occasionally
-  affects the global ML environment as well.  While each ML
-  compilation unit is safe, the order of scheduling of independent
-  declarations might cause problems when composing several modules
-  later on, due to hiding of previous ML names.
-
-  This cannot be helped in general, because the ML toplevel lacks the
-  graph structure of the Isabelle theory space.  Nevertheless, some
-  sound conventions of keeping global ML names essentially disjoint
-  (e.g.\ with the help of ML structures) prevents the problem to occur
-  in most practical situations.
-
   \end{itemize}
 
   Recall that in an open ``LCF-style'' system like Isabelle/Isar, the