diff -r 54262af6d310 -r 736b8853189a src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Feb 27 13:37:04 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Feb 27 13:39:06 2021 +0100
@@ -48,6 +48,7 @@
   val check_path: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_file: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T
+  val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T
 end;
 
 structure Resources: RESOURCES =
@@ -387,6 +388,19 @@
 val check_file = formal_check File.check_file;
 val check_dir = formal_check File.check_dir;
 
+fun check_session_dir ctxt opt_dir s =
+  let
+    val dir = Path.expand (check_dir ctxt opt_dir s);
+    val ok =
+      File.is_file (dir + Path.explode("ROOT")) orelse
+      File.is_file (dir + Path.explode("ROOTS"));
+  in
+    if ok then dir
+    else
+      error ("Bad session root directory (missing ROOT or ROOTS): " ^
+        Path.print dir ^ Position.here (Input.pos_of s))
+  end;
+
 
 (* antiquotations *)