# HG changeset patch # User paulson # Date 868010178 -7200 # Node ID 124103119f1c27c9344323eb0d7dccd31d0e844d # Parent 88e7860240797c3ec0f7499d8d1f838954626681 Moved MLWorks.ML to its proper place, directory ML-Systems. Note that MLWorks does not quite work yet, especially top-level pretty printing diff -r 88e786024079 -r 124103119f1c src/Pure/ML-Systems/MLWorks.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/MLWorks.ML Fri Jul 04 11:56:18 1997 +0200 @@ -0,0 +1,115 @@ +(* Title: Pure/MLWorks.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Compatibility file for MLWorks (??) + +NB: There is still no easy way of building Isabelle under MLWorks. This file + is just a start towards compatibility. One problem is the peculiar + behaviour of "use" in MLWorks. Strange errors occur when loading theories, + and ROOT.ML files on subdirectories are loaded incorrectly. +*) + +(*** Poly/ML emulation ***) + +(** +Shell.File.loadSource "system.__os"; +Shell.File.loadSource "basis.__timer"; +Shell.File.loadSource "system.__time"; +Shell.File.loadSource "unix.__os_file_sys"; +Shell.File.loadSource "basis.__list"; +Shell.File.loadSource "basis.__char"; +Shell.File.loadSource "basis.__string"; +Shell.File.loadSource "basis.__text_io"; +**) + + +(*To exit the system with an exit code -- an alternative to ^D *) +fun exit 0 = OS.Process.exit OS.Process.success + | exit _ = OS.Process.exit OS.Process.failure; +fun quit () = exit 0; + +(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) +fun print_depth n = (); + +(*Interface for toplevel pretty printers, see also Pure/install_pp.ML + CURRENTLY UNAVAILABLE*) +fun make_pp path pprint = (); +fun install_pp _ = (); + + +(*** New Jersey ML parameters ***) + +(*** Character/string functions which are compatible with 0.93 and Poly/ML ***) + +fun ord s = Char.ord (String.sub(s,0)); +val chr = str o Char.chr; +val explode = (map str) o String.explode; +val implode = String.concat; + + +(*** Timing functions ***) + +(*A conditional timing function: applies f to () and, if the flag is true, + prints its runtime. *) +fun cond_timeit flag f = + if flag then + let open Time (*...for Time.toString, Time.+ and Time.- *) + val CPUtimer = Timer.startCPUTimer(); + val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); + val result = f(); + val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) + in print("User " ^ toString (usrt2-usrt1) ^ + " GC " ^ toString (gct2-gct1) ^ + " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ + " secs\n") + handle Time => (); + result + end + else f(); + + +(*** File handling ***) + +(*Get time of last modification; if file doesn't exist return an empty string*) +fun file_info "" = "" + | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>""; + + +(*** ML command execution ***) + +val tmpName = OS.FileSys.tmpName(); + +(*Can one redirect 'use' directly to an instream?*) +fun use_string slist = + let val tmpFile = TextIO.openOut tmpName + in app (fn s => TextIO.output (tmpFile, s)) slist; + TextIO.closeOut tmpFile; + use tmpName + end; + + +(*** System command execution ***) + +(*Execute an Unix command which doesn't take any input from stdin and + sends its output to stdout. + This could be done more easily by Unix.execute, but that function + doesn't use the PATH.*) +fun execute command = + let val is = (OS.Process.system (command ^ " > " ^ tmpName); + TextIO.openIn tmpName); + val result = TextIO.inputAll is; + in TextIO.closeIn is; + OS.FileSys.remove tmpName; + result + end; + + +(*Don't know what the boolean is for*) +fun xML filename = Shell.saveImage (filename, false); + + +(*Non-printing and 8-bit chars are forbidden in string constants*) +val needs_filtered_use = true; + diff -r 88e786024079 -r 124103119f1c src/Pure/MLWorks.ML --- a/src/Pure/MLWorks.ML Fri Jul 04 11:54:43 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -(* Title: Pure/MLWorks.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Compatibility file for MLWorks (??) - -NB: There is still no easy way of building Isabelle under MLWorks. This file - is just a start towards compatibility. One problem is the peculiar - behaviour of "use" in MLWorks. Strange errors occur when loading theories, - and ROOT.ML files on subdirectories are loaded incorrectly. -*) - -(*** Poly/ML emulation ***) - -(** -Shell.File.loadSource "system.__os"; -Shell.File.loadSource "basis.__timer"; -Shell.File.loadSource "system.__time"; -Shell.File.loadSource "unix.__os_file_sys"; -Shell.File.loadSource "basis.__list"; -Shell.File.loadSource "basis.__char"; -Shell.File.loadSource "basis.__string"; -Shell.File.loadSource "basis.__text_io"; -**) - - -(*To exit the system with an exit code -- an alternative to ^D *) -fun exit 0 = OS.Process.exit OS.Process.success - | exit _ = OS.Process.exit OS.Process.failure; -fun quit () = exit 0; - -(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) -fun print_depth n = (); - -(*Interface for toplevel pretty printers, see also Pure/install_pp.ML - CURRENTLY UNAVAILABLE*) -fun make_pp path pprint = (); -fun install_pp _ = (); - - -(*** New Jersey ML parameters ***) - -(*** Character/string functions which are compatible with 0.93 and Poly/ML ***) - -fun ord s = Char.ord (String.sub(s,0)); -val chr = str o Char.chr; -val explode = (map str) o String.explode; -val implode = String.concat; - - -(*** Timing functions ***) - -(*A conditional timing function: applies f to () and, if the flag is true, - prints its runtime. *) -fun cond_timeit flag f = - if flag then - let open Time (*...for Time.toString, Time.+ and Time.- *) - val CPUtimer = Timer.startCPUTimer(); - val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); - val result = f(); - val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) - in print("User " ^ toString (usrt2-usrt1) ^ - " GC " ^ toString (gct2-gct1) ^ - " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ - " secs\n") - handle Time => (); - result - end - else f(); - - -(*** File handling ***) - -(*Get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>""; - - -(*** ML command execution ***) - -val tmpName = OS.FileSys.tmpName(); - -(*Can one redirect 'use' directly to an instream?*) -fun use_string slist = - let val tmpFile = TextIO.openOut tmpName - in app (fn s => TextIO.output (tmpFile, s)) slist; - TextIO.closeOut tmpFile; - use tmpName - end; - - -(*** System command execution ***) - -(*Execute an Unix command which doesn't take any input from stdin and - sends its output to stdout. - This could be done more easily by Unix.execute, but that function - doesn't use the PATH.*) -fun execute command = - let val is = (OS.Process.system (command ^ " > " ^ tmpName); - TextIO.openIn tmpName); - val result = TextIO.inputAll is; - in TextIO.closeIn is; - OS.FileSys.remove tmpName; - result - end; - - -(*Don't know what the boolean is for*) -fun xML filename = Shell.saveImage (filename, false); - - -(*Non-printing and 8-bit chars are forbidden in string constants*) -val needs_filtered_use = true; -