# HG changeset patch
# User wenzelm
# Date 1553721336 -3600
# Node ID 93a95a24da82b3d7eb81f67ccc99f0a40908b53b
# Parent  76554a0cafe329c82d8145d79b01d3473669b5a1
tuned;

diff -r 76554a0cafe3 -r 93a95a24da82 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Mar 27 21:58:30 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Mar 27 22:15:36 2019 +0100
@@ -165,26 +165,21 @@
 
 local
 
-fun flat_modules selects width pretty_modules =
-  let val format = Code_Printer.format selects width in
-    (case pretty_modules of
-      Singleton (_, p) => format p
-    | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules))
-  end;
+fun flat_modules format pretty_modules =
+  (case pretty_modules of
+    Singleton (_, p) => format p
+  | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules));
 
-fun export_to_file root width pretty_modules =
-  let val format = Code_Printer.format [] width in
-    (case pretty_modules of
-      Singleton (_, p) => File.write root (format p)
-    | Hierarchy code_modules =>
-        (Isabelle_System.mkdirs root;
-          List.app (fn (names, p) =>
-            File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules))
-  end;
+fun export_to_file root format pretty_modules =
+  (case pretty_modules of
+    Singleton (_, p) => File.write root (format p)
+  | Hierarchy code_modules =>
+      (Isabelle_System.mkdirs root;
+        List.app (fn (names, p) =>
+          File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
 
-fun export_to_exports width pretty_modules =
+fun export_to_exports format pretty_modules =
   let
-    val format = Code_Printer.format [] width;
     fun export name content thy = (Export.export thy name [content]; thy);
   in
     (case pretty_modules of
@@ -194,28 +189,31 @@
 
 in
 
-fun export_result some_file width (pretty_code, _) thy =
+fun export_result some_file format (pretty_code, _) thy =
   (case some_file of
     NONE =>
       let
-        val thy' = export_to_exports width pretty_code thy;
+        val thy' = export_to_exports format pretty_code thy;
         val _ = writeln (Export.message thy' "");
       in thy' end
-  | SOME NONE => (writeln (flat_modules [] width pretty_code); thy)
+  | SOME NONE => (writeln (flat_modules format pretty_code); thy)
   | SOME (SOME relative_root) =>
       let
         val root = File.full_path (Resources.master_directory thy) relative_root;
         val _ = File.check_dir (Path.dir root);
-        val _ = export_to_file root width pretty_code;
+        val _ = export_to_file root format pretty_code;
       in thy end);
 
-fun produce_result syms width (Singleton (_, p), deresolve) =
-      ([([], Code_Printer.format [] width p)], map deresolve syms)
-  | produce_result syms width (Hierarchy code_modules, deresolve) =
-      ((map o apsnd) (Code_Printer.format [] width) code_modules, map deresolve syms);
+fun produce_result syms width pretty_modules =
+  let val format = Code_Printer.format [] width in
+    (case pretty_modules of
+      (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms)
+    | (Hierarchy code_modules, deresolve) =>
+        ((map o apsnd) format code_modules, map deresolve syms))
+  end;
 
 fun present_result selects width (pretty_code, _) =
-  flat_modules selects width pretty_code;
+  flat_modules (Code_Printer.format selects width) pretty_code;
 
 end;
 
@@ -404,9 +402,9 @@
 fun export_code_for some_file target_name module_name some_width args program all_public cs thy =
   let
     val thy_ctxt = Proof_Context.init_global thy;
-    val width = the_width thy_ctxt some_width;
+    val format = Code_Printer.format [] (the_width thy_ctxt some_width);
     val res = invoke_serializer thy_ctxt target_name module_name args program all_public cs;
-  in export_result some_file width res thy end;
+  in export_result some_file format res thy end;
 
 fun produce_code_for ctxt target_name module_name some_width args =
   let
@@ -427,11 +425,12 @@
   let
     val thy_ctxt = Proof_Context.init_global thy;
     val { env_var, make_destination, make_command } = #check (the_language thy_ctxt target_name);
+    val format = Code_Printer.format [] 80;
     fun ext_check p =
       let
         val destination = make_destination p;
         val thy' =
-          export_result (SOME (SOME destination)) 80
+          export_result (SOME (SOME destination)) format
             (invoke_serializer thy_ctxt target_name generatedN args program all_public syms) thy;
         val cmd = make_command generatedN;
         val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";