src/Pure/codegen.ML
changeset 25009 61946780de00
parent 24920 2a45e400fdad
child 25309 30142fd3babf
     1.1 --- a/src/Pure/codegen.ML	Fri Oct 12 15:46:29 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Fri Oct 12 18:09:12 2007 +0200
     1.3 @@ -1013,26 +1013,28 @@
     1.4  
     1.5  val eval_result = ref (fn () => Bound 0);
     1.6  
     1.7 -fun eval_term thy = PrintMode.setmp [] (fn t =>
     1.8 -  let
     1.9 -    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    1.10 -      error "Term to be evaluated contains type variables";
    1.11 -    val _ = (null (term_vars t) andalso null (term_frees t)) orelse
    1.12 -      error "Term to be evaluated contains variables";
    1.13 -    val (code, gr) = setmp mode ["term_of"]
    1.14 -      (generate_code_i thy [] "Generated")
    1.15 -      [("result", Abs ("x", TFree ("'a", []), t))];
    1.16 -    val s = "structure EvalTerm =\nstruct\n\n" ^
    1.17 -      space_implode "\n" (map snd code) ^
    1.18 -      "\nopen Generated;\n\n" ^ Pretty.string_of
    1.19 -        (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
    1.20 -          Pretty.brk 1,
    1.21 -          mk_app false (mk_term_of gr "Generated" false (fastype_of t))
    1.22 -            [Pretty.str "(result ())"],
    1.23 -          Pretty.str ");"]) ^
    1.24 -      "\n\nend;\n";
    1.25 -    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
    1.26 -  in !eval_result () end);
    1.27 +fun eval_term thy t =
    1.28 +  let val e = PrintMode.setmp [] (fn () =>
    1.29 +    let
    1.30 +      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    1.31 +        error "Term to be evaluated contains type variables";
    1.32 +      val _ = (null (term_vars t) andalso null (term_frees t)) orelse
    1.33 +        error "Term to be evaluated contains variables";
    1.34 +      val (code, gr) = setmp mode ["term_of"]
    1.35 +        (generate_code_i thy [] "Generated")
    1.36 +        [("result", Abs ("x", TFree ("'a", []), t))];
    1.37 +      val s = "structure EvalTerm =\nstruct\n\n" ^
    1.38 +        space_implode "\n" (map snd code) ^
    1.39 +        "\nopen Generated;\n\n" ^ Pretty.string_of
    1.40 +          (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
    1.41 +            Pretty.brk 1,
    1.42 +            mk_app false (mk_term_of gr "Generated" false (fastype_of t))
    1.43 +              [Pretty.str "(result ())"],
    1.44 +            Pretty.str ");"]) ^
    1.45 +        "\n\nend;\n";
    1.46 +      val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
    1.47 +    in !eval_result end) ();
    1.48 +  in e () end;
    1.49  
    1.50  fun print_evaluated_term s = Toplevel.keep (fn state =>
    1.51    let