equal
deleted
inserted
replaced
110 |
110 |
111 val class_expr = plus1_unless locale_keyword P.xname; |
111 val class_expr = plus1_unless locale_keyword P.xname; |
112 |
112 |
113 val locale_expression = |
113 val locale_expression = |
114 let |
114 let |
115 fun expr2 x = P.xname x; |
115 val expr2 = P.xname; |
116 fun expr1 x = (Scan.optional prefix ("", false) -- expr2 -- |
116 val expr1 = Scan.optional prefix ("", false) -- expr2 -- |
117 Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; |
117 Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); |
118 fun expr0 x = (plus1_unless locale_keyword expr1) x; |
118 val expr0 = plus1_unless locale_keyword expr1; |
119 in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end; |
119 in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end; |
120 |
120 |
121 val context_element = P.group "context element" loc_element; |
121 val context_element = P.group "context element" loc_element; |
122 |
122 |
123 end; |
123 end; |