# HG changeset patch
# User wenzelm
# Date 1614429546 -3600
# Node ID 736b8853189a96b12980380ad92193c266b415ea
# Parent  54262af6d310f7d3e886462e76c9b1d8e2afe2f3
more checks;

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 *)
 
diff -r 54262af6d310 -r 736b8853189a src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Feb 27 13:37:04 2021 +0100
+++ b/src/Pure/Pure.thy	Sat Feb 27 13:39:06 2021 +0100
@@ -136,12 +136,13 @@
                 let
                   val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
                   val range = Position.range (pos1, pos2);
+                  val source = Input.source true line range;
                   val _ =
                     if line = "" then ()
                     else if String.isPrefix "#" line then
                       Context_Position.report ctxt (#1 range) Markup.comment
                     else
-                      (ignore (Resources.check_dir ctxt (SOME dir) (Input.source true line range))
+                      (ignore (Resources.check_session_dir ctxt (SOME dir) source)
                         handle ERROR msg => Output.error_message msg);
                 in pos2 |> Position.advance "\n" end);
           in thy' end)));