doc-src/IsarImplementation/Thy/unused.thy
changeset 18537 2681f9e34390
child 20429 116255c9209b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy	Mon Jan 02 20:16:52 2006 +0100
     1.3 @@ -0,0 +1,16 @@
     1.4 +
     1.5 +text {*
     1.6 +  The Isar toplevel works differently for interactive developments
     1.7 +  vs.\ batch processing of theory sources.  For example, diagnostic
     1.8 +  commands produce a warning batch mode, because they are considered
     1.9 +  alien to the final theory document being produced eventually.
    1.10 +  Moreover, full @{text undo} with intermediate checkpoints to protect
    1.11 +  against destroying theories accidentally are limited to interactive
    1.12 +  mode.  In batch mode there is only a single strictly linear stream
    1.13 +  of potentially desctructive theory transformations.
    1.14 +*}
    1.15 +
    1.16 +  \item @{ML Toplevel.empty} is an empty transition; the Isar command
    1.17 +  dispatcher internally applies @{ML Toplevel.name} (for the command)
    1.18 +  name and @{ML Toplevel.position} for the source position.
    1.19 +