# HG changeset patch
# User wenzelm
# Date 1206814438 -3600
# Node ID 3a2efce3e9925adf8be9ba2d63013dfc5f4e4e29
# Parent  9d1029ce0e13efef7c8068748fb4e7b7bd28fc69
* Eliminated destructive theorem database.
* Commands 'use' and 'ML' are now purely functional; added diagnostic 'ML_val'.

diff -r 9d1029ce0e13 -r 3a2efce3e992 NEWS
--- a/NEWS	Sat Mar 29 13:03:09 2008 +0100
+++ b/NEWS	Sat Mar 29 19:13:58 2008 +0100
@@ -29,6 +29,14 @@
 
 *** Pure ***
 
+* Eliminated destructive theorem database.  Potential INCOMPATIBILITY,
+really need to observe linear functional update of theories.
+
+* Commands 'use' and 'ML' are now purely functional, opearing on
+theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
+instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.
+INCOMPATIBILITY.
+
 * Eliminated theory ProtoPure.  Potential INCOMPATIBILITY.
 
 * Command 'setup': discontinued implicit version.
diff -r 9d1029ce0e13 -r 3a2efce3e992 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Mar 29 13:03:09 2008 +0100
+++ b/doc-src/IsarRef/pure.tex	Sat Mar 29 19:13:58 2008 +0100
@@ -81,7 +81,7 @@
   Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
   \texttt{$A$.ML} consisting of ML code that is executed in the context of the
   \emph{finished} theory $A$.  That file should not be included in the
-  $\isarkeyword{files}$ dependency declaration, though.
+  $\isarkeyword{uses}$ dependency declaration, though.
   
 \item [$\END$] concludes the current theory definition or context switch.
   Note that this command cannot be undone, but the whole theory definition has
@@ -466,16 +466,13 @@
 
 \subsection{Incorporating ML code}\label{sec:ML}
 
-\indexisarcmd{use}\indexisarcmd{ML}
-\indexisarcmd{ML-val}\indexisarcmd{ML-command}
-\indexisarcmd{ML-setup}\indexisarcmd{setup}
-\indexisarcmd{method-setup}
+\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-val}\indexisarcmd{ML-command}
+\indexisarcmd{setup}\indexisarcmd{method-setup}
 \begin{matharray}{rcl}
-  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
-  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
+  \isarcmd{use} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+  \isarcmd{ML} & : & \isarkeep{theory~|~local{\dsh}theory} \\
   \isarcmd{ML_val} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
-  \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
   \isarcmd{setup} & : & \isartrans{theory}{theory} \\
   \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
 \end{matharray}
@@ -483,29 +480,28 @@
 \begin{rail}
   'use' name
   ;
-  ('ML' | 'ML\_val' | 'ML\_command' | 'ML\_setup' | 'setup') text
+  ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
   ;
   'method\_setup' name '=' text text
   ;
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
-  The current theory context (if present) is passed down to the ML session,
-  but may not be modified.  Furthermore, the file name is checked with the
-  $\isarkeyword{files}$ dependency declaration given in the theory header (see
-  also \S\ref{sec:begin-thy}).
+\item [$\isarkeyword{use}~file$] reads and executes ML commands from
+  $file$.  The current theory context is passed down to the ML
+  toplevel and may be modified, using \verb,Context.>>, or any other
+  ML commands derived from it.  The file name is checked with the
+  $\isarkeyword{uses}$ dependency declaration given in the theory
+  header (see also \S\ref{sec:begin-thy}).
   
-\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_val}~text$ and
-  $\isarkeyword{ML_command}~text$] execute ML commands from $text$.
-  The theory context is passed in the same way as for
-  $\isarkeyword{use}$, but may not be changed.  Note that the output
-  of $\isarkeyword{ML_command}$ is less verbose than plain
-  $\isarkeyword{ML}$.
-  
-\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
-  theory context is passed down to the ML session, and fetched back
-  afterwards.  Thus $text$ may actually change the theory as a side effect.
+\item [$\isarkeyword{ML}~text$] is similar to $\isarkeyword{use}$, but
+  executes ML commands from the given $text$.
+
+\item [$\isarkeyword{ML_val}$ and $\isarkeyword{ML_command}$] are
+  diagnostic versions of $\isarkeyword{ML}$, which means that the
+  context may not be updated.  $\isarkeyword{ML_val}$ echos the
+  bindings produced at the ML toplevel, but $\isarkeyword{ML_command}$
+  is silent.
   
 \item [$\isarkeyword{setup}~text$] changes the current theory context
   by applying $text$, which refers to an ML expression of type