src/Pure/library.ML
changeset 2317 672015b535d7
parent 2303 84ed9e0d7c50
child 2403 8115988ccc22
equal deleted inserted replaced
2316:ba9c9ed28dd8 2317:672015b535d7
   683 
   683 
   684 
   684 
   685 (** input / output **)
   685 (** input / output **)
   686 
   686 
   687 val cd = OS.FileSys.chDir;
   687 val cd = OS.FileSys.chDir;
       
   688 val pwd = OS.FileSys.getDir;
   688 
   689 
   689 val prs_fn = ref(fn s => TextIO.output (TextIO.stdOut, s));
   690 val prs_fn = ref(fn s => TextIO.output (TextIO.stdOut, s));
   690 
   691 
   691 fun prs s = !prs_fn s;
   692 fun prs s = !prs_fn s;
   692 fun writeln s = prs (s ^ "\n");
   693 fun writeln s = prs (s ^ "\n");