# HG changeset patch
# User wenzelm
# Date 1365514643 -7200
# Node ID 5151706dc9a6bd4425b5beddeff3109641a39277
# Parent  21c10672633b9096002c1ca949615bfddbbab5f6
more accurate documentation;

diff -r 21c10672633b -r 5151706dc9a6 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 15:29:25 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 15:37:23 2013 +0200
@@ -85,9 +85,10 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "Toplevel.debug := true"} makes the toplevel print further
-  details about internal error conditions, exceptions being raised
-  etc.
+  \item @{ML "Toplevel.debug := true"} enables low-level exception
+  trace of the ML runtime system.  Note that the result might appear
+  on some raw output window only, outside the formal context of the
+  source text.
 
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.