src/Pure/library.ML
changeset 955 aa0c5f9daf5b
parent 544 c53386a5bcf1
child 1290 ee8f41456d28
equal deleted inserted replaced
954:d3f734f66141 955:aa0c5f9daf5b
   690 (*timed "use" function, printing filenames*)
   690 (*timed "use" function, printing filenames*)
   691 fun time_use fname = timeit (fn () =>
   691 fun time_use fname = timeit (fn () =>
   692   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
   692   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
   693    writeln ("\n**** Finished " ^ fname ^ " ****")));
   693    writeln ("\n**** Finished " ^ fname ^ " ****")));
   694 
   694 
       
   695 (*For Makefiles: use the file, but exit with error code if errors found.*)
       
   696 fun exit_use fname = use fname handle _ => exit 1;
   695 
   697 
   696 
   698 
   697 (** filenames **)
   699 (** filenames **)
   698 
   700 
   699 (*convert UNIX filename of the form "path/file" to "path/" and "file";
   701 (*convert UNIX filename of the form "path/file" to "path/" and "file";