explicit model concerning files of generated code
authorhaftmann
Thu Jan 10 12:07:05 2019 +0000 (6 months ago)
changeset 69623ef02c5e051e5
parent 69622 003475955593
child 69624 e02bdf853a4c
explicit model concerning files of generated code
src/HOL/Library/code_test.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Mon Jan 07 18:50:41 2019 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Thu Jan 10 12:07:05 2019 +0000
     1.3 @@ -164,7 +164,9 @@
     1.4        | SOME f => f)
     1.5      val debug = Config.get (Proof_Context.init_global thy) overlord
     1.6      val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
     1.7 -    fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
     1.8 +    fun evaluate result =
     1.9 +      with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
    1.10 +      |> parse_result compiler
    1.11      fun evaluator program _ vs_ty deps =
    1.12        Exn.interruptible_capture evaluate
    1.13          (Code_Target.compilation_text ctxt target program deps true vs_ty)
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jan 07 18:50:41 2019 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jan 10 12:07:05 2019 +0000
     2.3 @@ -233,13 +233,17 @@
     2.4        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
     2.5      fun run in_path =
     2.6        let
     2.7 -        fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
     2.8 +        fun mk_code_file module =
     2.9 +          let
    2.10 +            val (paths, base) = split_last module
    2.11 +          in Path.appends (in_path :: map Path.basic (paths @ [base ^ ".hs"])) end;
    2.12          val generatedN = Code_Target.generatedN
    2.13 -        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file
    2.14 -        val code = the (AList.lookup (op =) code_modules generatedN)
    2.15 -        val code_file = mk_code_file generatedN
    2.16 -        val narrowing_engine_file = mk_code_file "Narrowing_Engine"
    2.17 -        val main_file = mk_code_file "Main"
    2.18 +        val includes = AList.delete (op =) [generatedN] code_modules
    2.19 +          |> (map o apfst) mk_code_file
    2.20 +        val code = the (AList.lookup (op =) code_modules [generatedN])
    2.21 +        val code_file = mk_code_file [generatedN]
    2.22 +        val narrowing_engine_file = mk_code_file ["Narrowing_Engine"]
    2.23 +        val main_file = mk_code_file ["Main"]
    2.24          val main =
    2.25            "module Main where {\n\n" ^
    2.26            "import System.IO;\n" ^
     3.1 --- a/src/Tools/Code/code_haskell.ML	Mon Jan 07 18:50:41 2019 +0100
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jan 10 12:07:05 2019 +0000
     3.3 @@ -331,7 +331,7 @@
     3.4  ];
     3.5  
     3.6  fun serialize_haskell module_prefix string_classes ctxt { module_name,
     3.7 -    reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } exports program =
     3.8 +    reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
     3.9    let
    3.10  
    3.11      (* build program *)
    3.12 @@ -357,9 +357,14 @@
    3.13        deresolve (if string_classes then deriving_show else K false);
    3.14  
    3.15      (* print modules *)
    3.16 -    fun print_module_frame module_name exports ps =
    3.17 -      (module_name, Pretty.chunks2 (
    3.18 -        concat [str "module",
    3.19 +    fun module_names module_name =
    3.20 +      let
    3.21 +        val (xs, x) = split_last (Long_Name.explode module_name)
    3.22 +      in xs @ [x ^ ".hs"] end
    3.23 +    fun print_module_frame module_name header exports ps =
    3.24 +      (module_names module_name, Pretty.chunks2 (
    3.25 +        header
    3.26 +        @ concat [str "module",
    3.27            case exports of
    3.28              SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
    3.29            | NONE => str module_name,
    3.30 @@ -397,30 +402,14 @@
    3.31            |> split_list
    3.32            |> apfst (map_filter I);
    3.33        in
    3.34 -        print_module_frame module_name (SOME export_ps)
    3.35 +        print_module_frame module_name [str language_pragma] (SOME export_ps)
    3.36            ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
    3.37        end;
    3.38  
    3.39 -    (*serialization*)
    3.40 -    fun write_module width (SOME destination) (module_name, content) =
    3.41 -          let
    3.42 -            val _ = File.check_dir destination;
    3.43 -            val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
    3.44 -              o separate "/" o Long_Name.explode) module_name;
    3.45 -            val _ = Isabelle_System.mkdirs (Path.dir filepath);
    3.46 -          in
    3.47 -            (File.write filepath o format [] width o Pretty.chunks2)
    3.48 -              [str language_pragma, content]
    3.49 -          end
    3.50 -      | write_module width NONE (_, content) = writeln (format [] width content);
    3.51    in
    3.52 -    Code_Target.serialization
    3.53 -      (fn width => fn destination => K () o map (write_module width destination))
    3.54 -      (fn present => fn width => rpair (try (deresolver ""))
    3.55 -        o (map o apsnd) (format present width))
    3.56 -      (map (fn (module_name, content) => print_module_frame module_name NONE [content]) includes
    3.57 -        @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
    3.58 -          ((flat o rev o Graph.strong_conn) haskell_program))
    3.59 +    (Code_Target.Hierarchy (map (fn (module_name, content) => print_module_frame module_name [] NONE [content]) includes
    3.60 +      @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
    3.61 +        ((flat o rev o Graph.strong_conn) haskell_program)), try (deresolver ""))
    3.62    end;
    3.63  
    3.64  val serializer : Code_Target.serializer =
     4.1 --- a/src/Tools/Code/code_ml.ML	Mon Jan 07 18:50:41 2019 +0100
     4.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jan 10 12:07:05 2019 +0000
     4.3 @@ -827,9 +827,9 @@
     4.4        memorize_data = K I, modify_stmts = modify_stmts }
     4.5    end;
     4.6  
     4.7 -fun serialize_ml print_ml_module print_ml_stmt ctxt
     4.8 +fun serialize_ml print_ml_module print_ml_stmt ml_extension ctxt
     4.9      { module_name, reserved_syms, identifiers, includes,
    4.10 -      class_syntax, tyco_syntax, const_syntax } exports program =
    4.11 +      class_syntax, tyco_syntax, const_syntax } program exports =
    4.12    let
    4.13  
    4.14      (* build program *)
    4.15 @@ -855,18 +855,15 @@
    4.16        @ map snd (Code_Namespace.print_hierarchical {
    4.17          print_module = print_module, print_stmt = print_stmt,
    4.18          lift_markup = apsnd } ml_program));
    4.19 -    fun write width NONE = writeln o format [] width
    4.20 -      | write width (SOME p) = File.write p o format [] width;
    4.21 -    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
    4.22    in
    4.23 -    Code_Target.serialization write prepare p
    4.24 +    (Code_Target.Singleton (ml_extension, p), try (deresolver []))
    4.25    end;
    4.26  
    4.27  val serializer_sml : Code_Target.serializer =
    4.28 -  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt);
    4.29 +  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt "ML");
    4.30  
    4.31  val serializer_ocaml : Code_Target.serializer =
    4.32 -  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt);
    4.33 +  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt "ocaml");
    4.34  
    4.35  
    4.36  (** Isar setup **)
     5.1 --- a/src/Tools/Code/code_runtime.ML	Mon Jan 07 18:50:41 2019 +0100
     5.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 10 12:07:05 2019 +0000
     5.3 @@ -437,7 +437,7 @@
     5.4      val thy = Proof_Context.theory_of ctxt;
     5.5      val (ml_modules, target_names) =
     5.6        Code_Target.produce_code_for ctxt
     5.7 -        target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
     5.8 +        target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos);
     5.9      val ml_code = space_implode "\n\n" (map snd ml_modules);
    5.10      val (consts', tycos') = chop (length consts) target_names;
    5.11      val consts_map = map2 (fn const =>
    5.12 @@ -856,7 +856,7 @@
    5.13    |-> (fn ([Const (const, _)], _) =>
    5.14      Code_Target.set_printings (Constant (const,
    5.15        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
    5.16 -  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN []));
    5.17 +  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE []));
    5.18  
    5.19  fun process_file filepath (definienda, thy) =
    5.20    let
     6.1 --- a/src/Tools/Code/code_scala.ML	Mon Jan 07 18:50:41 2019 +0100
     6.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jan 10 12:07:05 2019 +0000
     6.3 @@ -402,7 +402,7 @@
     6.4    end;
     6.5  
     6.6  fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers,
     6.7 -    includes, class_syntax, tyco_syntax, const_syntax } exports program =
     6.8 +    includes, class_syntax, tyco_syntax, const_syntax } program exports =
     6.9    let
    6.10  
    6.11      (* build program *)
    6.12 @@ -438,11 +438,8 @@
    6.13        @ Code_Namespace.print_hierarchical {
    6.14          print_module = print_module, print_stmt = print_stmt,
    6.15          lift_markup = I } scala_program);
    6.16 -    fun write width NONE = writeln o format [] width
    6.17 -      | write width (SOME p) = File.write p o format [] width;
    6.18 -    fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
    6.19    in
    6.20 -    Code_Target.serialization write prepare p
    6.21 +    (Code_Target.Singleton ("scala", p), try (deresolver []))
    6.22    end;
    6.23  
    6.24  val serializer : Code_Target.serializer =
     7.1 --- a/src/Tools/Code/code_target.ML	Mon Jan 07 18:50:41 2019 +0100
     7.2 +++ b/src/Tools/Code/code_target.ML	Thu Jan 10 12:07:05 2019 +0000
     7.3 @@ -9,11 +9,13 @@
     7.4    val cert_tyco: Proof.context -> string -> string
     7.5    val read_tyco: Proof.context -> string -> string
     7.6  
     7.7 -  val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
     7.8 +  datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
     7.9 +
    7.10 +  val export_code_for: Proof.context -> Path.T option -> string -> string -> int option -> Token.T list
    7.11      -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
    7.12 -  val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
    7.13 -    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
    7.14 -  val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
    7.15 +  val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
    7.16 +    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
    7.17 +  val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
    7.18      -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
    7.19    val check_code_for: Proof.context -> string -> bool -> Token.T list
    7.20      -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
    7.21 @@ -21,19 +23,19 @@
    7.22    val export_code: Proof.context -> bool -> string list
    7.23      -> (((string * string) * Path.T option) * Token.T list) list -> unit
    7.24    val produce_code: Proof.context -> bool -> string list
    7.25 -    -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
    7.26 +    -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
    7.27    val present_code: Proof.context -> string list -> Code_Symbol.T list
    7.28 -    -> string -> int option -> string -> Token.T list -> string
    7.29 +    -> string -> string -> int option -> Token.T list -> string
    7.30    val check_code: Proof.context -> bool -> string list
    7.31      -> ((string * bool) * Token.T list) list -> unit
    7.32  
    7.33    val generatedN: string
    7.34    val compilation_text: Proof.context -> string -> Code_Thingol.program
    7.35      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    7.36 -    -> (string * string) list * string
    7.37 +    -> (string list * string) list * string
    7.38    val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
    7.39      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    7.40 -    -> ((string * string) list * string) * (Code_Symbol.T -> string option)
    7.41 +    -> ((string list * string) list * string) * (Code_Symbol.T -> string option)
    7.42  
    7.43    type serializer
    7.44    type literals = Code_Printer.literals
    7.45 @@ -43,11 +45,7 @@
    7.46    val add_language: string * language -> theory -> theory
    7.47    val add_derived_target: string * ancestry -> theory -> theory
    7.48    val the_literals: Proof.context -> string -> literals
    7.49 -  type serialization
    7.50    val parse_args: 'a parser -> Token.T list -> 'a
    7.51 -  val serialization: (int -> Path.T option -> 'a -> unit)
    7.52 -    -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
    7.53 -    -> 'a -> serialization
    7.54    val default_code_width: int Config.T
    7.55  
    7.56    type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
    7.57 @@ -146,44 +144,54 @@
    7.58    end;
    7.59  
    7.60  
    7.61 -(** serializations and serializer **)
    7.62 -
    7.63 -(* serialization: abstract nonsense to cover different destinies for generated code *)
    7.64 -
    7.65 -datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
    7.66 -type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
    7.67 +(** serializers **)
    7.68  
    7.69 -fun serialization output _ content width (Export some_path) =
    7.70 -      (output width some_path content; NONE)
    7.71 -  | serialization _ string content width Produce =
    7.72 -      string [] width content |> SOME
    7.73 -  | serialization _ string content width (Present syms) =
    7.74 -     string syms width content
    7.75 -     |> (apfst o map o apsnd) Output.output
    7.76 -     |> SOME;
    7.77 -
    7.78 -fun export some_path f = (f (Export some_path); ());
    7.79 -fun produce f = the (f Produce);
    7.80 -fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
    7.81 -
    7.82 -
    7.83 -(* serializers: functions producing serializations *)
    7.84 +datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
    7.85  
    7.86  type serializer = Token.T list
    7.87    -> Proof.context
    7.88    -> {
    7.89 -    module_name: string,
    7.90      reserved_syms: string list,
    7.91      identifiers: Code_Printer.identifiers,
    7.92      includes: (string * Pretty.T) list,
    7.93      class_syntax: string -> string option,
    7.94      tyco_syntax: string -> Code_Printer.tyco_syntax option,
    7.95 -    const_syntax: string -> Code_Printer.const_syntax option }
    7.96 -  -> Code_Symbol.T list
    7.97 +    const_syntax: string -> Code_Printer.const_syntax option,
    7.98 +    module_name: string }
    7.99    -> Code_Thingol.program
   7.100 -  -> serialization;
   7.101 +  -> Code_Symbol.T list
   7.102 +  -> pretty_modules * (Code_Symbol.T -> string option);
   7.103 +
   7.104 +fun flat_modules selects width (Singleton (_, p)) =
   7.105 +      Code_Printer.format selects width p
   7.106 +  | flat_modules selects width (Hierarchy code_modules) =
   7.107 +      space_implode "\n\n" (map (Code_Printer.format selects width o snd) code_modules);
   7.108 +
   7.109 +fun export_to_file root width (Singleton (_, p)) =
   7.110 +      File.write root (Code_Printer.format [] width p)
   7.111 +  | export_to_file root width (Hierarchy code_modules) = (
   7.112 +      Isabelle_System.mkdirs root;
   7.113 +      map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules;
   7.114 +      ());
   7.115  
   7.116 -  
   7.117 +fun export_result ctxt some_root width (pretty_code, _) =
   7.118 +  case some_root of
   7.119 +    NONE => (writeln (flat_modules [] width pretty_code); ())
   7.120 +  | SOME relative_root =>
   7.121 +      let
   7.122 +        val root = File.full_path (Resources.master_directory (Proof_Context.theory_of ctxt)) relative_root;
   7.123 +        val _ = File.check_dir (Path.dir root);
   7.124 +      in export_to_file root width pretty_code end;
   7.125 +
   7.126 +fun produce_result syms width (Singleton (_, p), deresolve) =
   7.127 +      ([([], Code_Printer.format [] width p)], map deresolve syms)
   7.128 +  | produce_result syms width (Hierarchy code_modules, deresolve) =
   7.129 +      ((map o apsnd) (Code_Printer.format [] width) code_modules, map deresolve syms);
   7.130 +
   7.131 +fun present_result selects width (pretty_code, _) =
   7.132 +  flat_modules selects width pretty_code;
   7.133 +
   7.134 +
   7.135  (** theory data **)
   7.136  
   7.137  type language = {serializer: serializer, literals: literals,
   7.138 @@ -232,7 +240,7 @@
   7.139      val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
   7.140    in (modify, (target, data)) end;
   7.141  
   7.142 -  fun allocate_target target_name target thy =
   7.143 +fun allocate_target target_name target thy =
   7.144    let
   7.145      val _ = if exists_target thy target_name
   7.146        then error ("Attempt to overwrite existing target " ^ quote target_name)
   7.147 @@ -287,6 +295,10 @@
   7.148  
   7.149  val default_code_width = Attrib.setup_config_int \<^binding>\<open>default_code_width\<close> (K 80);
   7.150  
   7.151 +fun default_width ctxt = Config.get ctxt default_code_width;
   7.152 +
   7.153 +val the_width = the_default o default_width;
   7.154 +
   7.155  
   7.156  (* montage *)
   7.157  
   7.158 @@ -302,10 +314,11 @@
   7.159  fun activate_target ctxt target_name =
   7.160    let
   7.161      val thy = Proof_Context.theory_of ctxt;
   7.162 -    val (modify, target_data) = join_ancestry thy target_name;
   7.163 -  in (target_data, modify) end;
   7.164 +    val (modify, (target, data)) = join_ancestry thy target_name;
   7.165 +    val serializer = (#serializer o #language) target;
   7.166 +  in { serializer = serializer, data = data, modify = modify } end;
   7.167  
   7.168 -fun project_program ctxt syms_hidden syms1 program1 =
   7.169 +fun project_program_for_syms ctxt syms_hidden syms1 program1 =
   7.170    let
   7.171      val syms2 = subtract (op =) syms_hidden syms1;
   7.172      val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
   7.173 @@ -318,78 +331,70 @@
   7.174      val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
   7.175    in program3 end;
   7.176  
   7.177 -fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
   7.178 -    printings module_name args proto_program syms =
   7.179 +fun project_includes_for_syms syms includes =
   7.180 +   let
   7.181 +     fun select_include (name, (content, cs)) =
   7.182 +       if null cs orelse exists (member (op =) syms) cs
   7.183 +       then SOME (name, content) else NONE;
   7.184 +  in map_filter select_include includes end;
   7.185 +
   7.186 +fun prepare_serializer ctxt target_name module_name args proto_program syms =
   7.187    let
   7.188 -    val syms_hidden = Code_Symbol.symbols_of printings;
   7.189 -    val program = project_program ctxt syms_hidden syms proto_program;
   7.190 -    val syms_all = Code_Symbol.Graph.all_succs proto_program syms;
   7.191 -    fun select_include (name, (content, syms)) =
   7.192 -      if null syms orelse exists (member (op =) syms_all) syms
   7.193 -      then SOME (name, content) else NONE;
   7.194 -    val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
   7.195 -  in
   7.196 -    (serializer args ctxt {
   7.197 -      module_name = module_name,
   7.198 -      reserved_syms = reserved,
   7.199 -      identifiers = identifiers,
   7.200 +    val { serializer, data, modify } = activate_target ctxt target_name;
   7.201 +    val printings = Code_Printer.the_printings data;
   7.202 +    val _ = if module_name = "" then () else (check_name true module_name; ())
   7.203 +    val hidden_syms = Code_Symbol.symbols_of printings;
   7.204 +    val prepared_program = project_program_for_syms ctxt hidden_syms syms proto_program;
   7.205 +    val prepared_syms = subtract (op =) hidden_syms syms;
   7.206 +    val all_syms = Code_Symbol.Graph.all_succs proto_program syms;
   7.207 +    val includes = project_includes_for_syms all_syms
   7.208 +      (Code_Symbol.dest_module_data printings);
   7.209 +    val prepared_serializer = serializer args ctxt {
   7.210 +      reserved_syms = Code_Printer.the_reserved data,
   7.211 +      identifiers = Code_Printer.the_identifiers data,
   7.212        includes = includes,
   7.213        const_syntax = Code_Symbol.lookup_constant_data printings,
   7.214        tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
   7.215 -      class_syntax = Code_Symbol.lookup_type_class_data printings },
   7.216 -      (subtract (op =) syms_hidden syms, program))
   7.217 +      class_syntax = Code_Symbol.lookup_type_class_data printings,
   7.218 +      module_name = module_name };
   7.219 +  in
   7.220 +    (prepared_serializer o modify, (prepared_program, prepared_syms))
   7.221    end;
   7.222  
   7.223 -fun mount_serializer ctxt target_name some_width module_name args program syms =
   7.224 +fun invoke_serializer ctxt target_name module_name args program all_public syms =
   7.225    let
   7.226 -    val default_width = Config.get ctxt default_code_width;
   7.227 -    val ((target, data), modify) = activate_target ctxt target_name;
   7.228 -    val serializer = (#serializer o #language) target;
   7.229 -    val (prepared_serializer, (prepared_syms, prepared_program)) =
   7.230 -      prepare_serializer ctxt serializer
   7.231 -        (Code_Printer.the_reserved data) (Code_Printer.the_identifiers data)
   7.232 -        (Code_Printer.the_printings data)
   7.233 -        module_name args (modify program) syms
   7.234 -    val width = the_default default_width some_width;
   7.235 -  in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
   7.236 -
   7.237 -fun invoke_serializer ctxt target_name some_width raw_module_name args program all_public syms =
   7.238 -  let
   7.239 -    val module_name = if raw_module_name = "" then ""
   7.240 -      else (check_name true raw_module_name; raw_module_name)
   7.241 -    val (mounted_serializer, (prepared_syms, prepared_program)) =
   7.242 -      mount_serializer ctxt target_name some_width module_name args program syms;
   7.243 +    val (prepared_serializer, (prepared_program, prepared_syms)) =
   7.244 +      prepare_serializer ctxt target_name module_name args program syms;
   7.245 +    val exports = if all_public then [] else prepared_syms;
   7.246    in
   7.247      Code_Preproc.timed_exec "serializing"
   7.248 -      (fn () => mounted_serializer prepared_program (if all_public then [] else prepared_syms)) ctxt
   7.249 +      (fn () => prepared_serializer prepared_program exports) ctxt
   7.250    end;
   7.251  
   7.252  fun assert_module_name "" = error "Empty module name not allowed here"
   7.253    | assert_module_name module_name = module_name;
   7.254  
   7.255 -val using_master_directory =
   7.256 -  Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
   7.257 -
   7.258  in
   7.259  
   7.260  val generatedN = "Generated_Code";
   7.261  
   7.262 -fun export_code_for ctxt some_path target_name some_width module_name args =
   7.263 -  export (using_master_directory ctxt some_path)
   7.264 -  ooo invoke_serializer ctxt target_name some_width module_name args;
   7.265 +fun export_code_for ctxt some_root target_name module_name some_width args =
   7.266 +  export_result ctxt some_root (the_width ctxt some_width)
   7.267 +  ooo invoke_serializer ctxt target_name module_name args;
   7.268  
   7.269 -fun produce_code_for ctxt target_name some_width module_name args =
   7.270 +fun produce_code_for ctxt target_name module_name some_width args =
   7.271    let
   7.272 -    val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
   7.273 +    val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
   7.274    in fn program => fn all_public => fn syms =>
   7.275 -    produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
   7.276 +    produce_result syms (the_width ctxt some_width)
   7.277 +      (serializer program all_public syms)
   7.278    end;
   7.279  
   7.280 -fun present_code_for ctxt target_name some_width module_name args =
   7.281 +fun present_code_for ctxt target_name module_name some_width args =
   7.282    let
   7.283 -    val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
   7.284 +    val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
   7.285    in fn program => fn (syms, selects) =>
   7.286 -    present selects (serializer program false syms)
   7.287 +    present_result selects (the_width ctxt some_width) (serializer program false syms)
   7.288    end;
   7.289  
   7.290  fun check_code_for ctxt target_name strict args program all_public syms =
   7.291 @@ -399,8 +404,8 @@
   7.292      fun ext_check p =
   7.293        let
   7.294          val destination = make_destination p;
   7.295 -        val _ = export (SOME destination) (invoke_serializer ctxt target_name (SOME 80)
   7.296 -          generatedN args program all_public syms);
   7.297 +        val _ = export_result ctxt (SOME destination) 80
   7.298 +          (invoke_serializer ctxt target_name generatedN args program all_public syms)
   7.299          val cmd = make_command generatedN;
   7.300        in
   7.301          if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   7.302 @@ -415,7 +420,7 @@
   7.303      else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   7.304    end;
   7.305  
   7.306 -fun dynamic_compilation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
   7.307 +fun dynamic_compilation_text prepared_serializer width prepared_program syms all_public ((vs, ty), t) =
   7.308    let
   7.309      val _ = if Code_Thingol.contains_dict_var t then
   7.310        error "Term to be evaluated contains free dictionaries" else ();
   7.311 @@ -427,19 +432,21 @@
   7.312            Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE))
   7.313        |> fold (curry (perhaps o try o
   7.314            Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
   7.315 -    val (program_code, deresolve) =
   7.316 -      produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
   7.317 -    val value_name = the (deresolve Code_Symbol.value);
   7.318 -  in ((program_code, value_name), deresolve) end;
   7.319 +    val (pretty_code, deresolve) =
   7.320 +      prepared_serializer program (if all_public then [] else [Code_Symbol.value]);
   7.321 +    val (compilation_code, [SOME value_name]) =
   7.322 +      produce_result [Code_Symbol.value] width (pretty_code, deresolve);
   7.323 +  in ((compilation_code, value_name), deresolve) end;
   7.324  
   7.325  fun compilation_text' ctxt target_name some_module_name program syms =
   7.326    let
   7.327 +    val width = default_width ctxt;
   7.328      val evaluation_args = the_evaluation_args ctxt target_name;
   7.329 -    val (mounted_serializer, (_, prepared_program)) =
   7.330 -      mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) evaluation_args program syms;
   7.331 +    val (prepared_serializer, (prepared_program, _)) =
   7.332 +      prepare_serializer ctxt target_name (the_default generatedN some_module_name) evaluation_args program syms;
   7.333    in
   7.334      Code_Preproc.timed_exec "serializing"
   7.335 -    (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt
   7.336 +      (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt
   7.337    end;
   7.338  
   7.339  fun compilation_text ctxt target_name program syms =
   7.340 @@ -462,8 +469,8 @@
   7.341  fun export_code ctxt all_public cs seris =
   7.342    let
   7.343      val program = Code_Thingol.consts_program ctxt cs;
   7.344 -    val _ = map (fn (((target_name, module_name), some_path), args) =>
   7.345 -      export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
   7.346 +    val _ = map (fn (((target_name, module_name), some_root), args) =>
   7.347 +      export_code_for ctxt some_root target_name module_name NONE args program all_public (map Constant cs)) seris;
   7.348    in () end;
   7.349  
   7.350  fun export_code_cmd all_public raw_cs seris ctxt =
   7.351 @@ -523,11 +530,11 @@
   7.352      (parse_const_terms --
   7.353        Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
   7.354        -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
   7.355 -    (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
   7.356 +    (fn ctxt => fn ((read_constants, reads_statements), (target_name, some_width)) =>
   7.357        Latex.string
   7.358 -        (present_code ctxt (mk_cs ctxt)
   7.359 -          (maps (fn f => f ctxt) mk_stmtss)
   7.360 -          target_name some_width "Example" [])));
   7.361 +        (Latex.output_ascii (present_code ctxt (read_constants ctxt)
   7.362 +          (maps (fn read_statements => read_statements ctxt) reads_statements)
   7.363 +          target_name "Example" some_width []))));
   7.364  
   7.365  end;
   7.366