src/Pure/ROOT.ML
changeset 80889 510f6cb6721e
parent 80803 7e39c785ca5d
child 80919 1a52cc1c3274
--- a/src/Pure/ROOT.ML	Mon Sep 16 19:36:20 2024 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 16 19:58:28 2024 +0200
@@ -114,6 +114,9 @@
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
+ML_file "General/completion.ML";
+ML_file "General/name_space.ML";
+ML_file "PIDE/markup_expression.ML";
 ML_file "soft_type_system.ML";
 
 
@@ -158,8 +161,6 @@
 ML_file "term_ord.ML";
 ML_file "term_items.ML";
 ML_file "term_subst.ML";
-ML_file "General/completion.ML";
-ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";