--- a/Admin/isatest/isatest-statistics Tue Jul 27 20:16:14 2010 +0200
+++ b/Admin/isatest/isatest-statistics Wed Jul 28 11:42:48 2010 +0200
@@ -51,7 +51,7 @@
SESSIONS="$@"
case "$PLATFORM" in
- *para* | *-M*)
+ *para* | *-M* | afp)
PARALLEL=true
;;
*)
--- a/Admin/isatest/isatest-stats Tue Jul 27 20:16:14 2010 +0200
+++ b/Admin/isatest/isatest-stats Wed Jul 28 11:42:48 2010 +0200
@@ -6,20 +6,21 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
+PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
ISABELLE_SESSIONS="\
HOL-Plain \
HOL-Main \
HOL \
HOL-Proofs \
+ HOL-Library \
HOL-Algebra \
HOL-Auth \
HOL-Bali \
HOL-Decision_Procs \
HOL-Hoare \
HOL-Hoare_Parallel \
- HOL-Library \
+ HOL-Imperative_HOL \
HOL-Metis_Examples \
HOL-MicroJava \
HOL-Multivariate_Analysis \
@@ -27,11 +28,13 @@
HOL-Nominal-Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
+ HOL-Predicate_Compile_Examples \
HOL-Proofs-Extraction \
HOL-Proofs-Lambda \
HOL-SET_Protocol \
HOL-UNITY \
HOL-Word \
+ HOL-Word-SMT_Examples \
HOL-ex \
HOLCF \
IOA \
@@ -40,17 +43,23 @@
ZF-UNITY"
AFP_SESSIONS="\
+ Coinductive \
CoreC++ \
- Jinja-Slicing \
+ Group-Ring-Module \
+ Group-Ring-Module-Valuation \
HOL-BytecodeLogicJmlTypes \
+ HOL-Collections \
HOL-DiskPaxos \
+ HOL-FeatherweightJava \
HOL-Fermat3_4 \
HOL-Flyspeck-Tame \
- HOL-Group-Ring-Module \
- HOL-Jinja \
- HOL-JinjaThreads \
+ HOL-Free-Groups \
+ HOL-GraphMarkingIBP \
HOL-JiveDataStoreModel \
+ HOL-Locally-Nameless-Sigma \
+ HOL-Ordinals_and_Cardinals \
HOL-POPLmark-deBruijn \
+ HOL-Presburger-Automata \
HOL-Program-Conflict-Analysis \
HOL-RSAPSS \
HOL-Recursion-Theory-I \
@@ -59,10 +68,17 @@
HOL-SenSocialChoice \
HOL-SumSquares \
HOL-Topology \
- HOL-Valuation \
+ HOL-Tree-Automata \
+ HOL-Word-JinjaThreads \
+ HOLCF-WorkerWrapper \
+ HRB-Slicing \
+ Jinja \
+ Jinja-Slicing \
LinearQuantifierElim \
Simpl \
- Simpl-BDD"
+ Simpl-BDD \
+ Slicing \
+ Slicing-InformationFlowSlicing"
for PLATFORM in $PLATFORMS
do
--- a/doc-src/IsarImplementation/Thy/Integration.thy Tue Jul 27 20:16:14 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Wed Jul 28 11:42:48 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 20:16:14 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Wed Jul 28 11:42:48 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 20:16:14 2010 +0200
+++ b/doc-src/antiquote_setup.ML Wed Jul 28 11:42:48 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 20:16:14 2010 +0200
+++ b/doc-src/rail.ML Wed Jul 28 11:42:48 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
--- a/etc/isar-keywords-ZF.el Tue Jul 27 20:16:14 2010 +0200
+++ b/etc/isar-keywords-ZF.el Wed Jul 28 11:42:48 2010 +0200
@@ -190,7 +190,6 @@
"thm_deps"
"thus"
"thy_deps"
- "touch_thy"
"translations"
"txt"
"txt_raw"
@@ -270,13 +269,18 @@
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
"cannot_undo"
+ "disable_pr"
+ "enable_pr"
"exit"
"init_toplevel"
"kill"
+ "kill_thy"
"linear_undo"
"quit"
+ "remove_thy"
"undo"
- "undos_proof"))
+ "undos_proof"
+ "use_thy"))
(defconst isar-keywords-diag
'("ML_command"
@@ -285,15 +289,12 @@
"cd"
"class_deps"
"commit"
- "disable_pr"
"display_drafts"
- "enable_pr"
"find_consts"
"find_theorems"
"full_prf"
"header"
"help"
- "kill_thy"
"pr"
"pretty_setmargin"
"prf"
@@ -325,15 +326,12 @@
"print_trans_rules"
"prop"
"pwd"
- "remove_thy"
"term"
"thm"
"thm_deps"
"thy_deps"
- "touch_thy"
"typ"
"unused_thms"
- "use_thy"
"welcome"))
(defconst isar-keywords-theory-begin
--- a/etc/isar-keywords.el Tue Jul 27 20:16:14 2010 +0200
+++ b/etc/isar-keywords.el Wed Jul 28 11:42:48 2010 +0200
@@ -250,7 +250,6 @@
"thm_deps"
"thus"
"thy_deps"
- "touch_thy"
"translations"
"txt"
"txt_raw"
@@ -334,13 +333,18 @@
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
"cannot_undo"
+ "disable_pr"
+ "enable_pr"
"exit"
"init_toplevel"
"kill"
+ "kill_thy"
"linear_undo"
"quit"
+ "remove_thy"
"undo"
- "undos_proof"))
+ "undos_proof"
+ "use_thy"))
(defconst isar-keywords-diag
'("ML_command"
@@ -352,16 +356,13 @@
"code_deps"
"code_thms"
"commit"
- "disable_pr"
"display_drafts"
- "enable_pr"
"export_code"
"find_consts"
"find_theorems"
"full_prf"
"header"
"help"
- "kill_thy"
"nitpick"
"normal_form"
"pr"
@@ -401,17 +402,14 @@
"pwd"
"quickcheck"
"refute"
- "remove_thy"
"sledgehammer"
"smt_status"
"term"
"thm"
"thm_deps"
"thy_deps"
- "touch_thy"
"typ"
"unused_thms"
- "use_thy"
"value"
"values"
"welcome"))
--- a/src/HOL/Groups.thy Tue Jul 27 20:16:14 2010 +0200
+++ b/src/HOL/Groups.thy Wed Jul 28 11:42:48 2010 +0200
@@ -6,7 +6,7 @@
theory Groups
imports Orderings
-uses ("~~/src/HOL/Tools/abel_cancel.ML")
+uses ("Tools/abel_cancel.ML")
begin
subsection {* Fact collections *}
@@ -802,7 +802,7 @@
end
-use "~~/src/HOL/Tools/abel_cancel.ML"
+use "Tools/abel_cancel.ML"
simproc_setup abel_cancel_sum
("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
--- a/src/HOL/Quotient.thy Tue Jul 27 20:16:14 2010 +0200
+++ b/src/HOL/Quotient.thy Wed Jul 28 11:42:48 2010 +0200
@@ -7,11 +7,11 @@
theory Quotient
imports Plain Sledgehammer
uses
- ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
- ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
- ("~~/src/HOL/Tools/Quotient/quotient_def.ML")
- ("~~/src/HOL/Tools/Quotient/quotient_term.ML")
- ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML")
+ ("Tools/Quotient/quotient_info.ML")
+ ("Tools/Quotient/quotient_typ.ML")
+ ("Tools/Quotient/quotient_def.ML")
+ ("Tools/Quotient/quotient_term.ML")
+ ("Tools/Quotient/quotient_tacs.ML")
begin
@@ -708,7 +708,7 @@
text {* Auxiliary data for the quotient package *}
-use "~~/src/HOL/Tools/Quotient/quotient_info.ML"
+use "Tools/Quotient/quotient_info.ML"
declare [[map "fun" = (fun_map, fun_rel)]]
@@ -728,15 +728,15 @@
eq_comp_r
text {* Translation functions for the lifting process. *}
-use "~~/src/HOL/Tools/Quotient/quotient_term.ML"
+use "Tools/Quotient/quotient_term.ML"
text {* Definitions of the quotient types. *}
-use "~~/src/HOL/Tools/Quotient/quotient_typ.ML"
+use "Tools/Quotient/quotient_typ.ML"
text {* Definitions for quotient constants. *}
-use "~~/src/HOL/Tools/Quotient/quotient_def.ML"
+use "Tools/Quotient/quotient_def.ML"
text {*
@@ -759,7 +759,7 @@
text {* Tactics for proving the lifted theorems *}
-use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
+use "Tools/Quotient/quotient_tacs.ML"
subsection {* Methods / Interface *}
--- a/src/Pure/General/secure.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/General/secure.ML Wed Jul 28 11:42:48 2010 +0200
@@ -57,7 +57,7 @@
fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
fun Isar_setup () = use_global "open Unsynchronized;";
-fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
+fun PG_setup () = use_global "structure ThyLoad = ProofGeneral.ThyLoad;";
(* shell commands *)
--- a/src/Pure/Isar/isar_cmd.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jul 28 11:42:48 2010 +0200
@@ -34,10 +34,6 @@
val immediate_proof: Toplevel.transition -> Toplevel.transition
val done_proof: Toplevel.transition -> Toplevel.transition
val skip_proof: Toplevel.transition -> Toplevel.transition
- val init_theory: string * string list * (string * bool) list ->
- Toplevel.transition -> Toplevel.transition
- val exit: Toplevel.transition -> Toplevel.transition
- val quit: Toplevel.transition -> Toplevel.transition
val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
val disable_pr: Toplevel.transition -> Toplevel.transition
val enable_pr: Toplevel.transition -> Toplevel.transition
@@ -271,19 +267,6 @@
val skip_proof = local_skip_proof o global_skip_proof;
-(* init and exit *)
-
-fun init_theory (name, imports, uses) =
- Toplevel.init_theory name
- (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses));
-
-val exit = Toplevel.keep (fn state =>
- (Context.set_thread_data (try Toplevel.generic_theory_of state);
- raise Toplevel.TERMINATE));
-
-val quit = Toplevel.imperative quit;
-
-
(* print state *)
fun set_limit _ NONE = ()
--- a/src/Pure/Isar/isar_syn.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jul 28 11:42:48 2010 +0200
@@ -28,7 +28,10 @@
val _ =
Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
- (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
+ (Thy_Header.args >> (fn (name, imports, uses) =>
+ Toplevel.print o
+ Toplevel.init_theory name
+ (fn () => Thy_Info.toplevel_begin_theory name imports (map (apfst Path.explode) uses))));
val _ =
Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
@@ -944,23 +947,18 @@
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
val _ =
- Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
+ Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
(Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
val _ =
- Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
- (Parse.name >> (fn name =>
- Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.touch_thy name)));
-
-val _ =
- Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
+ Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
(Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
val _ =
Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
- Keyword.diag (Parse.name >> (fn name =>
+ Keyword.control (Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
val _ =
@@ -979,11 +977,11 @@
(opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
val _ =
- Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
+ Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
val _ =
- Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
+ Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
val _ =
@@ -992,11 +990,14 @@
val _ =
Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
- (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
+ (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
val _ =
Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
- (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
+ (Scan.succeed
+ (Toplevel.no_timing o Toplevel.keep (fn state =>
+ (Context.set_thread_data (try Toplevel.generic_theory_of state);
+ raise Toplevel.TERMINATE))));
end;
--- a/src/Pure/Isar/outer_syntax.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 28 11:42:48 2010 +0200
@@ -31,7 +31,7 @@
type isar
val isar: bool -> isar
val prepare_command: Position.T -> string -> Toplevel.transition
- val load_thy: string -> Position.T -> string -> (unit -> unit) * theory
+ val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -249,9 +249,9 @@
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_unit commands (cmd, proof, proper_proof) =
+fun prepare_unit commands init (cmd, proof, proper_proof) =
let
- val (tr, proper_cmd) = prepare_span commands cmd;
+ val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
in
if proper_cmd andalso proper_proof then [(tr, proof_trs)]
@@ -268,7 +268,7 @@
(* load_thy *)
-fun load_thy name pos text =
+fun load_thy name init pos text =
let
val (lexs, commands) = get_syntax ();
val time = ! Output.timing;
@@ -279,7 +279,7 @@
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val _ = List.app Thy_Syntax.report_span spans;
val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
- |> Par_List.map (prepare_unit commands) |> flat;
+ |> Par_List.map (prepare_unit commands init) |> flat;
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
--- a/src/Pure/Isar/toplevel.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jul 28 11:42:48 2010 +0200
@@ -46,7 +46,8 @@
val interactive: bool -> transition -> transition
val print: transition -> transition
val no_timing: transition -> transition
- val init_theory: string -> (bool -> theory) -> transition -> transition
+ val init_theory: string -> (unit -> theory) -> transition -> transition
+ val modify_init: (unit -> theory) -> transition -> transition
val exit: transition -> transition
val keep: (state -> unit) -> transition -> transition
val keep': (bool -> state -> unit) -> transition -> transition
@@ -295,16 +296,16 @@
(* primitive transitions *)
datatype trans =
- Init of string * (bool -> theory) | (*theory name, init*)
+ Init of string * (unit -> theory) | (*theory name, init*)
Exit | (*formal exit of theory*)
Keep of bool -> state -> unit | (*peek at state*)
Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*)
local
-fun apply_tr int (Init (_, f)) (State (NONE, _)) =
+fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
State (SOME (Theory (Context.Theory
- (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
+ (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
| apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
State (NONE, prev)
| apply_tr int (Keep f) state =
@@ -394,6 +395,12 @@
(* basic transitions *)
fun init_theory name f = add_trans (Init (name, f));
+
+fun modify_init f tr =
+ (case init_of tr of
+ SOME name => init_theory name f (reset_trans tr)
+ | NONE => tr);
+
val exit = add_trans Exit;
val keep' = add_trans o Keep;
--- a/src/Pure/ProofGeneral/pgip_parser.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Wed Jul 28 11:42:48 2010 +0200
@@ -19,7 +19,7 @@
fun badcmd text = [D.Badcmd {text = text}];
fun thy_begin text =
- (case try (Thy_Header.read Position.none) (Source.of_string text) of
+ (case try (Thy_Header.read Position.none) text of
NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
| SOME (name, imports, _) =>
D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Jul 28 11:42:48 2010 +0200
@@ -8,9 +8,10 @@
signature PROOF_GENERAL =
sig
val test_markupN: string
+ val sendback: string -> Pretty.T list -> unit
val init: bool -> unit
val init_outer_syntax: unit -> unit
- val sendback: string -> Pretty.T list -> unit
+ structure ThyLoad: sig val add_path: string -> unit end
end;
structure ProofGeneral: PROOF_GENERAL =
@@ -115,7 +116,7 @@
fun trace_action action name =
if action = Thy_Info.Update then
List.app tell_file_loaded (Thy_Info.loaded_files name)
- else if action = Thy_Info.Outdate orelse action = Thy_Info.Remove then
+ else if action = Thy_Info.Remove then
List.app tell_file_retracted (Thy_Info.loaded_files name)
else ();
@@ -130,19 +131,17 @@
(*liberal low-level version*)
val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
-val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
+val inform_file_retracted = Thy_Info.kill_thy o thy_name;
fun inform_file_processed file =
let
val name = thy_name file;
val _ = name = "" andalso error ("Bad file name: " ^ quote file);
val _ =
- if Thy_Info.known_thy name then
- Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
- handle ERROR msg =>
- (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
- tell_file_retracted (Thy_Header.thy_path name))
- else ();
+ Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
+ handle ERROR msg =>
+ (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
+ tell_file_retracted (Thy_Header.thy_path name))
val _ = Isar.init ();
in () end;
@@ -247,4 +246,12 @@
Secure.PG_setup ();
Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
+
+(* fake old ThyLoad -- with new semantics *)
+
+structure ThyLoad =
+struct
+ val add_path = Thy_Load.set_master_path o Path.explode;
end;
+
+end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jul 28 11:42:48 2010 +0200
@@ -200,8 +200,6 @@
fun trace_action action name =
if action = Thy_Info.Update then
List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
- else if action = Thy_Info.Outdate then
- List.app (tell_file_outdated true) (Thy_Info.loaded_files name)
else if action = Thy_Info.Remove then
List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
else ()
@@ -217,11 +215,11 @@
val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
-val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
+val inform_file_retracted = Thy_Info.kill_thy o thy_name;
fun inform_file_processed path state =
let val name = thy_name path in
- if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
+ if Toplevel.is_toplevel state then
Thy_Info.register_thy (Toplevel.end_theory Position.none state)
handle ERROR msg =>
(warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
@@ -804,8 +802,7 @@
val filepath = PgipTypes.path_of_pgipurl url
val filedir = Path.dir filepath
val thy_name = Path.implode o #1 o Path.split_ext o Path.base
- val openfile_retract = Output.no_warnings_CRITICAL
- (Thy_Info.if_known_thy Thy_Info.remove_thy) o thy_name;
+ val openfile_retract = Output.no_warnings_CRITICAL Thy_Info.kill_thy o thy_name;
in
case !currently_open_file of
SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
--- a/src/Pure/Thy/thy_header.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML Wed Jul 28 11:42:48 2010 +0200
@@ -7,7 +7,7 @@
signature THY_HEADER =
sig
val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
- val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
+ val read: Position.T -> string -> string * string list * (string * bool) list
val thy_path: string -> Path.T
val split_thy_path: Path.T -> Path.T * string
val consistent_name: string -> string -> unit
@@ -53,9 +53,10 @@
(Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
(Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
-fun read pos src =
+fun read pos str =
let val res =
- src
+ str
+ |> Source.of_string_limited 8000
|> Symbol.source {do_recover = false}
|> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
|> Token.source_proper
--- a/src/Pure/Thy/thy_info.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Jul 28 11:42:48 2010 +0200
@@ -1,29 +1,26 @@
(* Title: Pure/Thy/thy_info.ML
Author: Markus Wenzel, TU Muenchen
-Main part of theory loader database, including handling of theory and
+Global theory info database, with auto-loading according to theory and
file dependencies.
*)
signature THY_INFO =
sig
- datatype action = Update | Outdate | Remove
+ datatype action = Update | Remove
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
- val known_thy: string -> bool
- val if_known_thy: (string -> unit) -> string -> unit
val lookup_theory: string -> theory option
val get_theory: string -> theory
val is_finished: string -> bool
val master_directory: string -> Path.T
val loaded_files: string -> Path.T list
- val touch_thy: string -> unit
val thy_ord: theory * theory -> order
val remove_thy: string -> unit
val kill_thy: string -> unit
val use_thys: string list -> unit
val use_thy: string -> unit
- val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
+ val toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
val register_thy: theory -> unit
val finish: unit -> unit
end;
@@ -33,7 +30,7 @@
(** theory loader actions and hooks **)
-datatype action = Update | Outdate | Remove;
+datatype action = Update | Remove;
local
val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
@@ -60,37 +57,21 @@
fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
-fun upd_deps name entry G =
- fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
- |> Graph.map_node name (K entry);
-
-fun new_deps name parents entry G =
- (if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G)
- |> add_deps name parents;
+fun new_entry name parents entry =
+ Graph.new_node (name, entry) #> add_deps name parents;
(* thy database *)
type deps =
- {update_time: int, (*symbolic time of update; negative value means outdated*)
- master: (Path.T * File.ident) option, (*master dependencies for thy file*)
- text: string, (*source text for thy*)
- parents: string list}; (*source specification of parents (partially qualified)*)
-
-fun make_deps update_time master text parents : deps =
- {update_time = update_time, master = master, text = text, parents = parents};
+ {master: (Path.T * File.ident), (*master dependencies for thy file*)
+ parents: string list}; (*source specification of parents (partially qualified)*)
-fun init_deps master text parents = SOME (make_deps ~1 master text parents);
-
-fun master_dir NONE = Path.current
- | master_dir (SOME (path, _)) = Path.dir path;
+fun make_deps master parents : deps = {master = master, parents = parents};
-fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d);
-fun master_dir'' d = the_default Path.current (Option.map master_dir' d);
-
+fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
fun base_name s = Path.implode (Path.base (Path.explode s));
-
local
val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
in
@@ -112,26 +93,20 @@
SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
val known_thy = is_some o lookup_thy;
-fun if_known_thy f name = if known_thy name then f name else ();
fun get_thy name =
(case lookup_thy name of
SOME thy => thy
| NONE => error (loader_msg "nothing known about theory" [name]));
-fun change_thy name f = CRITICAL (fn () =>
- (get_thy name; change_thys (Graph.map_node name f)));
-
(* access deps *)
val lookup_deps = Option.map #1 o lookup_thy;
val get_deps = #1 o get_thy;
-fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
-fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));
val is_finished = is_none o get_deps;
-val master_directory = master_dir' o get_deps;
+val master_directory = master_dir o get_deps;
fun get_parents name =
thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
@@ -153,174 +128,97 @@
fun loaded_files name =
(case get_deps name of
NONE => []
- | SOME {master, ...} =>
- (case master of
- NONE => []
- | SOME (thy_path, _) => thy_path :: Thy_Load.loaded_files (get_theory name)));
+ | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name));
(** thy operations **)
-(* maintain update_time *)
-
-local
-
-fun is_outdated name =
- (case lookup_deps name of
- SOME (SOME {update_time, ...}) => update_time < 0
- | _ => false);
-
-fun unfinished name =
- if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE)
- else SOME name;
-
-in
+(* abstract update time *)
-fun outdate_thy name =
- if is_finished name orelse is_outdated name then ()
- else CRITICAL (fn () =>
- (change_deps name (Option.map (fn {master, text, parents, ...} =>
- make_deps ~1 master text parents)); perform Outdate name));
-
-fun touch_thys names =
- List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
-
-fun touch_thy name = touch_thys [name];
-
-end;
-
-
-(* management data *)
-
-structure Management_Data = Theory_Data
+structure Update_Time = Theory_Data
(
- type T =
- Task_Queue.group option * (*worker thread group*)
- int; (*abstract update time*)
- val empty = (NONE, 0);
+ type T = int;
+ val empty = 0;
fun extend _ = empty;
fun merge _ = empty;
);
-val thy_ord = int_ord o pairself (#2 o Management_Data.get);
-
-
-(* pending proofs *)
-
-fun join_thy name =
- (case lookup_theory name of
- NONE => ()
- | SOME thy => PureThy.join_proofs thy);
-
-fun cancel_thy name =
- (case lookup_theory name of
- NONE => ()
- | SOME thy =>
- (case #1 (Management_Data.get thy) of
- NONE => ()
- | SOME group => Future.cancel_group group));
+val thy_ord = int_ord o pairself Update_Time.get;
(* remove theory *)
fun remove_thy name =
- if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+ if is_finished name then error (loader_msg "attempt to change finished theory" [name])
else
let
val succs = thy_graph Graph.all_succs [name];
- val _ = List.app cancel_thy succs;
val _ = priority (loader_msg "removing" succs);
val _ = CRITICAL (fn () =>
(List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
in () end;
-val kill_thy = if_known_thy remove_thy;
-
-
-(* load_thy *)
-
-fun required_by _ [] = ""
- | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-
-fun load_thy upd_time initiators name =
- let
- val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
- fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
- val (pos, text) =
- (case get_deps name of
- SOME {master = SOME (master_path, _), text, ...} =>
- if text = "" then corrupted ()
- else (Path.position master_path, text)
- | _ => corrupted ());
- val _ = touch_thy name;
- val _ =
- change_deps name (Option.map (fn {master, text, parents, ...} =>
- make_deps upd_time master text parents));
- val (after_load, theory) = Outer_Syntax.load_thy name pos text;
- val _ = put_theory name theory;
- val _ =
- CRITICAL (fn () =>
- (change_deps name
- (Option.map (fn {update_time, master, parents, ...} =>
- make_deps update_time master "" parents));
- perform Update name));
- in after_load end;
+fun kill_thy name =
+ if known_thy name then remove_thy name
+ else ();
(* scheduling loader tasks *)
-datatype task = Task of (unit -> unit -> unit) | Finished | Running;
-fun task_finished Finished = true | task_finished _ = false;
+datatype task =
+ Task of string list * (theory list -> (theory * (unit -> unit))) |
+ Finished of theory;
+
+fun task_finished (Task _) = false
+ | task_finished (Finished _) = true;
local
+fun schedule_seq task_graph =
+ ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
+ (case Graph.get_node task_graph name of
+ Task (parents, body) =>
+ let
+ val (thy, after_load) = body (map (the o Symtab.lookup tab) parents);
+ val _ = after_load ();
+ in Symtab.update (name, thy) tab end
+ | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
+
fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
let
- val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
- (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
-
+ val tasks = Graph.topological_order task_graph;
val par_proofs = ! parallel_proofs >= 1;
- fun fork (name, body) tab =
- let
- val deps = Graph.imm_preds task_graph name
- |> map_filter (fn parent =>
- (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
- fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
-
- val future = Future.fork_deps (map #2 deps) (fn () =>
- (case map_filter failed deps of
- [] => body ()
- | bad => error (loader_msg
- ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
- val future' =
- if par_proofs then future
- else Future.map (fn after_load => (after_load (); fn () => ())) future;
- in Symtab.update (name, future') tab end;
-
- val futures = fold fork tasks Symtab.empty;
+ val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
+ (case Graph.get_node task_graph name of
+ Task (parents, body) =>
+ let
+ val get = the o Symtab.lookup tab;
+ val deps = map (`get) (Graph.imm_preds task_graph name);
+ fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
- val failed = tasks |> maps (fn (name, _) =>
- let
- val after_load = Future.join (the (Symtab.lookup futures name));
- val _ = join_thy name;
- val _ = after_load ();
- in [] end handle exn => [(name, exn)]) |> rev;
+ val future = Future.fork_deps (map #1 deps) (fn () =>
+ (case map_filter failed deps of
+ [] => body (map (#1 o Future.join o get) parents)
+ | bad => error (loader_msg
+ ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+ val future' =
+ if par_proofs then future
+ else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
+ in Symtab.update (name, future') tab end
+ | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
- val _ = List.app (kill_thy o #1) failed;
- val _ = Exn.release_all (map (Exn.Exn o #2) failed);
+ val _ =
+ tasks |> maps (fn name =>
+ let
+ val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
+ val _ = PureThy.join_proofs thy;
+ val _ = after_load ();
+ in [] end handle exn => [Exn.Exn exn])
+ |> rev |> Exn.release_all;
in () end) ();
-fun schedule_seq tasks =
- Graph.topological_order tasks
- |> List.app (fn name =>
- (case Graph.get_node tasks name of
- Task body =>
- let val after_load = body ()
- in after_load () handle exn => (kill_thy name; reraise exn) end
- | _ => ()));
-
in
fun schedule_tasks tasks =
@@ -337,34 +235,54 @@
local
+fun required_by _ [] = ""
+ | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
+
+fun load_thy initiators update_time (deps: deps) text dir name parent_thys =
+ let
+ val _ = kill_thy name;
+ val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+
+ val {master = (thy_path, _), ...} = deps;
+ val pos = Path.position thy_path;
+ val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
+ fun init () =
+ Thy_Load.begin_theory dir name parent_thys uses
+ |> Present.begin_theory update_time dir uses
+ |> Update_Time.put update_time;
+
+ val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
+
+ val parent_names = map Context.theory_name parent_thys;
+ fun after_load' () =
+ (after_load ();
+ CRITICAL (fn () =>
+ (change_thys (new_entry name parent_names (SOME deps, SOME theory));
+ perform Update name)));
+
+ in (theory, after_load') end;
+
fun check_deps dir name =
(case lookup_deps name of
- SOME NONE => (true, NONE, get_parents name)
+ SOME NONE => (true, NONE, get_parents name, NONE)
| NONE =>
let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
- in (false, init_deps (SOME master) text parents, parents) end
- | SOME (SOME {update_time, master, text, parents}) =>
- let
- val (thy_path, thy_id) = Thy_Load.check_thy dir name;
- val master' = SOME (thy_path, thy_id);
- in
- if Option.map #2 master <> SOME thy_id then
+ in (false, SOME (make_deps master parents), parents, SOME text) end
+ | SOME (SOME {master, parents}) =>
+ let val master' = Thy_Load.check_thy dir name in
+ if #2 master <> #2 master' then
let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
- in (false, init_deps master' text' parents', parents') end
+ in (false, SOME (make_deps master' parents'), parents', SOME text') end
else
let
val current =
(case lookup_theory name of
NONE => false
- | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
- val update_time' = if current then update_time else ~1;
- val deps' = SOME (make_deps update_time' master' text parents);
- in (current, deps', parents) end
+ | SOME theory => Thy_Load.all_current theory);
+ val deps' = SOME (make_deps master' parents);
+ in (current, deps', parents, NONE) end
end);
-fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
- SOME (make_deps update_time master (File.read path) parents);
-
in
fun require_thys initiators dir strs tasks =
@@ -380,33 +298,33 @@
SOME task => (task_finished task, tasks)
| NONE =>
let
- val (current, deps, parents) = check_deps dir' name
+ val (current, deps, parents, opt_text) = check_deps dir' name
handle ERROR msg => cat_error msg
(loader_msg "the error(s) above occurred while examining theory" [name] ^
required_by "\n" initiators);
+
val parent_names = map base_name parents;
-
- val (parents_current, tasks_graph') =
- require_thys (name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
+ val (parents_current, tasks') =
+ require_thys (name :: initiators) (Path.append dir (master_dir deps)) parents tasks;
val all_current = current andalso parents_current;
- val _ = if not all_current andalso known_thy name then outdate_thy name else ();
- val entry =
- if all_current then (deps, SOME (get_theory name))
- else (read_text deps, NONE);
- val _ = change_thys (new_deps name parent_names entry);
-
- val upd_time = serial ();
- val tasks_graph'' = tasks_graph' |> new_deps name parent_names
- (if all_current then Finished
- else Task (fn () => load_thy upd_time initiators name));
- in (all_current, tasks_graph'') end)
+ val task =
+ if all_current then Finished (get_theory name)
+ else
+ (case deps of
+ NONE => raise Fail "Malformed deps"
+ | SOME (dep as {master = (thy_path, _), ...}) =>
+ let
+ val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
+ val update_time = serial ();
+ in Task (parent_names, load_thy initiators update_time dep text dir' name) end);
+ in (all_current, new_entry name parent_names task tasks') end)
end;
end;
-(* use_thy etc. *)
+(* use_thy *)
fun use_thys_dir dir arg =
schedule_tasks (snd (require_thys [] dir arg Graph.empty));
@@ -415,65 +333,32 @@
val use_thy = use_thys o single;
-(* begin theory *)
-
-fun check_unfinished name =
- if known_thy name andalso is_finished name then
- error (loader_msg "cannot update finished theory" [name])
- else ();
-
-fun begin_theory name parents uses int =
- let
- val parent_names = map base_name parents;
- val dir = master_dir'' (lookup_deps name);
- val _ = check_unfinished name;
- val _ = if int then use_thys_dir dir parents else ();
+(* toplevel begin theory -- without maintaining database *)
- val theory =
- Theory.begin_theory name (map get_theory parent_names)
- |> Thy_Load.init dir
- |> fold (Thy_Load.require o fst) uses;
-
- val deps =
- if known_thy name then get_deps name
- else init_deps NONE "" parents;
- val _ = change_thys (new_deps name parent_names (deps, NONE));
-
- val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
- val update_time = if update_time > 0 then update_time else serial ();
- val theory' = theory
- |> Management_Data.put (Future.worker_group (), update_time)
- |> Present.begin_theory update_time dir uses;
-
- val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
- val theory'' =
- fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
- in theory'' end;
+fun toplevel_begin_theory name imports uses =
+ let
+ val dir = Thy_Load.get_master_path ();
+ val _ = kill_thy name;
+ val _ = use_thys_dir dir imports;
+ val parents = map (get_theory o base_name) imports;
+ in Thy_Load.begin_theory dir name parents uses end;
-(* register existing theories *)
+(* register theory *)
fun register_thy theory =
let
val name = Context.theory_name theory;
+ val _ = kill_thy name;
val _ = priority ("Registering theory " ^ quote name);
- val parent_names = map Context.theory_name (Theory.parents_of theory);
- val _ = map get_theory parent_names;
val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
- val update_time = #2 (Management_Data.get theory);
- val parents =
- (case lookup_deps name of
- SOME (SOME {parents, ...}) => parents
- | _ => parent_names);
- val deps = make_deps update_time (SOME master) "" parents;
+ val parents = map Context.theory_name (Theory.parents_of theory);
+ val deps = make_deps master parents;
in
CRITICAL (fn () =>
- (if known_thy name then
- (List.app remove_thy (thy_graph Graph.imm_succs name);
- change_thys (Graph.del_nodes [name]))
- else ();
- change_thys (new_deps name parents (SOME deps, SOME theory));
+ (map get_theory parents;
+ change_thys (new_entry name parents (SOME deps, SOME theory));
perform Update name))
end;
--- a/src/Pure/Thy/thy_load.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Wed Jul 28 11:42:48 2010 +0200
@@ -17,8 +17,9 @@
signature THY_LOAD =
sig
include BASIC_THY_LOAD
+ val set_master_path: Path.T -> unit
+ val get_master_path: unit -> Path.T
val master_directory: theory -> Path.T
- val init: Path.T -> theory -> theory
val require: Path.T -> theory -> theory
val provide: Path.T * (Path.T * File.ident) -> theory -> theory
val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
@@ -31,6 +32,7 @@
val provide_file: Path.T -> theory -> theory
val use_ml: Path.T -> unit
val exec_ml: Path.T -> generic_theory -> generic_theory
+ val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory
end;
structure Thy_Load: THY_LOAD =
@@ -61,7 +63,7 @@
val master_directory = #master_dir o Files.get;
-fun init master_dir = map_files (fn _ => (master_dir, [], []));
+fun master dir = map_files (fn _ => (dir, [], []));
fun require src_path =
map_files (fn (master_dir, required, provided) =>
@@ -69,16 +71,19 @@
error ("Duplicate source file dependency: " ^ Path.implode src_path)
else (master_dir, src_path :: required, provided));
-fun provide (src_path, path_info) =
+fun provide (src_path, path_id) =
map_files (fn (master_dir, required, provided) =>
if AList.defined (op =) provided src_path then
error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
- else (master_dir, required, (src_path, path_info) :: provided));
+ else (master_dir, required, (src_path, path_id) :: provided));
-(* maintain load path *)
+(* maintain default paths *)
-local val load_path = Unsynchronized.ref [Path.current] in
+local
+ val load_path = Unsynchronized.ref [Path.current];
+ val master_path = Unsynchronized.ref Path.current;
+in
fun show_path () = map Path.implode (! load_path);
@@ -97,6 +102,9 @@
fun search_path dir path =
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
+fun set_master_path path = master_path := path;
+fun get_master_path () = ! master_path;
+
end;
@@ -140,10 +148,9 @@
fun deps_thy dir name =
let
- val master as (path, _) = check_thy dir name;
- val text = File.read path;
- val (name', imports, uses) =
- Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
+ val master as (thy_path, _) = check_thy dir name;
+ val text = File.read thy_path;
+ val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
val _ = Thy_Header.consistent_name name name';
val uses = map (Path.explode o #1) uses;
in {master = master, text = text, imports = imports, uses = uses} end;
@@ -171,10 +178,10 @@
fun all_current thy =
let
val {master_dir, provided, ...} = Files.get thy;
- fun current (src_path, path_info) =
+ fun current (src_path, (_, id)) =
(case test_file master_dir src_path of
NONE => false
- | SOME path_info' => eq_snd (op =) (path_info, path_info'));
+ | SOME (_, id') => id = id');
in can check_loaded thy andalso forall current provided end;
val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
@@ -191,17 +198,27 @@
else
let
val thy = ML_Context.the_global_context ();
- val (path, info) = check_file (master_directory thy) src_path;
+ val (path, id) = check_file (master_directory thy) src_path;
val _ = ML_Context.eval_file path;
val _ = Context.>> Local_Theory.propagate_ml_env;
- val provide = provide (src_path, (path, info));
+ val provide = provide (src_path, (path, id));
val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
- in () end
+ in () end;
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
+
+(* begin theory *)
+
+fun begin_theory dir name parents uses =
+ Theory.begin_theory name parents
+ |> master dir
+ |> fold (require o fst) uses
+ |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
+ |> Theory.checkpoint;
+
end;
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;