src/Pure/ML/ml_compiler_polyml.ML
changeset 56275 600f432ab556
parent 56265 785569927666
child 56281 03c3d1a7c3b8
equal deleted inserted replaced
56274:71eab6907eee 56275:600f432ab556
    72   in fn tree => Output.report (implode (reported_tree tree [])) end;
    72   in fn tree => Output.report (implode (reported_tree tree [])) end;
    73 
    73 
    74 
    74 
    75 (* eval ML source tokens *)
    75 (* eval ML source tokens *)
    76 
    76 
    77 fun eval verbose pos toks =
    77 type flags = {SML: bool, verbose: bool};
       
    78 
       
    79 fun eval {SML, verbose} pos toks =
    78   let
    80   let
    79     val _ = Secure.secure_mltext ();
    81     val _ = Secure.secure_mltext ();
    80     val space = ML_Env.name_space;
    82     val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
    81     val opt_context = Context.thread_data ();
    83     val opt_context = Context.thread_data ();
    82 
    84 
    83 
    85 
    84     (* input *)
    86     (* input *)
    85 
    87