# HG changeset patch # User wenzelm # Date 1280086959 -7200 # Node ID a2e73df0b1e03c53cfc723da7181d63390f29b31 # Parent ddc3b72f9a4295697f4236a5d1a63a197694f3f9 simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; eliminated obsolete touch_child_thys, register_theory; diff -r ddc3b72f9a42 -r a2e73df0b1e0 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Jul 25 14:41:48 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Jul 25 21:42:39 2010 +0200 @@ -138,8 +138,7 @@ val _ = name = "" andalso error ("Bad file name: " ^ quote file); val _ = if Thy_Info.known_thy name then - (Thy_Info.register_thy name (Toplevel.end_theory Position.none (Isar.state ())); - Thy_Info.touch_child_thys name) + 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)) diff -r ddc3b72f9a42 -r a2e73df0b1e0 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Jul 25 14:41:48 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Jul 25 21:42:39 2010 +0200 @@ -218,15 +218,14 @@ 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_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name; -fun proper_inform_file_processed path state = +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 - (Thy_Info.touch_child_thys name; - Thy_Info.register_thy name (Toplevel.end_theory Position.none state) handle ERROR msg => - (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); - tell_file_retracted true (Path.base path))) + Thy_Info.register_thy (Toplevel.end_theory Position.none state) + handle ERROR msg => + (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); + tell_file_retracted true (Path.base path)) else raise Toplevel.UNDEF end; @@ -819,7 +818,7 @@ fun closefile _ = case !currently_open_file of - SOME f => (proper_inform_file_processed f (Isar.state()); + SOME f => (inform_file_processed f (Isar.state ()); priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); currently_open_file := NONE) | NONE => raise PGIP (" when no file is open!") diff -r ddc3b72f9a42 -r a2e73df0b1e0 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Jul 25 14:41:48 2010 +0200 +++ b/src/Pure/Thy/thy_info.ML Sun Jul 25 21:42:39 2010 +0200 @@ -18,15 +18,13 @@ val master_directory: string -> Path.T val loaded_files: string -> Path.T list val touch_thy: string -> unit - val touch_child_thys: 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 register_thy: string -> theory -> unit - val register_theory: theory -> unit + val register_thy: theory -> unit val finish: unit -> unit end; @@ -187,7 +185,6 @@ List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names)); fun touch_thy name = touch_thys [name]; -fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name); end; @@ -454,45 +451,28 @@ (* register existing theories *) -fun register_thy name theory = - let - val _ = priority ("Registering theory " ^ quote name); - val _ = map get_theory (get_parents name); - val _ = check_unfinished name; - val _ = touch_thy name; - val master = #master (Thy_Load.deps_thy Path.current name); - val upd_time = #2 (Management_Data.get theory); - in - CRITICAL (fn () => - (change_deps name (Option.map (fn {parents, ...} => - make_deps upd_time (SOME master) "" parents)); - put_theory name theory; - perform Update name)) - end; - -fun register_theory theory = +fun register_thy theory = let val name = Context.theory_name theory; - val parents = Theory.parents_of theory; - val parent_names = map Context.theory_name parents; - - fun err txt bads = - error (loader_msg txt bads ^ "\ncannot register theory " ^ quote 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 nonfinished = filter_out is_finished parent_names; - fun get_variant (x, y_name) = - if Theory.eq_thy (x, get_theory y_name) then NONE - else SOME y_name; - val variants = map_filter get_variant (parents ~~ parent_names); - - fun register G = - (Graph.new_node (name, (NONE, SOME theory)) G - handle Graph.DUP _ => err "duplicate theory entry" []) - |> add_deps name 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; in - if not (null nonfinished) then err "non-finished parent theories" nonfinished - else if not (null variants) then err "different versions of parent theories" variants - else CRITICAL (fn () => (change_thys register; perform Update name)) + 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)); + perform Update name)) end; diff -r ddc3b72f9a42 -r a2e73df0b1e0 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Sun Jul 25 14:41:48 2010 +0200 +++ b/src/Pure/pure_setup.ML Sun Jul 25 21:42:39 2010 +0200 @@ -4,14 +4,16 @@ Pure theory and ML toplevel setup. *) -(* the Pure theories *) +(* the Pure theory *) Context.>> (Context.map_theory (Outer_Syntax.process_file (Path.explode "Pure.thy") #> Theory.end_theory)); + structure Pure = struct val thy = ML_Context.the_global_context () end; + Context.set_thread_data NONE; -Thy_Info.register_theory Pure.thy; +Thy_Info.register_thy Pure.thy; (* ML toplevel pretty printing *)