# HG changeset patch # User wenzelm # Date 1280310168 -7200 # Node ID ac704f1c8dde2ed641e159c0b7418291a0a29d40 # Parent dc56a9a8e19d4329a3d3cbd12a0f6ea85525f5ab# Parent aac4eb1fa1d87286d0f474cab988f50280a9b5da merged diff -r dc56a9a8e19d -r ac704f1c8dde Admin/isatest/isatest-statistics --- 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 ;; *) diff -r dc56a9a8e19d -r ac704f1c8dde Admin/isatest/isatest-stats --- 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 diff -r dc56a9a8e19d -r ac704f1c8dde doc-src/IsarImplementation/Thy/Integration.thy --- 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 \} 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 dc56a9a8e19d -r ac704f1c8dde doc-src/IsarImplementation/Thy/document/Integration.tex --- 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 diff -r dc56a9a8e19d -r ac704f1c8dde doc-src/antiquote_setup.ML --- 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; diff -r dc56a9a8e19d -r ac704f1c8dde doc-src/rail.ML --- 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 diff -r dc56a9a8e19d -r ac704f1c8dde etc/isar-keywords-ZF.el --- 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 diff -r dc56a9a8e19d -r ac704f1c8dde etc/isar-keywords.el --- 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")) diff -r dc56a9a8e19d -r ac704f1c8dde src/HOL/Groups.thy --- 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") = diff -r dc56a9a8e19d -r ac704f1c8dde src/HOL/Quotient.thy --- 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 *} diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/General/secure.ML --- 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 *) diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Isar/isar_cmd.ML --- 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 = () diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Isar/isar_syn.ML --- 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; diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Isar/outer_syntax.ML --- 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); diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Isar/toplevel.ML --- 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; diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/ProofGeneral/pgip_parser.ML --- 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}) diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/ProofGeneral/proof_general_emacs.ML --- 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; diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 (" when a file is already open!\nCurrently open file: " ^ diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Thy/thy_header.ML --- 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 diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Thy/thy_info.ML --- 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; diff -r dc56a9a8e19d -r ac704f1c8dde src/Pure/Thy/thy_load.ML --- 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;