1.1 --- a/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 27 23:01:42 2010 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 27 23:02:45 2010 +0200
1.3 @@ -322,7 +322,7 @@
1.4 sources and associates them with the current theory.
1.5
1.6 The basic internal actions of the theory database are @{text
1.7 - "update"}, @{text "outdate"}, and @{text "remove"}:
1.8 + "update"} and @{text "remove"}:
1.9
1.10 \begin{itemize}
1.11
1.12 @@ -330,9 +330,6 @@
1.13 @{text "theory"} value of the same name; it asserts that the theory
1.14 sources are now consistent with that value;
1.15
1.16 - \item @{text "outdate A"} invalidates the link of a theory database
1.17 - entry to its sources, but retains the present theory value;
1.18 -
1.19 \item @{text "remove A"} deletes entry @{text "A"} from the theory
1.20 database.
1.21
1.22 @@ -342,8 +339,8 @@
1.23 entry as expected, in order to preserve global consistency of the
1.24 state of all loaded theories with the sources of the external store.
1.25 This implies certain causalities between actions: @{text "update"}
1.26 - or @{text "outdate"} of an entry will @{text "outdate"} all
1.27 - descendants; @{text "remove"} will @{text "remove"} all descendants.
1.28 + or @{text "remove"} of an entry will @{text "remove"} all
1.29 + descendants.
1.30
1.31 \medskip There are separate user-level interfaces to operate on the
1.32 theory database directly or indirectly. The primitive actions then
1.33 @@ -354,7 +351,7 @@
1.34 is up-to-date, too. Earlier theories are reloaded as required, with
1.35 @{text update} actions proceeding in topological order according to
1.36 theory dependencies. There may be also a wave of implied @{text
1.37 - outdate} actions for derived theory nodes until a stable situation
1.38 + remove} actions for derived theory nodes until a stable situation
1.39 is achieved eventually.
1.40 *}
1.41
1.42 @@ -363,12 +360,9 @@
1.43 @{index_ML use_thy: "string -> unit"} \\
1.44 @{index_ML use_thys: "string list -> unit"} \\
1.45 @{index_ML Thy_Info.get_theory: "string -> theory"} \\
1.46 - @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
1.47 @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
1.48 - @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
1.49 - @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
1.50 - @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]
1.51 - @{verbatim "datatype action = Update | Outdate | Remove"} \\
1.52 + @{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]
1.53 + @{verbatim "datatype action = Update | Remove"} \\
1.54 @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
1.55 \end{mldecls}
1.56
1.57 @@ -390,22 +384,13 @@
1.58 presently associated with name @{text A}. Note that the result
1.59 might be outdated.
1.60
1.61 - \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
1.62 - on theory @{text A} and all descendants.
1.63 -
1.64 \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
1.65 descendants from the theory database.
1.66
1.67 - \item @{ML Thy_Info.begin_theory} is the basic operation behind a
1.68 - @{text \<THEORY>} header declaration. This {\ML} function is
1.69 - normally not invoked directly.
1.70 -
1.71 - \item @{ML Thy_Info.end_theory} concludes the loading of a theory
1.72 - proper and stores the result in the theory database.
1.73 -
1.74 - \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an
1.75 - existing theory value with the theory loader database. There is no
1.76 - management of associated sources.
1.77 + \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an
1.78 + existing theory value with the theory loader database and updates
1.79 + source version information according to the current file-system
1.80 + state.
1.81
1.82 \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
1.83 f} as a hook for theory database actions. The function will be
2.1 --- a/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jul 27 23:01:42 2010 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Tue Jul 27 23:02:45 2010 +0200
2.3 @@ -390,7 +390,7 @@
2.4 within the theory context. The system keeps track of incoming {\ML}
2.5 sources and associates them with the current theory.
2.6
2.7 - The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
2.8 + The basic internal actions of the theory database are \isa{update} and \isa{remove}:
2.9
2.10 \begin{itemize}
2.11
2.12 @@ -398,9 +398,6 @@
2.13 \isa{theory} value of the same name; it asserts that the theory
2.14 sources are now consistent with that value;
2.15
2.16 - \item \isa{outdate\ A} invalidates the link of a theory database
2.17 - entry to its sources, but retains the present theory value;
2.18 -
2.19 \item \isa{remove\ A} deletes entry \isa{A} from the theory
2.20 database.
2.21
2.22 @@ -410,8 +407,8 @@
2.23 entry as expected, in order to preserve global consistency of the
2.24 state of all loaded theories with the sources of the external store.
2.25 This implies certain causalities between actions: \isa{update}
2.26 - or \isa{outdate} of an entry will \isa{outdate} all
2.27 - descendants; \isa{remove} will \isa{remove} all descendants.
2.28 + or \isa{remove} of an entry will \isa{remove} all
2.29 + descendants.
2.30
2.31 \medskip There are separate user-level interfaces to operate on the
2.32 theory database directly or indirectly. The primitive actions then
2.33 @@ -420,7 +417,7 @@
2.34 sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
2.35 is up-to-date, too. Earlier theories are reloaded as required, with
2.36 \isa{update} actions proceeding in topological order according to
2.37 - theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
2.38 + theory dependencies. There may be also a wave of implied \isa{remove} actions for derived theory nodes until a stable situation
2.39 is achieved eventually.%
2.40 \end{isamarkuptext}%
2.41 \isamarkuptrue%
2.42 @@ -436,12 +433,9 @@
2.43 \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
2.44 \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
2.45 \indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\
2.46 - \indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
2.47 \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
2.48 - \indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
2.49 - \indexdef{}{ML}{Thy\_Info.end\_theory}\verb|Thy_Info.end_theory: theory -> unit| \\
2.50 - \indexdef{}{ML}{Thy\_Info.register\_theory}\verb|Thy_Info.register_theory: theory -> unit| \\[1ex]
2.51 - \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
2.52 + \indexdef{}{ML}{Thy\_Info.register\_thy}\verb|Thy_Info.register_thy: theory -> unit| \\[1ex]
2.53 + \verb|datatype action = Update |\verb,|,\verb| Remove| \\
2.54 \indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
2.55 \end{mldecls}
2.56
2.57 @@ -462,22 +456,13 @@
2.58 presently associated with name \isa{A}. Note that the result
2.59 might be outdated.
2.60
2.61 - \item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
2.62 - on theory \isa{A} and all descendants.
2.63 -
2.64 \item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
2.65 descendants from the theory database.
2.66
2.67 - \item \verb|Thy_Info.begin_theory| is the basic operation behind a
2.68 - \isa{{\isasymTHEORY}} header declaration. This {\ML} function is
2.69 - normally not invoked directly.
2.70 -
2.71 - \item \verb|Thy_Info.end_theory| concludes the loading of a theory
2.72 - proper and stores the result in the theory database.
2.73 -
2.74 - \item \verb|Thy_Info.register_theory|~\isa{text\ thy} registers an
2.75 - existing theory value with the theory loader database. There is no
2.76 - management of associated sources.
2.77 + \item \verb|Thy_Info.register_thy|~\isa{text\ thy} registers an
2.78 + existing theory value with the theory loader database and updates
2.79 + source version information according to the current file-system
2.80 + state.
2.81
2.82 \item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
2.83 invoked with the action and theory name being involved; thus derived
3.1 --- a/doc-src/antiquote_setup.ML Tue Jul 27 23:01:42 2010 +0200
3.2 +++ b/doc-src/antiquote_setup.ML Tue Jul 27 23:02:45 2010 +0200
3.3 @@ -181,7 +181,7 @@
3.4 val _ = entity_antiqs no_check "isatt" "executable";
3.5 val _ = entity_antiqs (K check_tool) "isatt" "tool";
3.6 val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
3.7 -val _ = entity_antiqs (K Thy_Info.known_thy) "" "theory";
3.8 +val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
3.9
3.10 end;
3.11
4.1 --- a/doc-src/rail.ML Tue Jul 27 23:01:42 2010 +0200
4.2 +++ b/doc-src/rail.ML Tue Jul 27 23:02:45 2010 +0200
4.3 @@ -74,7 +74,7 @@
4.4 ("executable", ("isatt", no_check, true)),
4.5 ("tool", ("isatt", K check_tool, true)),
4.6 ("file", ("isatt", K (File.exists o Path.explode), true)),
4.7 - ("theory", ("", K Thy_Info.known_thy, true))
4.8 + ("theory", ("", K (can Thy_Info.get_theory), true))
4.9 ];
4.10
4.11 in