# HG changeset patch
# User berghofe
# Date 1064240163 -7200
# Node ID 3d7c6fc7c66e3fed35313c3a1641b3c08db43255
# Parent  be5e838f37bd2e7af7d136d4886d7ce3708c2a15
add_attribute now takes parser as argument.

diff -r be5e838f37bd -r 3d7c6fc7c66e src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Sep 22 16:14:58 2003 +0200
+++ b/src/Pure/codegen.ML	Mon Sep 22 16:16:03 2003 +0200
@@ -23,7 +23,7 @@
 
   val add_codegen: string -> term codegen -> theory -> theory
   val add_tycodegen: string -> typ codegen -> theory -> theory
-  val add_attribute: string -> theory attribute -> theory -> theory
+  val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory
   val print_codegens: theory -> unit
   val generate_code: theory -> (string * string) list -> string
   val generate_code_i: theory -> (string * term) list -> string
@@ -133,7 +133,7 @@
      tycodegens : (string * typ codegen) list,
      consts : ((string * typ) * term mixfix list) list,
      types : (string * typ mixfix list) list,
-     attrs: (string * theory attribute) list,
+     attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
      test_params: test_params};
 
   val empty =
@@ -214,11 +214,11 @@
     | Some _ => error ("Code attribute " ^ name ^ " already declared"))
   end;
 
+fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
+
 val code_attr =
-  Attrib.syntax (Scan.depend (fn thy => Scan.optional Args.name "" >>
-    (fn name => (thy, case assoc (#attrs (CodegenData.get thy), name) of
-          None => error ("Unknown code attribute: " ^ quote name)
-        | Some att => att)))); 
+  Attrib.syntax (Scan.depend (fn thy => foldr op || (map mk_parser
+    (#attrs (CodegenData.get thy)), Scan.fail) >> pair thy));
 
 
 (**** associate constants with target language code ****)