doc-src/IsarImplementation/Thy/integration.thy
author wenzelm
Sat, 08 Jul 2006 14:01:40 +0200
changeset 20064 92aad017b847
parent 20025 95aeaa3ef35d
child 20447 5b75f1c4d7d6
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
(* $Id$ *)
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
theory integration imports base begin
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
chapter {* System integration *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
section {* Isar toplevel *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
text {* The Isar toplevel may be considered the centeral hub of the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
  Isabelle/Isar system, where all key components and sub-systems are
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
  integrated into a single read-eval-print loop of Isar commands.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
  Here we even incorporate the existing {\ML} toplevel of the compiler
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    14
  and run-time system (cf.\ \secref{sec:ML-toplevel}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    16
  Isabelle/Isar departs from original ``LCF system architecture''
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    17
  where {\ML} was really The Meta Language for defining theories and
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    18
  conducting proofs.  Instead, {\ML} merely serves as the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    19
  implementation language for the system (and user extensions), while
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    20
  our specific Isar toplevel supports particular notions of
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    21
  incremental theory and proof development more directly.  This
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    22
  includes the graph structure of theories and the block structure of
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    23
  proofs, support for unlimited undo, facilities for tracing,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    24
  debugging, timing, profiling.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    25
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    26
  \medskip The toplevel maintains an implicit state, which is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    27
  transformed by a sequence of transitions -- either interactively or
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    28
  in batch-mode.  In interactive mode, Isar state transitions are
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    29
  encapsulated as safe transactions, such that both failure and undo
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    30
  are handled conveniently without destroying the underlying draft
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    31
  theory (cf.~\secref{sec:context-theory}).  In batch mode,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    32
  transitions operate in a strictly linear (destructive) fashion, such
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    33
  that error conditions abort the present attempt to construct a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    34
  theory altogether.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    35
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    36
  The toplevel state is a disjoint sum of empty @{text toplevel}, or
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    37
  @{text theory}, or @{text proof}.  On entering the main Isar loop we
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    38
  start with an empty toplevel.  A theory is commenced by giving a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    39
  @{text \<THEORY>} header; within a theory we may issue theory
20025
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
    40
  commands such as @{text \<DEFINITION>}, or state a @{text
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
    41
  \<THEOREM>} to be proven.  Now we are within a proof state, with a
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
    42
  rich collection of Isar proof commands for structured proof
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    43
  composition, or unstructured proof scripts.  When the proof is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    44
  concluded we get back to the theory, which is then updated by
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    45
  storing the resulting fact.  Further theory declarations or theorem
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    46
  statements with proofs may follow, until we eventually conclude the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    47
  theory development by issuing @{text \<END>}.  The resulting theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    48
  is then stored within the theory database and we are back to the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    49
  empty toplevel.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    50
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    51
  In addition to these proper state transformations, there are also
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    52
  some diagnostic commands for peeking at the toplevel state without
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    53
  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    54
  \isakeyword{print-cases}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    55
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    56
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    57
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    58
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    59
  @{index_ML_type Toplevel.state} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    60
  @{index_ML Toplevel.UNDEF: "exn"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    61
  @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    62
  @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    63
  @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    64
  @{index_ML Toplevel.debug: "bool ref"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    65
  @{index_ML Toplevel.timing: "bool ref"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    66
  @{index_ML Toplevel.profiling: "int ref"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    67
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    68
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    69
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    70
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    71
  \item @{ML_type Toplevel.state} represents Isar toplevel states,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    72
  which are normally only manipulated through the toplevel transition
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    73
  concept (\secref{sec:toplevel-transition}).  Also note that a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    74
  toplevel state is subject to the same linerarity restrictions as a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    75
  theory context (cf.~\secref{sec:context-theory}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    76
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    77
  \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    78
  operations: @{ML_type Toplevel.state} is a sum type, many operations
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    79
  work only partially for certain cases.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    80
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    81
  \item @{ML Toplevel.is_toplevel} checks for an empty toplevel state.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    82
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    83
  \item @{ML Toplevel.theory_of} gets the theory of a theory or proof
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    84
  (!), otherwise raises @{ML Toplevel.UNDEF}.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    85
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    86
  \item @{ML Toplevel.proof_of} gets the Isar proof state if
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    87
  available, otherwise raises @{ML Toplevel.UNDEF}.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    88
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    89
  \item @{ML "set Toplevel.debug"} makes the toplevel print further
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    90
  details about internal error conditions, exceptions being raised
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
  etc.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    92
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    93
  \item @{ML "set Toplevel.timing"} makes the toplevel print timing
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    94
  information for each Isar command being executed.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    95
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    96
  \item @{ML Toplevel.profiling} controls low-level profiling of the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    97
  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    98
  and 2 space profiling.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    99
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   100
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   101
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   102
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   103
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   104
subsection {* Toplevel transitions *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   105
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   106
text {* An Isar toplevel transition consists of a partial
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   107
  function on the toplevel state, with additional information for
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   108
  diagnostics and error reporting: there are fields for command name,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   109
  source position, optional source text, as well as flags for
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   110
  interactive-only commands (which issue a warning in batch-mode),
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   111
  printing of result state, etc.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   112
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   113
  The operational part is represented as a sequential union of a list
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   114
  of partial functions, which are tried in turn until the first one
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   115
  succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}).  For example,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   116
  a single Isar command like \isacommand{qed} consists of the union of
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   117
  some function @{ML_type "Proof.state -> Proof.state"} for proofs
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   118
  within proofs, plus @{ML_type "Proof.state -> theory"} for proofs at
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   119
  the outer theory level.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   120
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   121
  Toplevel transitions are composed via transition transformers.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   122
  Internally, Isar commands are put together from an empty transition
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   123
  extended by name and source position (and optional source text).  It
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   124
  is then left to the individual command parser to turn the given
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   125
  syntax body into a suitable transition transformer that adjoin
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   126
  actual operations on a theory or proof state etc.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   127
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   128
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   129
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   130
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   131
  @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   132
  @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   133
  @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   134
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   135
  @{index_ML Toplevel.theory: "(theory -> theory) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   136
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   137
  @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   138
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   139
  @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   140
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   141
  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   142
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   143
  @{index_ML Toplevel.proof_to_theory: "(Proof.state -> theory) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   144
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   145
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   146
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   147
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   148
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   149
  \item @{ML Toplevel.print} sets the print flag, which causes the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   150
  resulting state of the transition to be echoed in interactive mode.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   151
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   152
  \item @{ML Toplevel.no_timing} indicates that the transition should
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   153
  never show timing information, e.g.\ because it is merely a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   154
  diagnostic command.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   155
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   156
  \item @{ML Toplevel.keep} adjoins a diagnostic function.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   157
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   158
  \item @{ML Toplevel.theory} adjoins a theory transformer.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   159
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   160
  \item @{ML Toplevel.theory_to_proof} adjoins a global goal function,
18590
f6a553aa3d81 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents: 18563
diff changeset
   161
  which turns a theory into a proof state.  The theory may be changed
f6a553aa3d81 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents: 18563
diff changeset
   162
  before entering the proof; the generic Isar goal setup includes an
f6a553aa3d81 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents: 18563
diff changeset
   163
  argument that specifies how to apply the proven result to the
f6a553aa3d81 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents: 18563
diff changeset
   164
  theory, when the proof is finished.
18558
48d5419fd191 more stuff;
wenzelm
parents: 18554
diff changeset
   165
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   166
  \item @{ML Toplevel.proof} adjoins a deterministic proof command,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   167
  with a singleton result state.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   168
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   169
  \item @{ML Toplevel.proofs} adjoins a general proof command, with
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   170
  zero or more result states (represented as a lazy list).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   171
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   172
  \item @{ML Toplevel.proof_to_theory} adjoins a concluding proof
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   173
  command, that returns the resulting theory, after storing the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   174
  resulting facts etc.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   175
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   176
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   177
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   178
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   179
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   180
subsection {* Toplevel control *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   181
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   182
text {* Apart from regular toplevel transactions there are a few
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   183
  special control commands that modify the behavior the toplevel
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   184
  itself, and only make sense in interactive mode.  Under normal
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   185
  circumstances, the user encounters these only implicitly as part of
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   186
  the protocol between the Isabelle/Isar system and a user-interface
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   187
  such as ProofGeneral.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   188
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   189
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   190
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   191
  \item \isacommand{undo} follows the three-level hierarchy of empty
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   192
  toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   193
  previous proof context, undo after a proof reverts to the theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   194
  before the initial goal statement, undo of a theory command reverts
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   195
  to the previous theory value, undo of a theory header discontinues
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   196
  the current theory development and removes it from the theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   197
  database (\secref{sec:theory-database}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   198
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   199
  \item \isacommand{kill} aborts the current level of development:
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   200
  kill in a proof context reverts to the theory before the initial
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   201
  goal statement, kill in a theory context aborts the current theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   202
  development, removing it from the database.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   203
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   204
  \item \isacommand{exit} drops out of the Isar toplevel into the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   205
  underlying {\ML} toplevel (\secref{sec:ML-toplevel}).  The Isar
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   206
  toplevel state is preserved and may be continued later.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   207
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   208
  \item \isacommand{quit} terminates the Isabelle/Isar process without
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   209
  saving.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   210
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   211
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   212
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   213
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   214
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   215
section {* ML toplevel \label{sec:ML-toplevel} *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   216
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   217
text {* The {\ML} toplevel provides a read-compile-eval-print loop for
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   218
  {\ML} values, types, structures, and functors.  {\ML} declarations
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   219
  operate on the global system state, which consists of the compiler
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   220
  environment plus the values of {\ML} reference variables.  There is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   221
  no clean way to undo {\ML} declarations, except for reverting to a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   222
  previously saved state of the whole Isabelle process.  {\ML} input
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   223
  is either read interactively from a TTY, or from a string (usually
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   224
  within a theory text), or from a source file (usually associated
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   225
  with a theory).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   226
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   227
  Whenever the {\ML} toplevel is active, the current Isabelle theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   228
  context is passed as an internal reference variable.  Thus {\ML}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   229
  code may access the theory context during compilation, it may even
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   230
  change the value of a theory being under construction --- following
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   231
  the usual linearity restrictions (cf.~\secref{sec:context-theory}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   232
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   233
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   234
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   235
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   236
  @{index_ML context: "theory -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   237
  @{index_ML the_context: "unit -> theory"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   238
  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   239
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   240
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   241
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   242
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   243
  \item @{ML context}~@{text thy} sets the {\ML} theory context to
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   244
  @{text thy}.  This is usually performed automatically by the system,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   245
  when dropping out of the interactive Isar toplevel into {\ML}, or
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   246
  when Isar invokes {\ML} to process code from a string or a file.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   247
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   248
  \item @{ML "the_context ()"} refers to the theory context of the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   249
  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   250
  to refer to @{ML "the_context ()"} correctly, recall that evaluation
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   251
  of a function body is delayed until actual runtime.  Moreover,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   252
  persistent {\ML} toplevel bindings to an unfinished theory should be
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   253
  avoided: code should either project out the desired information
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   254
  immediately, or produce an explicit @{ML_type theory_ref} (cf.\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   255
  \secref{sec:context-theory}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   256
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   257
  \item @{ML "Context.>>"}~@{text f} applies theory transformation
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   258
  @{text f} to the current theory of the {\ML} toplevel.  In order to
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   259
  work as expected, the theory should be still under construction, and
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   260
  the Isar language element that invoked the {\ML} compiler in the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   261
  first place shoule be ready to accept the changed theory value
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   262
  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   263
  Otherwise the theory may get destroyed!
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   264
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   265
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   266
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   267
  It is very important to note that the above functions are really
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   268
  restricted to the compile time, even though the {\ML} compiler is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   269
  invoked at runtime!  The majority of {\ML} code uses explicit
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   270
  functional arguments of a theory or proof context, as required.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   271
  Thus it may get run in an arbitrary context later on.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   272
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   273
  \bigskip
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   274
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   275
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   276
  @{index_ML Isar.main: "unit -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   277
  @{index_ML Isar.loop: "unit -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   278
  @{index_ML Isar.state: "unit -> Toplevel.state"} \\
20025
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
   279
  @{index_ML Isar.context: "unit -> Proof.context"} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   280
  @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   281
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   282
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   283
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   284
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   285
  \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   286
  initializing the state to empty toplevel state.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   287
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   288
  \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   289
  current state, after dropping out of the Isar toplevel loop.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   290
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   291
  \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   292
  toplevel state and optional error condition, respectively.  This
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   293
  only works after dropping out of the Isar toplevel loop.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   294
20025
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
   295
  \item @{ML "Isar.context ()"} produces the proof context from @{ML
20064
wenzelm
parents: 20025
diff changeset
   296
  "Isar.state ()"}.
20025
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
   297
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   298
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   299
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   300
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   301
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   302
section {* Theory database *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   303
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   304
text {* The theory database maintains a collection of theories,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   305
  together with some administrative information about the original
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   306
  sources, which are held in an external store (i.e.\ a collection of
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   307
  directories within the regular file system of the underlying
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   308
  platform).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   309
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   310
  The theory database is organized as a directed acyclic graph, with
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   311
  entries referenced by theory name.  Although some external
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   312
  interfaces allow to include a directory specification, this is only
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   313
  a hint to the underlying theory loader mechanism: the internal
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   314
  theory name space is flat.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   315
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   316
  Theory @{text A} is associated with the main theory file @{text
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   317
  A}\verb,.thy,, which needs to be accessible through the theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   318
  loader path.  A number of optional {\ML} source files may be
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   319
  associated with each theory, by declaring these dependencies in the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   320
  theory header as @{text \<USES>}, and loading them consecutively
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   321
  within the theory context.  The system keeps track of incoming {\ML}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   322
  sources and associates them with the current theory.  The special
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   323
  theory {\ML} file @{text A}\verb,.ML, is loaded after a theory has
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   324
  been concluded, in order to support legacy proof {\ML} proof
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   325
  scripts.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   326
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   327
  The basic internal actions of the theory database are @{text
18554
bff7a1466fe4 more stuff;
wenzelm
parents: 18537
diff changeset
   328
  "update"}, @{text "outdate"}, and @{text "remove"}:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   329
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   330
  \begin{itemize}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   331
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   332
  \item @{text "update A"} introduces a link of @{text "A"} with a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   333
  @{text "theory"} value of the same name; it asserts that the theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   334
  sources are consistent with that value.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   335
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   336
  \item @{text "outdate A"} invalidates the link of a theory database
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   337
  entry to its sources, but retains the present theory value.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   338
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   339
  \item @{text "remove A"} removes entry @{text "A"} from the theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   340
  database.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   341
  
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   342
  \end{itemize}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   343
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   344
  These actions are propagated to sub- or super-graphs of a theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   345
  entry in the usual way, in order to preserve global consistency of
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   346
  the state of all loaded theories with the sources of the external
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   347
  store.  This implies causal dependencies of certain actions: @{text
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   348
  "update"} or @{text "outdate"} of an entry will @{text "outdate"}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   349
  all descendants; @{text "remove"} will @{text "remove"} all
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   350
  descendants.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   351
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   352
  \medskip There are separate user-level interfaces to operate on the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   353
  theory database directly or indirectly.  The primitive actions then
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   354
  just happen automatically while working with the system.  In
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   355
  particular, processing a theory header @{text "\<THEORY> A
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   356
  \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensure that the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   357
  sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   358
  is up-to-date.  Earlier theories are reloaded as required, with
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   359
  @{text update} actions proceeding in topological order according to
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   360
  theory dependencies.  There may be also a wave of implied @{text
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   361
  outdate} actions for derived theory nodes until a stable situation
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   362
  is achieved eventually.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   363
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   364
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   365
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   366
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   367
  @{index_ML theory: "string -> theory"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   368
  @{index_ML use_thy: "string -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   369
  @{index_ML update_thy: "string -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   370
  @{index_ML use_thy_only: "string -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   371
  @{index_ML update_thy_only: "string -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   372
  @{index_ML touch_thy: "string -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   373
  @{index_ML remove_thy: "string -> unit"} \\[1ex]
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   374
  @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   375
  @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   376
  @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   377
  @{verbatim "datatype action = Update | Outdate | Remove"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   378
  @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   379
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   380
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   381
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   382
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   383
  \item @{ML theory}~@{text A} retrieves the theory value presently
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   384
  associated with @{text A}.  The result is not necessarily
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   385
  up-to-date!
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   386
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   387
  \item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   388
  or out-of-date.  It ensures that all parent theories are available
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   389
  as well, but does not reload them if older versions are already
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   390
  present.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   391
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   392
  \item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   393
  the @{text A} and all of its ancestors are fully up-to-date.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   394
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   395
  \item @{ML use_thy_only}~@{text A} is like @{ML use_thy}~@{text A},
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   396
  but refrains from loading the attached @{text A}\verb,.ML, file.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   397
  This is occasionally useful in replaying legacy {\ML} proof scripts
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   398
  by hand.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   399
  
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   400
  \item @{ML update_thy_only} is analogous to @{ML use_thy_only}, but
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   401
  proceeds like @{ML update_thy} for ancestors.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   402
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   403
  \item @{ML touch_thy}~@{text A} performs @{text outdate} action on
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   404
  theory @{text A} and all of its descendants.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   405
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   406
  \item @{ML remove_thy}~@{text A} removes @{text A} and all of its
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   407
  descendants from the theory database.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   408
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   409
  \item @{ML ThyInfo.begin_theory} is the basic operation behind a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   410
  @{text \<THEORY>} header declaration.  The boolean argument
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   411
  indicates the strictness of treating ancestors: for @{ML true} (as
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   412
  in interactive mode) like @{ML update_thy}, and for @{ML false} (as
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   413
  in batch mode) like @{ML use_thy}.  This is {\ML} functions is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   414
  normally not invoked directly.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   415
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   416
  \item @{ML ThyInfo.end_theory} concludes the loading of a theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   417
  proper; an attached theory {\ML} file may be still loaded later on.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   418
  This is {\ML} functions is normally not invoked directly.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   419
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   420
  \item @{ML ThyInfo.register_theory}~{text thy} registers an existing
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   421
  theory value with the theory loader database.  There is no
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   422
  management of associated sources; this is mainly for bootstrapping.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   423
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   424
  \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   425
  f} as a hook for theory database actions.  The function will be
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   426
  invoked with the action and theory name being involved; thus derived
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   427
  actions may be performed in associated system components, e.g.\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   428
  maintaining the state of an editor for theory sources.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   429
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   430
  The kind and order of actions occurring in practice depends both on
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   431
  user interactions and the internal process of resolving theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   432
  imports.  Hooks should not rely on a particular policy here!  Any
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   433
  exceptions raised by the hook are ignored by the theory database.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   434
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   435
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   436
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   437
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   438
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   439
(* FIXME section {* Sessions and document preparation *} *)
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   440
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   441
end