equal
deleted
inserted
replaced
82 |
82 |
83 local |
83 local |
84 |
84 |
85 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); |
85 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); |
86 |
86 |
|
87 val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name); |
|
88 |
87 val opt_files = |
89 val opt_files = |
88 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
90 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
89 |
91 |
90 val keyword_spec = |
92 val keyword_spec = |
91 Parse.group (fn () => "outer syntax keyword specification") |
93 Parse.group (fn () => "outer syntax keyword specification") |
103 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
105 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
104 |
106 |
105 in |
107 in |
106 |
108 |
107 val args = |
109 val args = |
108 theory_name -- |
110 theory_name :|-- (fn (name, pos) => |
109 Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] -- |
111 (if name = Context.PureN then Scan.succeed [] else imports) -- |
110 Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
112 Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
111 Parse.$$$ beginN >> |
113 Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords)); |
112 (fn ((name, imports), keywords) => make name imports keywords); |
|
113 |
114 |
114 end; |
115 end; |
115 |
116 |
116 |
117 |
117 (* read header *) |
118 (* read header *) |