# HG changeset patch
# User wenzelm
# Date 1513459206 -3600
# Node ID 0049bed35f5aff09488d17802641550b79973783
# Parent  81e9804b201482469ae796402b7b840e597e12a4
more markup;
multiple error output;

diff -r 81e9804b2014 -r 0049bed35f5a src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Sat Dec 16 21:53:07 2017 +0100
+++ b/src/Pure/Thy/sessions.ML	Sat Dec 16 22:20:06 2017 +0100
@@ -42,13 +42,16 @@
   Parse.session_name --
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
   Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
-  (Parse.$$$ "=" |-- Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
-    Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
-    Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
-    Scan.optional (Parse.$$$ "sessions" |-- Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
-    Scan.repeat theories --
-    Scan.repeat document_files))
-  >> (fn (((session, _), dir), ((((((_, descr), options), _), theories), document_files))) =>
+  (Parse.$$$ "=" |--
+    Parse.!!! (Scan.option (Parse.position Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
+      Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
+      Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
+      Scan.optional (Parse.$$$ "sessions" |--
+        Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] --
+      Scan.repeat theories --
+      Scan.repeat document_files))
+  >> (fn (((session, _), dir),
+          ((((((parent, descr), options), sessions), theories), document_files))) =>
     Toplevel.keep (fn state =>
       let
         val ctxt = Toplevel.context_of state;
@@ -56,13 +59,19 @@
         val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir;
 
         val _ =
+          (the_list parent @ sessions) |> List.app (fn arg =>
+            ignore (Resources.check_session ctxt arg)
+              handle ERROR msg => Output.error_message msg);
+
+        val _ =
           Context_Position.report ctxt
             (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
             Markup.comment;
 
         val _ =
           (options @ maps #1 theories) |> List.app (fn (x, y) =>
-            ignore (Completion.check_option_value ctxt x y (Options.default ())));
+            ignore (Completion.check_option_value ctxt x y (Options.default ()))
+              handle ERROR msg => Output.error_message msg);
 
         val _ =
           maps #2 theories |> List.app (fn (s, pos) =>