equal
deleted
inserted
replaced
115 |
115 |
116 local |
116 local |
117 |
117 |
118 fun imports name = |
118 fun imports name = |
119 if name = Context.PureN then Scan.succeed [] |
119 if name = Context.PureN then Scan.succeed [] |
120 else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname)); |
120 else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name)); |
121 |
121 |
122 val opt_files = |
122 val opt_files = |
123 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
123 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
124 |
124 |
125 val keyword_spec = |
125 val keyword_spec = |