equal
deleted
inserted
replaced
15 use "history.ML"; |
15 use "history.ML"; |
16 use "scan.ML"; |
16 use "scan.ML"; |
17 use "source.ML"; |
17 use "source.ML"; |
18 use "symbol.ML"; |
18 use "symbol.ML"; |
19 use "pretty.ML"; |
19 use "pretty.ML"; |
20 use "use.ML"; |
|
21 |
20 |
22 structure PureGeneral = |
21 structure PureGeneral = |
23 struct |
22 struct |
24 structure Symtab = Symtab; |
23 structure Symtab = Symtab; |
25 structure Graph = Graph; |
24 structure Graph = Graph; |
32 structure History = History; |
31 structure History = History; |
33 structure Scan = Scan; |
32 structure Scan = Scan; |
34 structure Source = Source; |
33 structure Source = Source; |
35 structure Symbol = Symbol; |
34 structure Symbol = Symbol; |
36 structure Pretty = Pretty; |
35 structure Pretty = Pretty; |
37 structure Use = Use; |
|
38 end; |
36 end; |