equal
deleted
inserted
replaced
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 = |
83 val keyword_decl = |
84 Scan.repeat1 Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >> |
84 Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >> |
85 (fn (names, kind) => map (rpair kind) names); |
85 (fn (names, kind) => map (rpair kind) names); |
86 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
86 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
87 |
87 |
88 val file = |
88 val file = |
89 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
89 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |