--- 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) =>