# HG changeset patch # User wenzelm # Date 1309626531 -7200 # Node ID f57bcfb54808f475a5dee1d5139f36548b99964f # Parent 9cba66fb109ab57f794619989c19ea066d857612 misc tuning; diff -r 9cba66fb109a -r f57bcfb54808 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Jul 02 10:37:35 2011 +0200 +++ b/src/Pure/Thy/thy_info.ML Sat Jul 02 19:08:51 2011 +0200 @@ -34,10 +34,11 @@ datatype action = Update | Remove; local - val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list); + val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list); in - fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f)); - fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks); + fun add_hook f = Synchronized.change hooks (cons f); + fun perform action name = + List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks); end; @@ -135,7 +136,7 @@ (** thy operations **) -(* remove theory *) +(* main loader actions *) fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () => if is_finished name then error (loader_msg "attempt to change finished theory" [name]) @@ -151,6 +152,16 @@ if known_thy name then remove_thy name else ()); +fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () => + let + val name = Context.theory_name theory; + val parents = map Context.theory_name (Theory.parents_of theory); + val _ = kill_thy name; + val _ = map get_theory parents; + val _ = change_thys (new_entry name parents (SOME deps, SOME theory)); + val _ = perform Update name; + in () end); + (* scheduling loader tasks *) @@ -226,7 +237,7 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy initiators update_time (deps: deps) text name parent_thys = +fun load_thy initiators update_time deps text name parent_thys = let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); @@ -240,13 +251,7 @@ |> Present.begin_theory update_time dir uses; val (theory, present) = Outer_Syntax.load_thy name init pos text; - - val parents = map Context.theory_name parent_thys; - fun commit () = - NAMED_CRITICAL "Thy_Info" (fn () => - (map get_theory parents; - change_thys (new_entry name parents (SOME deps, SOME theory)); - perform Update name)); + fun commit () = update_thy deps theory; in (theory, present, commit) end; fun check_deps dir name = @@ -332,16 +337,12 @@ let val name = Context.theory_name theory; val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; - val parents = map Context.theory_name (Theory.parents_of theory); val imports = Thy_Load.imports_of theory; - val deps = make_deps master imports; in NAMED_CRITICAL "Thy_Info" (fn () => (kill_thy name; Output.urgent_message ("Registering theory " ^ quote name); - map get_theory parents; - change_thys (new_entry name parents (SOME deps, SOME theory)); - perform Update name)) + update_thy (make_deps master imports) theory)) end;