# HG changeset patch
# User haftmann
# Date 1212060433 -7200
# Node ID a5f53d9d2b604af9b59da8c5a7437d6efdcad892
# Parent  12795abea6b69c8bef6b74402ec8e0849250f413
yet another attempt to circumvent printmode problems

diff -r 12795abea6b6 -r a5f53d9d2b60 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Wed May 28 23:44:43 2008 +0200
+++ b/src/Tools/code/code_package.ML	Thu May 29 13:27:13 2008 +0200
@@ -7,6 +7,7 @@
 
 signature CODE_PACKAGE =
 sig
+  val source_of: theory -> string -> string -> string list -> string;
   val evaluate_conv: theory
     -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
        -> string list -> thm))
@@ -105,6 +106,18 @@
       (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris;
   in () end;
 
+(* code retrieval *)
+
+fun source_of thy target module_name cs =
+  let
+    val (cs', _) = generate thy (CodeFuncgr.make thy cs)
+      (fold_map ooo ensure_const) cs;
+    val code = Program.get thy;
+  in
+    CodeTarget.string
+      (CodeTarget.serialize thy target false (SOME module_name) [] code (SOME cs'))
+  end;
+
 (* evaluation machinery *)
 
 fun evaluate eval_kind thy evaluator =
diff -r 12795abea6b6 -r a5f53d9d2b60 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Wed May 28 23:44:43 2008 +0200
+++ b/src/Tools/code/code_target.ML	Thu May 29 13:27:13 2008 +0200
@@ -66,10 +66,20 @@
 fun enum_default default sep opn cls [] = str default
   | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
 
+datatype serialization_dest = Compile | Write | File of Path.T | String;
+type serialization = serialization_dest -> string option;
+
 val code_width = ref 80;
-fun code_source p = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) Pretty.string_of) p ^ "\n";
+fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
+fun code_source p = code_setmp Pretty.string_of p ^ "\n";
 fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
 
+(*FIXME why another code_setmp?*)
+fun compile f = (code_setmp f Compile; ());
+fun write f = (code_setmp f Write; ());
+fun file p f = (code_setmp f (File p); ());
+fun string f = the (code_setmp f String);
+
 
 (** generic syntax **)
 
@@ -142,14 +152,6 @@
        Symtab.join (K snd) (const1, const2))
   );
 
-datatype serialization_dest = Compile | Write | File of Path.T | String;
-type serialization = serialization_dest -> string option;
-
-fun compile f = (f Compile; ());
-fun write f = (f Write; ());
-fun file p f = (f (File p); ());
-fun string f = the (f String);
-
 type serializer =
   string option
   -> Args.T list