equal
deleted
inserted
replaced
101 |
101 |
102 (* header args *) |
102 (* header args *) |
103 |
103 |
104 local |
104 local |
105 |
105 |
106 val imports = |
106 fun imports name = |
107 Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname)); |
107 if name = Context.PureN then Scan.succeed [] |
|
108 else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname)); |
108 |
109 |
109 val opt_files = |
110 val opt_files = |
110 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
111 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
111 |
112 |
112 val keyword_spec = |
113 val keyword_spec = |
126 |
127 |
127 in |
128 in |
128 |
129 |
129 val args = |
130 val args = |
130 Parse.position Parse.theory_name :|-- (fn (name, pos) => |
131 Parse.position Parse.theory_name :|-- (fn (name, pos) => |
131 (if name = Context.PureN then Scan.succeed [] else imports) -- |
132 imports name -- |
132 Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
133 Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
133 Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords)); |
134 Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords)); |
134 |
135 |
135 end; |
136 end; |
136 |
137 |