1(*---------------------------------------------------------------------------*) 2(* History provides "registers-with-bounded-history". You can read (via *) 3(* "project"), write (via "apply"), and undo. *) 4(*---------------------------------------------------------------------------*) 5 6structure History :> History = 7struct 8 9open Feedback Lib; 10 11val HIST_ERR = mk_HOL_ERR "History"; 12exception CANT_BACKUP_ANYMORE; 13 14datatype 'a history = HISTORY of {obj:'a, past:'a list, orig:'a, limit:int, save_points:'a list}; 15 16fun new_history {obj, limit} = HISTORY{obj=obj, past=[], orig=obj, limit=limit, save_points = []} 17 18local fun chop n alist = fst (split_after n alist) handle _ => alist 19in 20fun apply f (HISTORY{obj, past, orig, limit, save_points}) = 21 HISTORY{obj=f obj, past=chop limit (obj::past), orig=orig, limit=limit, save_points=save_points} 22 23fun set_limit (HISTORY{obj,past,orig,limit,save_points}) n = 24 if n<0 then raise HIST_ERR "set_limit" "negative limit" 25 else HISTORY{obj=obj, past=chop n past, orig=orig, limit=n,save_points=save_points} 26end; 27 28fun remove_past (HISTORY{obj,past,orig,limit,save_points}) = 29 new_history {obj=obj,limit=limit}; 30 31fun initialValue (HISTORY{orig, ...}) = orig; 32 33fun project f (HISTORY{obj, ...}) = f obj; 34 35fun undo (HISTORY{past=[], ...}) = raise CANT_BACKUP_ANYMORE 36 | undo (HISTORY{past=h::rst, limit, orig,save_points,...}) = 37 HISTORY{obj=h, past=rst, orig=orig, limit=limit,save_points=save_points} 38 39fun restore (HISTORY{obj,past,orig,limit,save_points}) = 40 let 41 val (save_points',obj') = if (null save_points) then ([], orig) else 42 (if not (null past) then (save_points, hd save_points) else 43 (if null (tl save_points) then ([], orig) else 44 (tl save_points, hd (tl (save_points))))); 45 in 46 HISTORY{obj=obj', past=[], orig=orig, limit=limit, save_points=save_points'} 47 end; 48 49fun save (HISTORY{obj,past,orig,limit,save_points}) = 50 HISTORY{obj=obj, past=[], orig=orig, limit=limit, save_points=obj::save_points} 51 52end 53