127 val thy = Context.theory_of context; |
127 val thy = Context.theory_of context; |
128 val (space, tab) = Attributes.get thy; |
128 val (space, tab) = Attributes.get thy; |
129 fun attr src = |
129 fun attr src = |
130 let val ((name, _), pos) = Args.dest_src src in |
130 let val ((name, _), pos) = Args.dest_src src in |
131 (case Symtab.lookup tab name of |
131 (case Symtab.lookup tab name of |
132 NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) |
132 NONE => error ("Unknown attribute: " ^ quote name ^ Position.here pos) |
133 | SOME (att, _) => |
133 | SOME (att, _) => |
134 (Context_Position.report_generic context pos (Name_Space.markup space name); att src)) |
134 (Context_Position.report_generic context pos (Name_Space.markup space name); att src)) |
135 end; |
135 end; |
136 in attr end; |
136 in attr end; |
137 |
137 |
252 val src2 = Args.closure src1; |
252 val src2 = Args.closure src1; |
253 in (src2, result) end; |
253 in (src2, result) end; |
254 |
254 |
255 fun err msg src = |
255 fun err msg src = |
256 let val ((name, _), pos) = Args.dest_src src |
256 let val ((name, _), pos) = Args.dest_src src |
257 in error (msg ^ " " ^ quote name ^ Position.str_of pos) end; |
257 in error (msg ^ " " ^ quote name ^ Position.here pos) end; |
258 |
258 |
259 fun eval src ((th, dyn), (decls, context)) = |
259 fun eval src ((th, dyn), (decls, context)) = |
260 (case (apply_att src (context, th), dyn) of |
260 (case (apply_att src (context, th), dyn) of |
261 ((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context)) |
261 ((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context)) |
262 | ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src |
262 | ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src |