--- a/src/Pure/codegen.ML Mon Nov 07 11:39:24 2005 +0100
+++ b/src/Pure/codegen.ML Mon Nov 07 12:06:11 2005 +0100
@@ -80,7 +80,7 @@
val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
val quotes_of: 'a mixfix list -> 'a list
val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
- val fillin_mixfix: 'a mixfix list -> Pretty.T list -> Pretty.T list -> string list * Pretty.T
+ val fillin_mixfix: 'a mixfix list -> Pretty.T list -> ('a -> Pretty.T) -> string list * Pretty.T
val mk_deftab: theory -> deftab
val get_node: codegr -> string -> node
@@ -649,24 +649,24 @@
| replace_quotes (x::xs) (Quote _ :: ms) =
Quote x :: replace_quotes xs ms;
-fun fillin_mixfix ms args qs =
+fun fillin_mixfix ms args f =
let
- fun fillin [] [] [] vars = (vars, [])
- | fillin (Arg :: ms) [] qs vars =
+ fun fillin [] [] vars = (vars, [])
+ | fillin (Arg :: ms) [] vars =
let
val v = "a_" ^ (string_of_int o length) vars;
- in fillin ms args qs (v::vars) ||> (cons o Pretty.str) v end
- | fillin (Arg :: ms) (a :: args) qs vars =
- fillin ms args qs vars ||> cons a
- | fillin (Ignore :: ms) args qs vars =
- fillin ms args qs vars
- | fillin (Module :: ms) args qs vars =
- fillin ms args qs vars
- | fillin (Pretty p :: ms) args qs vars =
- fillin ms args qs vars ||> cons p
- | fillin (Quote _ :: ms) args (q::qs) vars =
- fillin ms args qs vars ||> cons q
- in fillin ms args qs [] ||> Pretty.block end;
+ in fillin ms args (v::vars) ||> (cons o Pretty.str) v end
+ | fillin (Arg :: ms) (a :: args) vars =
+ fillin ms args vars ||> cons a
+ | fillin (Ignore :: ms) args vars =
+ fillin ms args vars
+ | fillin (Module :: ms) args vars =
+ fillin ms args vars
+ | fillin (Pretty p :: ms) args vars =
+ fillin ms args vars ||> cons p
+ | fillin (Quote q :: ms) args vars =
+ fillin ms args vars ||> cons (f q)
+ in fillin ms args [] ||> Pretty.block end;
(**** default code generators ****)