--- a/doc-src/IsarImplementation/Thy/document/integration.tex Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Mon Sep 04 20:07:55 2006 +0200
@@ -150,10 +150,10 @@
The operational part is represented as the sequential union of a
list of partial functions, which are tried in turn until the first
- one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|). This acts
- like an outer case-expression for various alternative state
- transitions. For example, \isakeyword{qed} acts differently for a
- local proofs vs.\ the global ending of the main proof.
+ one succeeds. This acts like an outer case-expression for various
+ alternative state transitions. For example, \isakeyword{qed} acts
+ differently for a local proofs vs.\ the global ending of the main
+ proof.
Toplevel transitions are composed via transition transformers.
Internally, Isar commands are put together from an empty transition
@@ -274,9 +274,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The {\ML} toplevel provides a read-compile-eval-print loop for
- {\ML} values, types, structures, and functors. {\ML} declarations
- operate on the global system state, which consists of the compiler
+The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
+ values, types, structures, and functors. {\ML} declarations operate
+ on the global system state, which consists of the compiler
environment plus the values of {\ML} reference variables. There is
no clean way to undo {\ML} declarations, except for reverting to a
previously saved state of the whole Isabelle process. {\ML} input
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Mon Sep 04 20:07:55 2006 +0200
@@ -477,6 +477,12 @@
}
\isamarkuptrue%
%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
\begin{isamarkuptext}%
FIXME tune
@@ -511,10 +517,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
\isamarkupsubsection{Strings of symbols%
}
\isamarkuptrue%
%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
\begin{isamarkuptext}%
FIXME tune
@@ -565,6 +584,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
\isadelimmlref
%
\endisadelimmlref
@@ -620,6 +646,12 @@
}
\isamarkuptrue%
%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
\begin{isamarkuptext}%
FIXME tune
@@ -642,6 +674,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
\isadelimmlref
%
\endisadelimmlref
--- a/doc-src/IsarImplementation/Thy/integration.thy Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy Mon Sep 04 20:07:55 2006 +0200
@@ -114,10 +114,10 @@
The operational part is represented as the sequential union of a
list of partial functions, which are tried in turn until the first
- one succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}). This acts
- like an outer case-expression for various alternative state
- transitions. For example, \isakeyword{qed} acts differently for a
- local proofs vs.\ the global ending of the main proof.
+ one succeeds. This acts like an outer case-expression for various
+ alternative state transitions. For example, \isakeyword{qed} acts
+ differently for a local proofs vs.\ the global ending of the main
+ proof.
Toplevel transitions are composed via transition transformers.
Internally, Isar commands are put together from an empty transition
@@ -219,9 +219,10 @@
section {* ML toplevel \label{sec:ML-toplevel} *}
-text {* The {\ML} toplevel provides a read-compile-eval-print loop for
- {\ML} values, types, structures, and functors. {\ML} declarations
- operate on the global system state, which consists of the compiler
+text {*
+ The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
+ values, types, structures, and functors. {\ML} declarations operate
+ on the global system state, which consists of the compiler
environment plus the values of {\ML} reference variables. There is
no clean way to undo {\ML} declarations, except for reverting to a
previously saved state of the whole Isabelle process. {\ML} input
--- a/doc-src/IsarImplementation/Thy/prelim.thy Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Mon Sep 04 20:07:55 2006 +0200
@@ -405,7 +405,7 @@
section {* Name spaces *}
-text {*
+text %FIXME {*
FIXME tune
By general convention, each kind of formal entities (logical
@@ -444,7 +444,7 @@
subsection {* Strings of symbols *}
-text {*
+text %FIXME {*
FIXME tune
Isabelle strings consist of a sequence of
@@ -542,7 +542,7 @@
subsection {* Qualified names *}
-text {*
+text %FIXME {*
FIXME tune
A \emph{qualified name} essentially consists of a non-empty list of
--- a/doc-src/IsarImplementation/implementation.tex Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Mon Sep 04 20:07:55 2006 +0200
@@ -18,7 +18,9 @@
\\[4ex] The Isabelle/Isar Implementation}
\author{\emph{Makarius Wenzel}}
-\makeglossary
+%FIXME
+%\makeglossary
+
\makeindex
@@ -78,8 +80,9 @@
\bibliography{../manual}
\endgroup
-\tocentry{\glossaryname}
-\printglossary
+%FIXME
+%\tocentry{\glossaryname}
+%\printglossary
\tocentry{\indexname}
\printindex