doc-src/IsarImplementation/Thy/unused.thy
author wenzelm
Mon Jan 02 20:16:52 2006 +0100 (2006-01-02 ago)
changeset 18537 2681f9e34390
child 20429 116255c9209b
permissions -rw-r--r--
"The Isabelle/Isar Implementation" manual;
     1 
     2 text {*
     3   The Isar toplevel works differently for interactive developments
     4   vs.\ batch processing of theory sources.  For example, diagnostic
     5   commands produce a warning batch mode, because they are considered
     6   alien to the final theory document being produced eventually.
     7   Moreover, full @{text undo} with intermediate checkpoints to protect
     8   against destroying theories accidentally are limited to interactive
     9   mode.  In batch mode there is only a single strictly linear stream
    10   of potentially desctructive theory transformations.
    11 *}
    12 
    13   \item @{ML Toplevel.empty} is an empty transition; the Isar command
    14   dispatcher internally applies @{ML Toplevel.name} (for the command)
    15   name and @{ML Toplevel.position} for the source position.
    16