tuned
authorhaftmann
Thu Oct 25 13:52:05 2007 +0200 (2007-10-25)
changeset 25191e1146aa1e3e3
parent 25190 5cd8486c5a4f
child 25192 b568f8c5d5ca
tuned
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_target.ML	Thu Oct 25 13:52:04 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Thu Oct 25 13:52:05 2007 +0200
     1.3 @@ -1707,17 +1707,10 @@
     1.4        (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
     1.5      val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
     1.6      val code' = CodeThingol.add_value_stmt (t, ty) code;
     1.7 -    fun eval () = (
     1.8 -      reff := NONE;
     1.9 -      seri (SOME [CodeName.value_name]) code';
    1.10 -      use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
    1.11 -        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_args ^ "))");
    1.12 -      case !reff
    1.13 -       of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
    1.14 -            ^ " (reference probably has been shadowed)")
    1.15 -        | SOME f => f
    1.16 -      );
    1.17 -  in CRITICAL eval () end;
    1.18 +    val label = "evaluation in SML";
    1.19 +    fun eval () = (seri (SOME [CodeName.value_name]) code';
    1.20 +      evaluate (ref_name, reff) label Output.ml_output (!eval_verbose) val_args);
    1.21 +  in NAMED_CRITICAL label eval end;
    1.22  
    1.23  
    1.24