src/Pure/ML/ml_context.ML
changeset 56434 7acc933bd7cc
parent 56304 40274e4f5ebf
child 57832 5b48f2047c24
equal deleted inserted replaced
56433:db69cb14f7ed 56434:7acc933bd7cc
   186      (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
   186      (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
   187       ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
   187       ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
   188 
   188 
   189 end;
   189 end;
   190 
   190 
   191 fun use s =
       
   192   ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
       
   193     handle ERROR msg => (writeln msg; error "ML error");
       
   194