changeset 51659:5151706dc9a6

more accurate documentation;
author wenzelm
date Tue, 09 Apr 2013 15:37:23 +0200
parents 21c10672633b
children 8e0a1d0a41ff
files src/Doc/IsarImplementation/Integration.thy
diffstat 1 Dateien verändert, 4 Zeilen hinzugefügt(+), 3 Zeilen entfernt(-) [+]
line wrap: on
line diff
--- 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.