# HG changeset patch
# User obua
# Date 1140098397 -3600
# Node ID 04b302f2902d22f94bbcad49ad71ff3a1fdadb8d
# Parent  c0321d7d6b3dafdf93bb2b716c156514a12ba7c4
cache improvements

diff -r c0321d7d6b3d -r 04b302f2902d src/HOL/Import/importrecorder.ML
--- a/src/HOL/Import/importrecorder.ML	Thu Feb 16 04:17:19 2006 +0100
+++ b/src/HOL/Import/importrecorder.ML	Thu Feb 16 14:59:57 2006 +0100
@@ -13,6 +13,7 @@
 			| Hol_type_mapping of string * string * string
 			| Indexed_theorem of int * term
 	                | Protect_varname of string * string
+			| Dump of string
 
     datatype history = History of history_entry list
 	 and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
@@ -37,6 +38,7 @@
     val add_hol_type_mapping : string -> string -> string -> unit
     val add_indexed_theorem : int -> thm -> unit
     val protect_varname : string -> string -> unit
+    val add_dump : string -> unit
 
     val set_skip_import_dir : string option -> unit
     val get_skip_import_dir : unit -> string option
@@ -63,6 +65,7 @@
 		    | Hol_type_mapping of string * string * string
 		    | Indexed_theorem of int * term
 	            | Protect_varname of string * string
+		    | Dump of string
 
 datatype history_entry = StartReplay of string*string  
 		       | StopReplay of string*string
@@ -108,6 +111,7 @@
       | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
       | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
       | delta (Protect_varname args) = wrap "protect_varname" entry args
+      | delta (Dump args) = wrap "dump" string args
 
     fun history_entry (StartReplay args) = wrap "startreplay" entry args
       | history_entry (StopReplay args) = wrap "stopreplay" entry args
@@ -146,6 +150,7 @@
       | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
       | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
       | delta "protect_varname" = unwrap Protect_varname entry
+      | delta "dump" = unwrap Dump string
       | delta _ = raise ParseException "delta"
 
     val delta = fn e => delta (name_of_wrap e) e
@@ -178,6 +183,7 @@
 fun add_specification names th = add_delta (Specification (names, prop_of th)) 
 fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
 fun protect_varname s t = add_delta (Protect_varname (s,t))
+fun add_dump s = add_delta (Dump s)
 			    
 fun set_skip_import_dir dir = (history_dir := dir)
 fun get_skip_import_dir () = !history_dir
diff -r c0321d7d6b3d -r 04b302f2902d src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 04:17:19 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 14:59:57 2006 +0100
@@ -114,6 +114,7 @@
     val prin : term -> unit 
     val protect_factname : string -> string 
     val replay_protect_varname : string -> string -> unit
+    val replay_add_dump : string -> theory -> theory
 end
 
 structure ProofKernel :> ProofKernel =
@@ -128,6 +129,9 @@
 
 fun to_hol_thm th = HOLThm ([], th)
 
+val replay_add_dump = add_dump
+fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
+
 datatype proof_info
   = Info of {disk_info: (string * string) option ref}
 	    
diff -r c0321d7d6b3d -r 04b302f2902d src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Thu Feb 16 04:17:19 2006 +0100
+++ b/src/HOL/Import/replay.ML	Thu Feb 16 14:59:57 2006 +0100
@@ -328,18 +328,6 @@
 	  | rps (t::ts) thy = rps ts (rp t thy)
 	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
 	  | rp (DeltaEntry ds) thy = fold delta ds thy
-(*    datatype deltastate = Consts of (string * typ * mixfix) list
-			| Specification of (string * string * bool) list * term
-			| Hol_mapping of string * string * string
-			| Hol_pending of string * string * term
-			| Hol_const_mapping of string * string * string
-			| Hol_move of string * string
-			| Defs of string * term
-			| Hol_theorem of string * string * term
-			| Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
-			| Hol_type_mapping of string * string * string
-			| Indexed_theorem of int * term
-*)
 	and delta (Specification (names, th)) thy = 
 	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
 	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
@@ -361,8 +349,8 @@
 	    add_hol4_type_mapping thyname tycname true fulltyname thy
 	  | delta (Indexed_theorem (i, th)) thy = 
 	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
-          | delta (Protect_varname (s,t)) thy =
-	    (P.replay_protect_varname s t; thy)
+          | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
+	  | delta (Dump s) thy = P.replay_add_dump s thy
     in
 	rps
     end