# HG changeset patch
# User haftmann
# Date 1547122025 0
# Node ID ef02c5e051e57fa454028b2dda38a9e1327f4258
# Parent  00347595559372a7f5dfd8998b234c0b9f608f83
explicit model concerning files of generated code

diff -r 003475955593 -r ef02c5e051e5 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/HOL/Library/code_test.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -164,7 +164,9 @@
       | SOME f => f)
     val debug = Config.get (Proof_Context.init_global thy) overlord
     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
-    fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
+    fun evaluate result =
+      with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
+      |> parse_result compiler
     fun evaluator program _ vs_ty deps =
       Exn.interruptible_capture evaluate
         (Code_Target.compilation_text ctxt target program deps true vs_ty)
diff -r 003475955593 -r ef02c5e051e5 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -233,13 +233,17 @@
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
     fun run in_path =
       let
-        fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
+        fun mk_code_file module =
+          let
+            val (paths, base) = split_last module
+          in Path.appends (in_path :: map Path.basic (paths @ [base ^ ".hs"])) end;
         val generatedN = Code_Target.generatedN
-        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file
-        val code = the (AList.lookup (op =) code_modules generatedN)
-        val code_file = mk_code_file generatedN
-        val narrowing_engine_file = mk_code_file "Narrowing_Engine"
-        val main_file = mk_code_file "Main"
+        val includes = AList.delete (op =) [generatedN] code_modules
+          |> (map o apfst) mk_code_file
+        val code = the (AList.lookup (op =) code_modules [generatedN])
+        val code_file = mk_code_file [generatedN]
+        val narrowing_engine_file = mk_code_file ["Narrowing_Engine"]
+        val main_file = mk_code_file ["Main"]
         val main =
           "module Main where {\n\n" ^
           "import System.IO;\n" ^
diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/Tools/Code/code_haskell.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -331,7 +331,7 @@
 ];
 
 fun serialize_haskell module_prefix string_classes ctxt { module_name,
-    reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } exports program =
+    reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
   let
 
     (* build program *)
@@ -357,9 +357,14 @@
       deresolve (if string_classes then deriving_show else K false);
 
     (* print modules *)
-    fun print_module_frame module_name exports ps =
-      (module_name, Pretty.chunks2 (
-        concat [str "module",
+    fun module_names module_name =
+      let
+        val (xs, x) = split_last (Long_Name.explode module_name)
+      in xs @ [x ^ ".hs"] end
+    fun print_module_frame module_name header exports ps =
+      (module_names module_name, Pretty.chunks2 (
+        header
+        @ concat [str "module",
           case exports of
             SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
           | NONE => str module_name,
@@ -397,30 +402,14 @@
           |> split_list
           |> apfst (map_filter I);
       in
-        print_module_frame module_name (SOME export_ps)
+        print_module_frame module_name [str language_pragma] (SOME export_ps)
           ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
       end;
 
-    (*serialization*)
-    fun write_module width (SOME destination) (module_name, content) =
-          let
-            val _ = File.check_dir destination;
-            val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
-              o separate "/" o Long_Name.explode) module_name;
-            val _ = Isabelle_System.mkdirs (Path.dir filepath);
-          in
-            (File.write filepath o format [] width o Pretty.chunks2)
-              [str language_pragma, content]
-          end
-      | write_module width NONE (_, content) = writeln (format [] width content);
   in
-    Code_Target.serialization
-      (fn width => fn destination => K () o map (write_module width destination))
-      (fn present => fn width => rpair (try (deresolver ""))
-        o (map o apsnd) (format present width))
-      (map (fn (module_name, content) => print_module_frame module_name NONE [content]) includes
-        @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
-          ((flat o rev o Graph.strong_conn) haskell_program))
+    (Code_Target.Hierarchy (map (fn (module_name, content) => print_module_frame module_name [] NONE [content]) includes
+      @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
+        ((flat o rev o Graph.strong_conn) haskell_program)), try (deresolver ""))
   end;
 
 val serializer : Code_Target.serializer =
diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/Tools/Code/code_ml.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -827,9 +827,9 @@
       memorize_data = K I, modify_stmts = modify_stmts }
   end;
 
-fun serialize_ml print_ml_module print_ml_stmt ctxt
+fun serialize_ml print_ml_module print_ml_stmt ml_extension ctxt
     { module_name, reserved_syms, identifiers, includes,
-      class_syntax, tyco_syntax, const_syntax } exports program =
+      class_syntax, tyco_syntax, const_syntax } program exports =
   let
 
     (* build program *)
@@ -855,18 +855,15 @@
       @ map snd (Code_Namespace.print_hierarchical {
         print_module = print_module, print_stmt = print_stmt,
         lift_markup = apsnd } ml_program));
-    fun write width NONE = writeln o format [] width
-      | write width (SOME p) = File.write p o format [] width;
-    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
   in
-    Code_Target.serialization write prepare p
+    (Code_Target.Singleton (ml_extension, p), try (deresolver []))
   end;
 
 val serializer_sml : Code_Target.serializer =
-  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt);
+  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt "ML");
 
 val serializer_ocaml : Code_Target.serializer =
