equal
deleted
inserted
replaced
8 use "graph.ML"; |
8 use "graph.ML"; |
9 use "object.ML"; |
9 use "object.ML"; |
10 use "seq.ML"; |
10 use "seq.ML"; |
11 use "name_space.ML"; |
11 use "name_space.ML"; |
12 use "position.ML"; |
12 use "position.ML"; |
|
13 use "scan.ML"; |
13 use "path.ML"; |
14 use "path.ML"; |
14 use "file.ML"; |
15 use "file.ML"; |
15 use "buffer.ML"; |
16 use "buffer.ML"; |
16 use "history.ML"; |
17 use "history.ML"; |
17 use "scan.ML"; |
|
18 use "source.ML"; |
18 use "source.ML"; |
19 use "symbol.ML"; |
19 use "symbol.ML"; |
20 use "pretty.ML"; |
20 use "pretty.ML"; |
21 |
21 |
22 structure PureGeneral = |
22 structure PureGeneral = |
25 structure Graph = Graph; |
25 structure Graph = Graph; |
26 structure Object = Object; |
26 structure Object = Object; |
27 structure Seq = Seq; |
27 structure Seq = Seq; |
28 structure NameSpace = NameSpace; |
28 structure NameSpace = NameSpace; |
29 structure Position = Position; |
29 structure Position = Position; |
|
30 structure Scan = Scan; |
30 structure Path = Path; |
31 structure Path = Path; |
31 structure File = File; |
32 structure File = File; |
32 structure Buffer = Buffer; |
33 structure Buffer = Buffer; |
33 structure History = History; |
34 structure History = History; |
34 structure Scan = Scan; |
|
35 structure Source = Source; |
35 structure Source = Source; |
36 structure Symbol = Symbol; |
36 structure Symbol = Symbol; |
37 structure Pretty = Pretty; |
37 structure Pretty = Pretty; |
38 end; |
38 end; |