changeset 62508 | d0b68218ea55 |
parent 62468 | d97e13e5ea5b |
child 62630 | bc772694cfbd |
62507:15c36c181130 | 62508:d0b68218ea55 |
---|---|
1 (* Title: Pure/ML/ml_heap.ML |
|
2 Author: Makarius |
|
3 |
|
4 ML heap operations. |
|
5 *) |
|
6 |
|
7 signature ML_HEAP = |
|
8 sig |
|
9 val share_common_data: unit -> unit |
|
10 val save_state: string -> unit |
|
11 end; |
|
12 |
|
13 structure ML_Heap: ML_HEAP = |
|
14 struct |
|
15 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
16 val save_state = PolyML.SaveState.saveState o ML_System.platform_path; |
|
17 end; |