equal
deleted
inserted
replaced
86 ML_file "General/seq.ML"; |
86 ML_file "General/seq.ML"; |
87 ML_file "General/time.ML"; |
87 ML_file "General/time.ML"; |
88 ML_file "General/timing.ML"; |
88 ML_file "General/timing.ML"; |
89 ML_file "General/sha1.ML"; |
89 ML_file "General/sha1.ML"; |
90 |
90 |
|
91 ML_file "PIDE/yxml.ML"; |
91 ML_file "PIDE/byte_message.ML"; |
92 ML_file "PIDE/byte_message.ML"; |
92 ML_file "PIDE/yxml.ML"; |
|
93 ML_file "PIDE/protocol_message.ML"; |
93 ML_file "PIDE/protocol_message.ML"; |
94 ML_file "PIDE/document_id.ML"; |
94 ML_file "PIDE/document_id.ML"; |
95 |
95 |
96 ML_file "General/change_table.ML"; |
96 ML_file "General/change_table.ML"; |
97 ML_file "General/graph.ML"; |
97 ML_file "General/graph.ML"; |