equal
deleted
inserted
replaced
182 | get_rules (Rule_Def.Sequence {rules, ...}) = rules |
182 | get_rules (Rule_Def.Sequence {rules, ...}) = rules |
183 | get_rules (Rule_Def.Rrls _) = []; |
183 | get_rules (Rule_Def.Rrls _) = []; |
184 |
184 |
185 fun id_from_rule _ (Rule.Rls_ rls) = id rls |
185 fun id_from_rule _ (Rule.Rls_ rls) = id rls |
186 | id_from_rule ctxt r = |
186 | id_from_rule ctxt r = |
187 raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r); |
187 raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string ctxt r); |
188 |
188 |
189 (* check if a rule is contained in a rule-set (recursivley down in Rls_); |
189 (* check if a rule is contained in a rule-set (recursivley down in Rls_); |
190 this rule can even be a rule-set itself *) |
190 this rule can even be a rule-set itself *) |
191 fun contains r rls = |
191 fun contains r rls = |
192 let |
192 let |