equal
deleted
inserted
replaced
|
1 (* Title: "BridgeJEdit/preliminary.sml" |
|
2 Author: Walther Neuper |
|
3 (c) due to copyright terms |
|
4 *) |
|
5 |
|
6 "-----------------------------------------------------------------------------------------------"; |
|
7 "table of contents -----------------------------------------------------------------------------"; |
|
8 "-----------------------------------------------------------------------------------------------"; |
|
9 "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; |
|
10 "-----------------------------------------------------------------------------------------------"; |
|
11 "-----------------------------------------------------------------------------------------------"; |
|
12 "-----------------------------------------------------------------------------------------------"; |
|
13 |
|
14 "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; |
|
15 "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; |
|
16 "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; |
|
17 (* Pure/context.ML |
|
18 signature THEORY_DATA = |
|
19 sig |
|
20 type T |
|
21 val get: theory -> T |
|
22 val put: T -> theory -> theory |
|
23 val map: (T -> T) -> theory -> theory |
|
24 end;*) |
|
25 (* |
|
26 Refs_Data.empty; (*in Refs_Data defined workers are hidden*) |
|
27 Refs_Data.extend; (*in Refs_Data defined workers are hidden*) |
|
28 Refs_Data.merge; (*in Refs_Data defined workers are hidden*) |
|
29 ML error: |
|
30 Value or constructor (empty) has not been declared in structure Refs *) |
|
31 |
|
32 Refs_Data.get: theory -> Refs_Data.T; (*from signature THEORY_DATA*) |
|
33 Refs_Data.put: Refs_Data.T -> theory -> theory; (*from signature THEORY_DATA*) |
|
34 Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*) |