# HG changeset patch
# User haftmann
# Date 1131352491 -3600
# Node ID 227ecb2cfa3d7943d61b80e8115d464c283a6492
# Parent  d196d84c306f1400c9bb1130c78ded37fd982fb7
added fillin_mixfix' needed by serializer

diff -r d196d84c306f -r 227ecb2cfa3d src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Nov 06 01:21:37 2005 +0100
+++ b/src/Pure/codegen.ML	Mon Nov 07 09:34:51 2005 +0100
@@ -78,6 +78,7 @@
   val eval_result: term ref
   val eval_term: theory -> term -> term
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
+  val fillin_mixfix': 'a mixfix list -> Pretty.T list -> string list * Pretty.T
   val mk_deftab: theory -> deftab
 
   val get_node: codegr -> string -> node
@@ -552,7 +553,7 @@
 fun is_instance thy T1 T2 =
   Sign.typ_instance thy (T1, Type.varifyT T2);
 
-fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
+fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) =>
   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
 
 fun get_aux_code xs = List.mapPartial (fn (m, code) =>
@@ -634,6 +635,25 @@
   | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
       q :: pretty_mixfix module module' ms ps qs;
 
+fun fillin_mixfix' ms args =
+  let
+    fun fillin [] [] vars = (vars, [])
+      | fillin (Arg :: ms) [] vars =
+          let
+            val v = "a_" ^ (string_of_int o length) vars;
+          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 _ :: ms) args vars =
+          error ("no quotes currently supported in codegen patterns");
+  in fillin ms args [] ||> Pretty.block end;
+
 
 (**** default code generators ****)
 
@@ -811,7 +831,7 @@
     fun string_of_cycle (a :: b :: cs) =
           let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
             if a = a' then Option.map (pair x)
-              (find_first (equal b o #2 o Graph.get_node gr)
+              (Library.find_first (equal b o #2 o Graph.get_node gr)
                 (Graph.imm_succs gr x))
             else NONE) code
           in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end