# HG changeset patch # User wenzelm # Date 1237144754 -3600 # Node ID 5e2d9604a3d3b9e911baac9537a9ef6e38ff19b2 # Parent c96c72709a209d579e169fb87b54af2ae58bea7d export section, sections; tuned signature; diff -r c96c72709a20 -r 5e2d9604a3d3 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Mar 15 16:59:17 2009 +0100 +++ b/src/Pure/Isar/method.ML Sun Mar 15 20:19:14 2009 +0100 @@ -84,7 +84,9 @@ val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method val no_args: method -> src -> Proof.context -> method - type modifier + type modifier = (Proof.context -> Proof.context) * attribute + val section: modifier parser list -> thm list context_parser + val sections: modifier parser list -> thm list list context_parser val sectioned_args: 'a context_parser -> modifier parser list -> ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b val bang_sectioned_args: modifier parser list -> @@ -433,15 +435,15 @@ fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths); +in + fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- (fn (m, ths) => Scan.succeed (app m (context, ths)))); -fun sectioned args ss = args -- Scan.repeat (section ss); - -in +fun sections ss = Scan.repeat (section ss); fun sectioned_args args ss f src ctxt = - let val ((x, _), ctxt') = syntax (sectioned args ss) src ctxt + let val ((x, _), ctxt') = syntax (args -- sections ss) src ctxt in f x ctxt' end; fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;