-  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt);
+  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt "ocaml");
 
 
 (** Isar setup **)
diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -437,7 +437,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val (ml_modules, target_names) =
       Code_Target.produce_code_for ctxt
-        target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
+        target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos);
     val ml_code = space_implode "\n\n" (map snd ml_modules);
     val (consts', tycos') = chop (length consts) target_names;
     val consts_map = map2 (fn const =>
@@ -856,7 +856,7 @@
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
-  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN []));
+  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE []));
 
 fun process_file filepath (definienda, thy) =
   let
diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/Tools/Code/code_scala.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -402,7 +402,7 @@
   end;
 
 fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers,
-    includes, class_syntax, tyco_syntax, const_syntax } exports program =
+    includes, class_syntax, tyco_syntax, const_syntax } program exports =
   let
 
     (* build program *)
@@ -438,11 +438,8 @@
       @ Code_Namespace.print_hierarchical {
         print_module = print_module, print_stmt = print_stmt,
         lift_markup = I } scala_program);
-    fun write width NONE = writeln o format [] width
-      | write width (SOME p) = File.write p o format [] width;
-    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
   in
-    Code_Target.serialization write prepare p
+    (Code_Target.Singleton ("scala", p), try (deresolver []))
   end;
 
 val serializer : Code_Target.serializer =
diff -r 003475955593 -r ef02c5e051e5 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -9,11 +9,13 @@
   val cert_tyco: Proof.context -> string -> string
   val read_tyco: Proof.context -> string -> string
 
-  val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
+  datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
+
+  val export_code_for: Proof.context -> Path.T option -> string -> string -> int option -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
-  val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
-    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
-  val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
+  val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
+    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
+  val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
     -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
   val check_code_for: Proof.context -> string -> bool -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
@@ -21,19 +23,19 @@
   val export_code: Proof.context -> bool -> string list
     -> (((string * string) * Path.T option) * Token.T list) list -> unit
   val produce_code: Proof.context -> bool -> string list
-    -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
+    -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
   val present_code: Proof.context -> string list -> Code_Symbol.T list
-    -> string -> int option -> string -> Token.T list -> string
+    -> string -> string -> int option -> Token.T list -> string
   val check_code: Proof.context -> bool -> string list
     -> ((string * bool) * Token.T list) list -> unit
 
   val generatedN: string
   val compilation_text: Proof.context -> string -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> (string * string) list * string
+    -> (string list * string) list * string
   val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> ((string * string) list * string) * (Code_Symbol.T -> string option)
+    -> ((string list * string) list * string) * (Code_Symbol.T -> string option)
 
   type serializer
   type literals = Code_Printer.literals
