changeset 50128 | 599c935aac82 |
parent 48992 | 0518bf89c777 |
child 51293 | 05b1bbae748d |
50127:ff0b52a6d72f | 50128:599c935aac82 |
---|---|
76 val usesN = "uses"; |
76 val usesN = "uses"; |
77 val beginN = "begin"; |
77 val beginN = "begin"; |
78 |
78 |
79 val header_lexicons = |
79 val header_lexicons = |
80 pairself (Scan.make_lexicon o map Symbol.explode) |
80 pairself (Scan.make_lexicon o map Symbol.explode) |
81 (["%", "(", ")", ",", "::", ";", "and", beginN, importsN, keywordsN, usesN], |
81 (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN, usesN], |
82 [headerN, theoryN]); |
82 [headerN, theoryN]); |
83 |
83 |
84 |
84 |
85 (* header args *) |
85 (* header args *) |
86 |
86 |
89 val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode; |
89 val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode; |
90 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); |
90 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); |
91 |
91 |
92 val opt_files = |
92 val opt_files = |
93 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
93 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
94 |
|
94 val keyword_spec = |
95 val keyword_spec = |
95 Parse.group (fn () => "outer syntax keyword specification") |
96 Parse.group (fn () => "outer syntax keyword specification") |
96 (Parse.name -- opt_files -- Parse.tags); |
97 (Parse.name -- opt_files -- Parse.tags); |
97 |
98 |
99 val keyword_compl = |
|
100 Parse.group (fn () => "outer syntax keyword completion") Parse.name; |
|
101 |
|
98 val keyword_decl = |
102 val keyword_decl = |
99 Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) >> |
103 Scan.repeat1 Parse.string -- |
100 (fn (names, spec) => map (rpair spec) names); |
104 Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) -- |
105 Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl) |
|
106 >> (fn ((names, spec), _) => map (rpair spec) names); |
|
107 |
|
101 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
108 val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
102 |
109 |
103 val file = |
110 val file = |
104 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
111 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
105 file_name >> rpair true; |
112 file_name >> rpair true; |