--- a/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 27 23:01:42 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 27 23:02:45 2010 +0200
@@ -322,7 +322,7 @@
sources and associates them with the current theory.
The basic internal actions of the theory database are @{text
- "update"}, @{text "outdate"}, and @{text "remove"}:
+ "update"} and @{text "remove"}:
\begin{itemize}
@@ -330,9 +330,6 @@
@{text "theory"} value of the same name; it asserts that the theory
sources are now consistent with that value;
- \item @{text "outdate A"} invalidates the link of a theory database
- entry to its sources, but retains the present theory value;
-
\item @{text "remove A"} deletes entry @{text "A"} from the theory
database.
@@ -342,8 +339,8 @@
entry as expected, in order to preserve global consistency of the
state of all loaded theories with the sources of the external store.
This implies certain causalities between actions: @{text "update"}
- or @{text "outdate"} of an entry will @{text "outdate"} all
- descendants; @{text "remove"} will @{text "remove"} all descendants.
+ or @{text "remove"} of an entry will @{text "remove"} all
+ descendants.
\medskip There are separate user-level interfaces to operate on the
theory database directly or indirectly. The primitive actions then
@@ -354,7 +351,7 @@
is up-to-date, too. Earlier theories are reloaded as required, with
@{text update} actions proceeding in topological order according to
theory dependencies. There may be also a wave of implied @{text
- outdate} actions for derived theory nodes until a stable situation
+ remove} actions for derived theory nodes until a stable situation
is achieved eventually.
*}
@@ -363,12 +360,9 @@
@{index_ML use_thy: "string -> unit"} \\
@{index_ML use_thys: "string list -> unit"} \\
@{index_ML Thy_Info.get_theory: "string -> theory"} \\
- @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
- @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
- @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
- @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]
- @{verbatim "datatype action = Update | Outdate | Remove"} \\
+ @{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]
+ @{verbatim "datatype action = Update | Remove"} \\
@{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
\end{mldecls}
@@ -390,22 +384,13 @@
presently associated with name @{text A}. Note that the result
might be outdated.
- \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
- on theory @{text A} and all descendants.
-
\item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
descendants from the theory database.
- \item @{ML Thy_Info.begin_theory} is the basic operation behind a
- @{text \<THEORY>} header declaration. This {\ML} function is
- normally not invoked directly.
-
- \item @{ML Thy_Info.end_theory} concludes the loading of a theory
- proper and stores the result in the theory database.
-
- \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an
- existing theory value with the theory loader database. There is no
- management of associated sources.
+ \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an
+ existing theory value with the theory loader database and updates
+ source version information according to the current file-system
+ state.
\item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
f} as a hook for theory database actions. The function will be
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jul 27 23:01:42 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jul 27 23:02:45 2010 +0200
@@ -390,7 +390,7 @@
within the theory context. The system keeps track of incoming {\ML}
sources and associates them with the current theory.
- The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
+ The basic internal actions of the theory database are \isa{update} and \isa{remove}:
\begin{itemize}
@@ -398,9 +398,6 @@
\isa{theory} value of the same name; it asserts that the theory
sources are now consistent with that value;
- \item \isa{outdate\ A} invalidates the link of a theory database
- entry to its sources, but retains the present theory value;
-
\item \isa{remove\ A} deletes entry \isa{A} from the theory
database.
@@ -410,8 +407,8 @@
entry as expected, in order to preserve global consistency of the
state of all loaded theories with the sources of the external store.
This implies certain causalities between actions: \isa{update}
- or \isa{outdate} of an entry will \isa{outdate} all
- descendants; \isa{remove} will \isa{remove} all descendants.
+ or \isa{remove} of an entry will \isa{remove} all
+ descendants.
\medskip There are separate user-level interfaces to operate on the
theory database directly or indirectly. The primitive actions then
@@ -420,7 +417,7 @@
sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
is up-to-date, too. Earlier theories are reloaded as required, with
\isa{update} actions proceeding in topological order according to
- theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
+ theory dependencies. There may be also a wave of implied \isa{remove} actions for derived theory nodes until a stable situation
is achieved eventually.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -436,12 +433,9 @@
\indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
\indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
\indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\
- \indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
\indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
- \indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
- \indexdef{}{ML}{Thy\_Info.end\_theory}\verb|Thy_Info.end_theory: theory -> unit| \\
- \indexdef{}{ML}{Thy\_Info.register\_theory}\verb|Thy_Info.register_theory: theory -> unit| \\[1ex]
- \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
+ \indexdef{}{ML}{Thy\_Info.register\_thy}\verb|Thy_Info.register_thy: theory -> unit| \\[1ex]
+ \verb|datatype action = Update |\verb,|,\verb| Remove| \\
\indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
\end{mldecls}
@@ -462,22 +456,13 @@
presently associated with name \isa{A}. Note that the result
might be outdated.
- \item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
- on theory \isa{A} and all descendants.
-
\item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
descendants from the theory database.
- \item \verb|Thy_Info.begin_theory| is the basic operation behind a
- \isa{{\isasymTHEORY}} header declaration. This {\ML} function is
- normally not invoked directly.
-
- \item \verb|Thy_Info.end_theory| concludes the loading of a theory
- proper and stores the result in the theory database.
-
- \item \verb|Thy_Info.register_theory|~\isa{text\ thy} registers an
- existing theory value with the theory loader database. There is no
- management of associated sources.
+ \item \verb|Thy_Info.register_thy|~\isa{text\ thy} registers an
+ existing theory value with the theory loader database and updates
+ source version information according to the current file-system
+ state.
\item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
invoked with the action and theory name being involved; thus derived
--- a/doc-src/antiquote_setup.ML Tue Jul 27 23:01:42 2010 +0200
+++ b/doc-src/antiquote_setup.ML Tue Jul 27 23:02:45 2010 +0200
@@ -181,7 +181,7 @@
val _ = entity_antiqs no_check "isatt" "executable";
val _ = entity_antiqs (K check_tool) "isatt" "tool";
val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
-val _ = entity_antiqs (K Thy_Info.known_thy) "" "theory";
+val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
end;
--- a/doc-src/rail.ML Tue Jul 27 23:01:42 2010 +0200
+++ b/doc-src/rail.ML Tue Jul 27 23:02:45 2010 +0200
@@ -74,7 +74,7 @@
("executable", ("isatt", no_check, true)),
("tool", ("isatt", K check_tool, true)),
("file", ("isatt", K (File.exists o Path.explode), true)),
- ("theory", ("", K Thy_Info.known_thy, true))
+ ("theory", ("", K (can Thy_Info.get_theory), true))
];
in