@@ -43,11 +45,7 @@
   val add_language: string * language -> theory -> theory
   val add_derived_target: string * ancestry -> theory -> theory
   val the_literals: Proof.context -> string -> literals
-  type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
-  val serialization: (int -> Path.T option -> 'a -> unit)
-    -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
-    -> 'a -> serialization
   val default_code_width: int Config.T
 
   type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
@@ -146,44 +144,54 @@
   end;
 
 
-(** serializations and serializer **)
-
-(* serialization: abstract nonsense to cover different destinies for generated code *)
-
-datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
-type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
+(** serializers **)
 
-fun serialization output _ content width (Export some_path) =
-      (output width some_path content; NONE)
-  | serialization _ string content width Produce =
-      string [] width content |> SOME
-  | serialization _ string content width (Present syms) =
-     string syms width content
-     |> (apfst o map o apsnd) Output.output
-     |> SOME;
-
-fun export some_path f = (f (Export some_path); ());
-fun produce f = the (f Produce);
-fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
-
-
-(* serializers: functions producing serializations *)
+datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
 
 type serializer = Token.T list
   -> Proof.context
   -> {
-    module_name: string,
     reserved_syms: string list,
     identifiers: Code_Printer.identifiers,
     includes: (string * Pretty.T) list,
     class_syntax: string -> string option,
     tyco_syntax: string -> Code_Printer.tyco_syntax option,
-    const_syntax: string -> Code_Printer.const_syntax option }
-  -> Code_Symbol.T list
+    const_syntax: string -> Code_Printer.const_syntax option,
+    module_name: string }
   -> Code_Thingol.program
-  -> serialization;
+  -> Code_Symbol.T list
+  -> pretty_modules * (Code_Symbol.T -> string option);
+
+fun flat_modules selects width (Singleton (_, p)) =
+      Code_Printer.format selects width p
+  | flat_modules selects width (Hierarchy code_modules) =
+      space_implode "\n\n" (map (Code_Printer.format selects width o snd) code_modules);
+
+fun export_to_file root width (Singleton (_, p)) =
+      File.write root (Code_Printer.format [] width p)
+  | export_to_file root width (Hierarchy code_modules) = (
+      Isabelle_System.mkdirs root;
+      map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules;
+      ());
 
