40 |
40 |
41 val command_parser = |
41 val command_parser = |
42 Parse.session_name -- |
42 Parse.session_name -- |
43 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] -- |
43 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] -- |
44 Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) -- |
44 Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) -- |
45 (Parse.$$$ "=" |-- Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- |
45 (Parse.$$$ "=" |-- |
46 Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty -- |
46 Parse.!!! (Scan.option (Parse.position Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- |
47 Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] -- |
47 Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty -- |
48 Scan.optional (Parse.$$$ "sessions" |-- Parse.!!! (Scan.repeat1 Parse.session_name)) [] -- |
48 Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] -- |
49 Scan.repeat theories -- |
49 Scan.optional (Parse.$$$ "sessions" |-- |
50 Scan.repeat document_files)) |
50 Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] -- |
51 >> (fn (((session, _), dir), ((((((_, descr), options), _), theories), document_files))) => |
51 Scan.repeat theories -- |
|
52 Scan.repeat document_files)) |
|
53 >> (fn (((session, _), dir), |
|
54 ((((((parent, descr), options), sessions), theories), document_files))) => |
52 Toplevel.keep (fn state => |
55 Toplevel.keep (fn state => |
53 let |
56 let |
54 val ctxt = Toplevel.context_of state; |
57 val ctxt = Toplevel.context_of state; |
55 val thy = Toplevel.theory_of state; |
58 val thy = Toplevel.theory_of state; |
56 val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir; |
59 val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir; |
|
60 |
|
61 val _ = |
|
62 (the_list parent @ sessions) |> List.app (fn arg => |
|
63 ignore (Resources.check_session ctxt arg) |
|
64 handle ERROR msg => Output.error_message msg); |
57 |
65 |
58 val _ = |
66 val _ = |
59 Context_Position.report ctxt |
67 Context_Position.report ctxt |
60 (Position.range_position (Symbol_Pos.range (Input.source_explode descr))) |
68 (Position.range_position (Symbol_Pos.range (Input.source_explode descr))) |
61 Markup.comment; |
69 Markup.comment; |
62 |
70 |
63 val _ = |
71 val _ = |
64 (options @ maps #1 theories) |> List.app (fn (x, y) => |
72 (options @ maps #1 theories) |> List.app (fn (x, y) => |
65 ignore (Completion.check_option_value ctxt x y (Options.default ()))); |
73 ignore (Completion.check_option_value ctxt x y (Options.default ())) |
|
74 handle ERROR msg => Output.error_message msg); |
66 |
75 |
67 val _ = |
76 val _ = |
68 maps #2 theories |> List.app (fn (s, pos) => |
77 maps #2 theories |> List.app (fn (s, pos) => |
69 let |
78 let |
70 val {node_name, theory_name, ...} = |
79 val {node_name, theory_name, ...} = |