src/Pure/codegen.ML
changeset 14818 ad83019a66a4
parent 14769 b698d0b243dc
child 14858 9fc1a5cf9b5a
     1.1 --- a/src/Pure/codegen.ML	Sat May 29 14:55:56 2004 +0200
     1.2 +++ b/src/Pure/codegen.ML	Sat May 29 14:57:39 2004 +0200
     1.3 @@ -449,11 +449,11 @@
     1.4                          (Graph.new_node (id, (None, "")) gr'), rhs');
     1.5                     val (gr2, xs) = codegens false (gr1, args');
     1.6                     val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
     1.7 -                 in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
     1.8 +                 in Graph.map_node id (K (None, Output.output (Pretty.string_of (Pretty.block
     1.9                     (separate (Pretty.brk 1) (if null args' then
    1.10                         [Pretty.str ("val " ^ id ^ " :"), ty]
    1.11                       else Pretty.str ("fun " ^ id) :: xs) @
    1.12 -                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
    1.13 +                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n"))) gr3
    1.14                   end, mk_app brack (Pretty.str id) ps)
    1.15               end))
    1.16  
    1.17 @@ -499,13 +499,13 @@
    1.18      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
    1.19        (invoke_codegen thy "<Top>" false (gr, t)))
    1.20          (gr, map (apsnd (prep_term sg)) xs)
    1.21 -  in
    1.22 -    "structure Generated =\nstruct\n\n" ^
    1.23 -    output_code gr' ["<Top>"] ^
    1.24 -    space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
    1.25 -      [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
    1.26 -    "\n\nend;\n\nopen Generated;\n"
    1.27 -  end));
    1.28 +    val code =
    1.29 +      "structure Generated =\nstruct\n\n" ^
    1.30 +      output_code gr' ["<Top>"] ^
    1.31 +      space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
    1.32 +        [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
    1.33 +      "\n\nend;\n\nopen Generated;\n";
    1.34 +  in Output.output code end));
    1.35  
    1.36  val generate_code_i = gen_generate_code (K I);
    1.37  val generate_code = gen_generate_code
    1.38 @@ -559,7 +559,7 @@
    1.39      val s = "structure TestTerm =\nstruct\n\n" ^
    1.40        setmp mode ["term_of", "test"] (generate_code_i thy)
    1.41          [("testf", list_abs_free (frees, t))] ^
    1.42 -      "\n" ^ Pretty.string_of
    1.43 +      "\n" ^ Output.output (Pretty.string_of
    1.44          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
    1.45            Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
    1.46            Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
    1.47 @@ -579,7 +579,7 @@
    1.48                       mk_app false (mk_term_of sg false T)
    1.49                         [Pretty.str s], Pretty.str ")"]]) frees)) @
    1.50                    [Pretty.str "]"])]],
    1.51 -            Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
    1.52 +            Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"])) ^
    1.53        "\n\nend;\n";
    1.54      val _ = use_text Context.ml_output false s;
    1.55      fun iter f k = if k > i then None