# HG changeset patch # User wenzelm # Date 1280264565 -7200 # Node ID 111ce96515641731285378ff65eac3ffdd86c311 # Parent 9a15982f41fe282603edb7857d43b7b3d141ad96 updated manual concerning theory loader; diff -r 9a15982f41fe -r 111ce9651564 doc-src/IsarImplementation/Thy/Integration.thy --- 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 \} 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 diff -r 9a15982f41fe -r 111ce9651564 doc-src/IsarImplementation/Thy/document/Integration.tex --- 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 diff -r 9a15982f41fe -r 111ce9651564 doc-src/antiquote_setup.ML --- 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; diff -r 9a15982f41fe -r 111ce9651564 doc-src/rail.ML --- 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