changeset 59363 | 4660b0409096 |
parent 59203 | 5f0bd5afc16d |
child 59470 | 31d810570879 |
--- a/src/Pure/ROOT.ML Tue Jan 13 21:46:09 2015 +0100 +++ b/src/Pure/ROOT.ML Wed Jan 14 11:52:08 2015 +0100 @@ -65,6 +65,7 @@ use "General/linear_set.ML"; use "General/buffer.ML"; use "General/pretty.ML"; +use "PIDE/xml.ML"; use "General/path.ML"; use "General/url.ML"; use "General/file.ML"; @@ -78,7 +79,6 @@ if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); use "General/sha1_samples.ML"; -use "PIDE/xml.ML"; use "PIDE/yxml.ML"; use "PIDE/document_id.ML";