-  
+fun export_result ctxt some_root width (pretty_code, _) =
+  case some_root of
+    NONE => (writeln (flat_modules [] width pretty_code); ())
+  | SOME relative_root =>
+      let
+        val root = File.full_path (Resources.master_directory (Proof_Context.theory_of ctxt)) relative_root;
+        val _ = File.check_dir (Path.dir root);
+      in export_to_file root width pretty_code 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 present_result selects width (pretty_code, _) =
+  flat_modules selects width pretty_code;
+
+
 (** theory data **)
 
 type language = {serializer: serializer, literals: literals,
@@ -232,7 +240,7 @@
     val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
   in (modify, (target, data)) end;
 
-  fun allocate_target target_name target thy =
+fun allocate_target target_name target thy =
   let
     val _ = if exists_target thy target_name
       then error ("Attempt to overwrite existing target " ^ quote target_name)
@@ -287,6 +295,10 @@
 
 val default_code_width = Attrib.setup_config_int \<^binding>\<open>default_code_width\<close> (K 80);
 
+fun default_width ctxt = Config.get ctxt default_code_width;
+
+val the_width = the_default o default_width;
+
 
 (* montage *)
 
@@ -302,10 +314,11 @@
 fun activate_target ctxt target_name =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val (modify, target_data) = join_ancestry thy target_name;
-  in (target_data, modify) end;
+    val (modify, (target, data)) = join_ancestry thy target_name;
+    val serializer = (#serializer o #language) target;
+  in { serializer = serializer, data = data, modify = modify } end;
 
-fun project_program ctxt syms_hidden syms1 program1 =
+fun project_program_for_syms ctxt syms_hidden syms1 program1 =
   let
     val syms2 = subtract (op =) syms_hidden syms1;
     val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
@@ -318,78 +331,70 @@
     val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
   in program3 end;
 
-fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
-    printings module_name args proto_program syms =
+fun project_includes_for_syms syms includes =
+   let
+     fun select_include (name, (content, cs)) =
+       if null cs orelse exists (member (op =) syms) cs
+       then SOME (name, content) else NONE;
+  in map_filter select_include includes end;
+
+fun prepare_serializer ctxt target_name module_name args proto_program syms =
   let
-    val syms_hidden = Code_Symbol.symbols_of printings;
-    val program = project_program ctxt syms_hidden syms proto_program;
-    val syms_all = Code_Symbol.Graph.all_succs proto_program syms;
-    fun select_include (name, (content, syms)) =
-      if null syms orelse exists (member (op =) syms_all) syms
-      then SOME (name, content) else NONE;
-    val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
-  in
-    (serializer args ctxt {
-      module_name = module_name,
-      reserved_syms = reserved,
-      identifiers = identifiers,
+    val { serializer, data, modify } = activate_target ctxt target_name;
+    val printings = Code_Printer.the_printings data;
+    val _ = if module_name = "" then () else (check_name true module_name; ())
+    val hidden_syms = Code_Symbol.symbols_of printings;
+    val prepared_program = project_program_for_syms ctxt hidden_syms syms proto_program;
+    val prepared_syms = subtract (op =) hidden_syms syms;
+    val all_syms = Code_Symbol.Graph.all_succs proto_program syms;
+    val includes = project_includes_for_syms all_syms
+      (Code_Symbol.dest_module_data printings);
+    val prepared_serializer = serializer args ctxt {
+      reserved_syms = Code_Printer.the_reserved data,
+      identifiers = Code_Printer.the_identifiers data,
       includes = includes,
       const_syntax = Code_Symbol.lookup_constant_data printings,
       tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
-      class_syntax = Code_Symbol.lookup_type_class_data printings },
-      (subtract (op =) syms_hidden syms, program))
+      class_syntax = Code_Symbol.lookup_type_class_data printings,
+      module_name = module_name };
+  in
+    (prepared_serializer o modify, (prepared_program, prepared_syms))
   end;
 
-fun mount_serializer ctxt target_name some_width module_name args program syms =
+fun invoke_serializer ctxt target_name module_name args program all_public syms =
   let
-    val default_width = Config.get ctxt default_code_width;
-    val ((target, data), modify) = activate_target ctxt target_name;
-    val serializer = (#serializer o #language) target;
-    val (prepared_serializer, (prepared_syms, prepared_program)) =
-      prepare_serializer ctxt serializer
-        (Code_Printer.the_reserved data) (Code_Printer.the_identifiers data)
-        (Code_Printer.the_printings data)
-        module_name args (modify program) syms
-    val width = the_default default_width some_width;
-  in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
-
-fun invoke_serializer ctxt target_name some_width raw_module_name args program all_public syms =
-  let
-    val module_name = if raw_module_name = "" then ""
-      else (check_name true raw_module_name; raw_module_name)
-    val (mounted_serializer, (prepared_syms, prepared_program)) =
-      mount_serializer ctxt target_name some_width module_name args program syms;
+    val (prepared_serializer, (prepared_program, prepared_syms)) =
+      prepare_serializer ctxt target_name module_name args program syms;
+    val exports = if all_public then [] else prepared_syms;
   in
     Code_Preproc.timed_exec "serializing"
-      (fn () => mounted_serializer prepared_program (if all_public then [] else prepared_syms)) ctxt
+      (fn () => prepared_serializer prepared_program exports) ctxt
   end;
 
 fun assert_module_name "" = error "Empty module name not allowed here"
   | assert_module_name module_name = module_name;
 
-val using_master_directory =
-  Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
-
 in
 
 val generatedN = "Generated_Code";
 
-fun export_code_for ctxt some_path target_name some_width module_name args =
-  export (using_master_directory ctxt some_path)
-  ooo invoke_serializer ctxt target_name some_width module_name args;
+fun export_code_for ctxt some_root target_name module_name some_width args =
+  export_result ctxt some_root (the_width ctxt some_width)
+  ooo invoke_serializer ctxt target_name module_name args;
 
-fun produce_code_for ctxt target_name some_width module_name args =
+fun produce_code_for ctxt target_name module_name some_width args =
   let
-    val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
+    val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
   in fn program => fn all_public => fn syms =>
-    produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
+    produce_result syms (the_width ctxt some_width)
+      (serializer program all_public syms)
   end;
 
-fun present_code_for ctxt target_name some_width module_name args =
+fun present_code_for ctxt target_name module_name some_width args =
   let
-    val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
+    val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
   in fn program => fn (syms, selects) =>
-    present selects (serializer program false syms)
+    present_result selects (the_width ctxt some_width) (serializer program false syms)
   end;
 
 fun check_code_for ctxt target_name strict args program all_public syms =
@@ -399,8 +404,8 @@
     fun ext_check p =
       let
         val destination = make_destination p;
-        val _ = export (SOME destination) (invoke_serializer ctxt target_name (SOME 80)
-          generatedN args program all_public syms);
+        val _ = export_result ctxt (SOME destination) 80
+          (invoke_serializer ctxt target_name generatedN args program all_public syms)
         val cmd = make_command generatedN;
       in
         if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
@@ -415,7 +420,7 @@
     else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
-fun dynamic_compilation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
+fun dynamic_compilation_text prepared_serializer width prepared_program syms all_public ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
@@ -427,19 +432,21 @@
           Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE))
       |> fold (curry (perhaps o try o
           Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
-    val (program_code, deresolve) =
-      produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
-    val value_name = the (deresolve Code_Symbol.value);
-  in ((program_code, value_name), deresolve) end;
+    val (pretty_code, deresolve) =
+      prepared_serializer program (if all_public then [] else [Code_Symbol.value]);
+    val (compilation_code, [SOME value_name]) =
+      produce_result [Code_Symbol.value] width (pretty_code, deresolve);
+  in ((compilation_code, value_name), deresolve) end;
 
 fun compilation_text' ctxt target_name some_module_name program syms =
   let
+    val width = default_width ctxt;
     val evaluation_args = the_evaluation_args ctxt target_name;
-    val (mounted_serializer, (_, prepared_program)) =
-      mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) evaluation_args program syms;
+    val (prepared_serializer, (prepared_program, _)) =
+      prepare_serializer ctxt target_name (the_default generatedN some_module_name) evaluation_args program syms;
   in
     Code_Preproc.timed_exec "serializing"
-    (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt
+      (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt
   end;
 
 fun compilation_text ctxt target_name program syms =
@@ -462,8 +469,8 @@
 fun export_code ctxt all_public cs seris =
   let
     val program = Code_Thingol.consts_program ctxt cs;
-    val _ = map (fn (((target_name, module_name), some_path), args) =>
-      export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
+    val _ = map (fn (((target_name, module_name), some_root), args) =>
+      export_code_for ctxt some_root target_name module_name NONE args program all_public (map Constant cs)) seris;
   in () end;
 
 fun export_code_cmd all_public raw_cs seris ctxt =
@@ -523,11 +530,11 @@
     (parse_const_terms --
       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
-    (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
+    (fn ctxt => fn ((read_constants, reads_statements), (target_name, some_width)) =>
       Latex.string
-        (present_code ctxt (mk_cs ctxt)
-          (maps (fn f => f ctxt) mk_stmtss)
-          target_name some_width "Example" [])));
+        (Latex.output_ascii (present_code ctxt (read_constants ctxt)
+          (maps (fn read_statements => read_statements ctxt) reads_statements)
+          target_name "Example" some_width []))));
 
 end;