more markup;
authorwenzelm
Sat Dec 16 22:20:06 2017 +0100 (17 months ago)
changeset 672200049bed35f5a
parent 67219 81e9804b2014
child 67221 62a5fbdded50
more markup;
multiple error output;
src/Pure/Thy/sessions.ML
     1.1 --- a/src/Pure/Thy/sessions.ML	Sat Dec 16 21:53:07 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.ML	Sat Dec 16 22:20:06 2017 +0100
     1.3 @@ -42,13 +42,16 @@
     1.4    Parse.session_name --
     1.5    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
     1.6    Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
     1.7 -  (Parse.$$$ "=" |-- Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
     1.8 -    Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
     1.9 -    Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
    1.10 -    Scan.optional (Parse.$$$ "sessions" |-- Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
    1.11 -    Scan.repeat theories --
    1.12 -    Scan.repeat document_files))
    1.13 -  >> (fn (((session, _), dir), ((((((_, descr), options), _), theories), document_files))) =>
    1.14 +  (Parse.$$$ "=" |--
    1.15 +    Parse.!!! (Scan.option (Parse.position Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
    1.16 +      Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
    1.17 +      Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
    1.18 +      Scan.optional (Parse.$$$ "sessions" |--
    1.19 +        Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] --
    1.20 +      Scan.repeat theories --
    1.21 +      Scan.repeat document_files))
    1.22 +  >> (fn (((session, _), dir),
    1.23 +          ((((((parent, descr), options), sessions), theories), document_files))) =>
    1.24      Toplevel.keep (fn state =>
    1.25        let
    1.26          val ctxt = Toplevel.context_of state;
    1.27 @@ -56,13 +59,19 @@
    1.28          val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir;
    1.29  
    1.30          val _ =
    1.31 +          (the_list parent @ sessions) |> List.app (fn arg =>
    1.32 +            ignore (Resources.check_session ctxt arg)
    1.33 +              handle ERROR msg => Output.error_message msg);
    1.34 +
    1.35 +        val _ =
    1.36            Context_Position.report ctxt
    1.37              (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
    1.38              Markup.comment;
    1.39  
    1.40          val _ =
    1.41            (options @ maps #1 theories) |> List.app (fn (x, y) =>
    1.42 -            ignore (Completion.check_option_value ctxt x y (Options.default ())));
    1.43 +            ignore (Completion.check_option_value ctxt x y (Options.default ()))
    1.44 +              handle ERROR msg => Output.error_message msg);
    1.45  
    1.46          val _ =
    1.47            maps #2 theories |> List.app (fn (s, pos) =>