author | wenzelm |
Mon, 29 Feb 2016 15:39:17 +0100 | |
changeset 62468 | d97e13e5ea5b |
parent 62467 | c1b88e647e2f |
permissions | -rw-r--r-- |
(* Title: Pure/RAW/ml_heap.ML Author: Makarius ML heap operations. *) signature ML_HEAP = sig val share_common_data: unit -> unit val save_state: string -> unit end; structure ML_Heap: ML_HEAP = struct fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; val save_state = PolyML.SaveState.saveState o ML_System.platform_path; end;