src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Sun Dec 06 16:14:16 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Dec 06 16:27:37 2020 +0100
@@ -19,9 +19,10 @@
 {
   /* session and theory names */
 
+  val ROOTS: Path = Path.explode("ROOTS")
   val ROOT: Path = Path.explode("ROOT")
-  val ROOTS: Path = Path.explode("ROOTS")
 
+  val roots_name: String = "ROOTS"
   val root_name: String = "ROOT"
   val theory_name: String = "Pure.Sessions"
 
@@ -37,6 +38,21 @@
     name == root_name || name == "README" || name == "index" || name == "bib"
 
 
+  /* ROOTS file format */
+
+  class File_Format extends isabelle.File_Format
+  {
+    val format_name: String = roots_name
+    val file_ext = ""
+    override def detect(name: String): Boolean = name == roots_name
+
+    override def theory_suffix: String = "ROOTS_file"
+    override def theory_content(name: String): String =
+      """theory "ROOTS" imports Pure begin ROOTS_file """ +
+        Outer_Syntax.quote_string(name) + """ end"""
+  }
+
+
   /* base info and source dependencies */
 
   object Base