equal
deleted
inserted
replaced
109 >> (curry Element.Notes ""); |
109 >> (curry Element.Notes ""); |
110 |
110 |
111 fun plus1_unless test scan = |
111 fun plus1_unless test scan = |
112 scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); |
112 scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); |
113 |
113 |
114 val instance = Parse.where_ |-- |
114 val instance = Scan.optional (Parse.where_ |-- |
115 Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || |
115 Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || |
116 Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; |
116 Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional) (Expression.Named []) -- |
|
117 (Scan.optional (Parse.$$$ "replaces" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []); |
117 |
118 |
118 in |
119 in |
119 |
120 |
120 val locale_prefix = |
121 val locale_prefix = |
121 Scan.optional |
122 Scan.optional |
131 val locale_expression = |
132 val locale_expression = |
132 let |
133 let |
133 val expr2 = Parse.position Parse.name; |
134 val expr2 = Parse.position Parse.name; |
134 val expr1 = |
135 val expr1 = |
135 locale_prefix -- expr2 -- |
136 locale_prefix -- expr2 -- |
136 Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); |
137 instance >> (fn ((p, l), i) => (l, (p, i))); |
137 val expr0 = plus1_unless locale_keyword expr1; |
138 val expr0 = plus1_unless locale_keyword expr1; |
138 in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; |
139 in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; |
139 |
140 |
140 val context_element = Parse.group (fn () => "context element") loc_element; |
141 val context_element = Parse.group (fn () => "context element") loc_element; |
141 |
142 |