78 |
78 |
79 val file_name = Parse.group (fn () => "file name") Parse.path; |
79 val file_name = Parse.group (fn () => "file name") Parse.path; |
80 val theory_name = Parse.group (fn () => "theory name") Parse.name; |
80 val theory_name = Parse.group (fn () => "theory name") Parse.name; |
81 |
81 |
82 val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags); |
82 val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags); |
83 val keyword_decl = Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind); |
83 val keyword_decl = |
|
84 Scan.repeat1 Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >> |
|
85 (fn (names, kind) => map (rpair kind) names); |
|
86 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
84 |
87 |
85 val file = |
88 val file = |
86 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
89 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
87 file_name >> rpair true; |
90 file_name >> rpair true; |
88 |
91 |
89 in |
92 in |
90 |
93 |
91 val args = |
94 val args = |
92 theory_name -- |
95 theory_name -- |
93 (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) -- |
96 (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) -- |
94 Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! (Parse.and_list1 keyword_decl)) [] -- |
97 Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] -- |
95 Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| |
98 Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| |
96 Parse.$$$ beginN >> |
99 Parse.$$$ beginN >> |
97 (fn (((name, imports), keywords), uses) => make name imports keywords uses); |
100 (fn (((name, imports), keywords), uses) => make name imports keywords uses); |
98 |
101 |
99 end; |
102 end; |