1.1 --- a/src/Tools/code/code_target.ML	Mon May 26 17:55:38 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Mon May 26 17:55:39 2008 +0200
     1.3 @@ -32,13 +32,13 @@
     1.4  
     1.5    type serializer;
     1.6    val add_serializer: string * serializer -> theory -> theory;
     1.7 +  val assert_serializer: theory -> string -> string;
     1.8    val get_serializer: theory -> string -> bool -> string option
     1.9      -> string option -> Args.T list
    1.10      -> string list option -> CodeThingol.code -> unit;
    1.11 -  val assert_serializer: theory -> string -> string;
    1.12 +  val sml_of: theory -> string list -> CodeThingol.code -> string;
    1.13    val eval: theory -> (string * (unit -> 'a) option ref)
    1.14      -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.15 -  val sml_of: theory -> string list -> CodeThingol.code -> string;
    1.16    val code_width: int ref;
    1.17  
    1.18    val setup: theory -> theory;
    1.19 @@ -62,6 +62,10 @@
    1.20  fun enum_default default sep opn cls [] = str default
    1.21    | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
    1.22  
    1.23 +val code_width = ref 80;
    1.24 +fun code_source p = Pretty.setmp_margin (!code_width) Pretty.string_of p ^ "\n";
    1.25 +fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    1.26 +
    1.27  
    1.28  (** syntax **)
    1.29  
    1.30 @@ -910,9 +914,6 @@
    1.31      str ("end;; (*struct " ^ name ^ "*)")
    1.32    ]);
    1.33  
    1.34 -val code_width = ref 80;
    1.35 -fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
    1.36 -
    1.37  fun seri_ml pr_def pr_modl module output labelled_name reserved_syms includes raw_module_alias
    1.38    (_ : string -> class_syntax option) tyco_syntax const_syntax cs code =
    1.39    let
    1.40 @@ -1093,9 +1094,9 @@
    1.41  fun isar_seri_sml module file =
    1.42    let
    1.43      val output = case file
    1.44 -     of NONE => use_text (1, "generated code") Output.ml_output false o code_output
    1.45 -      | SOME "-" => PrintMode.setmp [] writeln o code_output
    1.46 -      | SOME file => File.write (Path.explode file) o code_output;
    1.47 +     of NONE => use_text (1, "generated code") Output.ml_output false o code_source
    1.48 +      | SOME "-" => code_writeln
    1.49 +      | SOME file => File.write (Path.explode file) o code_source;
    1.50    in
    1.51      parse_args (Scan.succeed ())
    1.52      #> (fn () => seri_ml pr_sml pr_sml_modl module (output o snd))
    1.53 @@ -1103,16 +1104,14 @@
    1.54  
    1.55  fun eval_seri module file args =
    1.56    seri_ml pr_sml (K Pretty.chunks) (SOME "Isabelle_Eval")
    1.57 -    (fn (cs, p) => "let\n" ^ code_output p ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end");
    1.58 +    (fn (cs, p) => "let\n" ^ code_source p ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end");
    1.59  
    1.60  fun isar_seri_ocaml module file =
    1.61    let
    1.62      val output = case file
    1.63       of NONE => error "OCaml: no internal compilation"
    1.64 -      | SOME "-" => PrintMode.setmp [] writeln o code_output
    1.65 -      | SOME file => File.write (Path.explode file) o code_output;
    1.66 -    fun output_file file = File.write (Path.explode file) o code_output;
    1.67 -    val output_diag = PrintMode.setmp [] writeln o code_output;
    1.68 +      | SOME "-" => code_writeln
    1.69 +      | SOME file => File.write (Path.explode file) o code_source;
    1.70    in
    1.71      parse_args (Scan.succeed ())
    1.72      #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module (output o snd))
    1.73 @@ -1486,8 +1485,8 @@
    1.74                      o NameSpace.explode) modlname;
    1.75              val pathname = Path.append destination filename;
    1.76              val _ = File.mkdir (Path.dir pathname);
    1.77 -          in File.write pathname end
    1.78 -      | write_modulefile NONE _ = PrintMode.setmp [] writeln;
    1.79 +          in File.write pathname o code_source end
    1.80 +      | write_modulefile NONE _ = code_writeln;
    1.81      fun write_module destination (modulename, content) =
    1.82        Pretty.chunks [
    1.83          str ("module " ^ modulename ^ " where {"),
    1.84 @@ -1496,7 +1495,6 @@
    1.85          str "",
    1.86          str "}"
    1.87        ]
    1.88 -      |> code_output
    1.89        |> write_modulefile destination modulename;
    1.90      fun seri_module (modlname', (imports, (defs, _))) =
    1.91        let
    1.92 @@ -1564,8 +1562,7 @@
    1.93      |> Graph.fold (fn (name, (def, _)) =>
    1.94            case try pr (name, def) of SOME p => cons p | NONE => I) code
    1.95      |> Pretty.chunks2
    1.96 -    |> code_output
    1.97 -    |> PrintMode.setmp [] writeln
    1.98 +    |> code_writeln
    1.99    end;
   1.100  
   1.101