--- a/src/Pure/Makefile Thu Jun 19 11:31:14 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (Pure) #
-# #
-#########################################################################
-
-#The pure part is common to all systems.
-#Object-logics (like FOL) are loaded on top of it.
-
-#To make the system, cd to this directory and type
-# make -f Makefile
-
-#Environment variable ML_DBASE specifies the initial Poly/ML database, from
-# the Poly/ML distribution directory.
-#WARNING: Poly/ML parent databases should not be moved!
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES = POLY.ML NJ.ML NJ093.ML NJ1xx.ML ROOT.ML basis.ML library.ML\
- term.ML symtab.ML type.ML sign.ML\
- sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
- net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
- goals.ML axclass.ML install_pp.ML sorts.ML type_infer.ML\
- NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
-
-SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\
- Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\
- Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\
- Syntax/syn_ext.ML Syntax/mixfix.ML Syntax/symbol_font.ML\
- Syntax/token_trans.ML
-
-THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\
- Thy/thy_syn.ML Thy/thy_read.ML Thy/thm_database.ML
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE)
- @case `basename "$(COMP)"` in \
- poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
- cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
- echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
- | $(COMP) $(BIN)/Pure;\
- discgarb -c $(BIN)/Pure;;\
- sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
- then echo Bad value for ISABELLEBIN: \
- $(BIN) is not a writable directory; \
- exit 1; \
- fi;\
- echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\
- *) echo Bad value for ISABELLECOMP: $(COMP); \
- echo " " \"`basename "$(COMP)"`\" is not poly or sml;;\
- esac
-
-
-test: $(BIN)/Pure
-
-.PRECIOUS: $(BIN)/Pure
--- a/src/Pure/NJ.ML Thu Jun 19 11:31:14 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title: Pure/NJ
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Compatibility file for Standard ML of New Jersey.
-*)
-
-
-(*Determine if we are running under 0.93 or a newer version of SML/NJ
- This is based on the variable "version" defined in 0.93's System structure
- which is no longer present in 1.09.*)
-
-local val version = ""; open System in
- val smlversion = if version <> "" then 93 else 109
-end;
-
-use (if smlversion = 93 then "NJ093.ML" else "NJ1xx.ML");
-
-
-(** Other functions which are not specific to 0.93 or 1.xx*)
-
-(*Dummy version of the Poly/ML function*)
-fun commit() = ();
--- a/src/Pure/NJ093.ML Thu Jun 19 11:31:14 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-(* Title: Pure/NJ093.ML
- ID: $Id$
- Author: Carsten Clasohm, TU Muenchen
- Copyright 1996 TU Muenchen
-
-Compatibility file for Standard ML of New Jersey version 0.93.
-*)
-
-
-use"basis.ML";
-
-(*** Poly/ML emulation ***)
-
-(*To exit the system with an exit code -- an alternative to ^D *)
-val exit = System.Unsafe.CInterface.exit;
-fun quit () = exit 0;
-
-(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
-fun print_depth n = (System.Control.Print.printDepth := n div 2;
- System.Control.Print.printLength := n);
-
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp path pprint =
- let
- open System.PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (add_string pps, begin_block pps INCONSISTENT,
- fn wd => add_break pps (wd, 0), fn () => add_newline pps,
- fn () => end_block pps);
- in
- (path, pp)
- end;
-
-fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
-
-
-(*** New Jersey ML parameters ***)
-
-(* Suppresses Garbage Collection messages; default was 2 *)
-System.Control.Runtime.gcmessages := 0;
-
-
-(*** Timing functions ***)
-
-(*Print microseconds, suppressing trailing zeroes*)
-fun umakestring 0 = ""
- | umakestring n = chr(ord "0" + n div 100000) ^
- umakestring(10 * (n mod 100000));
-
-(*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 fun string_of_time (System.Timer.TIME {sec, usec}) =
- makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
- open System.Timer;
- val start = start_timer()
- val result = f();
- val nongc = check_timer(start)
- and gc = check_timer_gc(start);
- val both = add_time(nongc, gc)
- in print("Non GC " ^ string_of_time nongc ^
- " GC " ^ string_of_time gc ^
- " both "^ string_of_time both ^ " secs\n");
- result
- end
- else f();
-
-
-(*** File handling ***)
-
-(*Get time of last modification; if file doesn't exist return an empty string*)
-local
- open System.Timer;
- open System.Unsafe.SysIO;
-in
- fun file_info "" = ""
- | file_info name = makestring (mtime (PATH name)) handle _ => "";
-end;
-
-structure OS =
- struct
- structure FileSys =
- struct
- val chDir = System.Directory.cd
- val remove = System.Unsafe.SysIO.unlink (*Delete a file *)
- val getDir = System.Directory.getWD (*path of working directory*)
- end
- end;
-
-
-(*** ML command execution ***)
-
-fun use_string commands =
- System.Compile.use_stream (open_string (implode commands));
-
-
-(*** 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 IO.execute, but that function
- seems to be buggy in SML/NJ 0.93.*)
-fun execute command =
- let val tmp_name = "isa_converted.tmp"
- val is = (System.system (command ^ " > " ^ tmp_name);
- open_in tmp_name);
- val result = input (is, 999999);
- in close_in is;
- OS.FileSys.remove tmp_name;
- result
- end;
-
-(*redefine to flush its output immediately -- temporary patch suggested
- by Kim Dam Petersen*)
-val output = fn(s, t) => (output(s, t); flush_out s);
-
-(*For use in Makefiles -- saves space*)
-fun xML filename banner = (exportML filename; print(banner^"\n"));
-
-
-val needs_filtered_use = false;
--- a/src/Pure/NJ1xx.ML Thu Jun 19 11:31:14 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,132 +0,0 @@
-(* Title: Pure/NJ1xx.ML
- ID: $Id$
- Author: Carsten Clasohm, TU Muenchen
- Copyright 1996 TU Muenchen
-
-Compatibility file for Standard ML of New Jersey version 1.xx.
-*)
-
-(*** Poly/ML emulation ***)
-
-
-(*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 = (Compiler.Control.Print.printDepth := n div 2;
- Compiler.Control.Print.printLength := n);
-
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp path pprint =
- let
- open Compiler.PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (add_string pps, begin_block pps INCONSISTENT,
- fn wd => add_break pps (wd, 0), fn () => add_newline pps,
- fn () => end_block pps);
- in
- (path, pp)
- end;
-
-fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
-
-
-(*** New Jersey ML parameters ***)
-
-(* Suppresses Garbage Collection messages; doesn't work yet *)
-(*System.Runtime.gc 0;*)
-
-val _ = (Compiler.Control.Print.printLength := 1000;
- Compiler.Control.Print.printDepth := 350;
- Compiler.Control.Print.stringDepth := 250;
- Compiler.Control.Print.signatures := 2);
-
-(*** 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 ***)
-
-
-(*For version 109.21 and later:*)
-val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
-
-(*For versions prior to 109.21:*****
-fun use_string commands =
- Compiler.Interact.use_stream (open_string (implode commands));
-*)
-
-(*** 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 tmp_name = "isa_converted.tmp"
- val is = (OS.Process.system (command ^ " > " ^ tmp_name);
- TextIO.openIn tmp_name);
- val result = TextIO.inputAll is;
- in TextIO.closeIn is;
- OS.FileSys.remove tmp_name;
- result
- end;
-
-(*For exporting images. The short name saves space in Makefiles*)
-fun xML filename banner =
- let open SMLofNJ
- val runtime = hd (SMLofNJ.getAllArgs())
- and exec_file = TextIO.openOut filename
- in
- TextIO.output (*Write a shell script to invoke the actual image*)
- (exec_file,
- String.concat
- ["#!/bin/sh\n", runtime,
- " @SMLdebug=/dev/null", (*suppresses GC messages*)
- " @SMLload=", filename, ".heap\n"]);
- TextIO.closeOut exec_file;
- OS.Process.system ("chmod a+x " ^ filename);
- exportML (filename^".heap");
- print(banner^"\n")
- end;
-
-
-val needs_filtered_use = false;
--- a/src/Pure/POLY.ML Thu Jun 19 11:31:14 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-(* Title: Pure/POLY
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Compatibility file for Poly/ML (AHL release 1.88)
-*)
-
-open PolyML ExtendedIO;
-
-use"basis.ML";
-
-(*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 val before = System.processtime()
- val result = f()
- val both = real(System.processtime() - before) / 10.0
- in output(std_out, "Process time (incl GC): "^
- makestring both ^ " secs\n");
- result
- end
- else f();
-
-
-(*Save function: in Poly/ML, ignores filename and commits to present file*)
-
-fun xML filename banner = commit();
-
-
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp _ pprint (str, blk, brk, en) obj =
- pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
- fn () => brk (99999, 0), en);
-
-
-(*** File handling ***)
-
-local
-
-(*These are functions from library.ML *)
-fun take_suffix _ [] = ([], [])
- | take_suffix pred (x :: xs) =
- (case take_suffix pred xs of
- ([], sffx) => if pred x then ([], x :: sffx)
- else ([x], sffx)
- | (prfx, sffx) => (x :: prfx, sffx));
-
-fun apr (f,y) x = f(x,y);
-
-fun seq (proc: 'a -> unit) : 'a list -> unit =
- let fun seqf [] = ()
- | seqf (x :: xs) = (proc x; seqf xs)
- in seqf end;
-
-in
-
-(*Get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""
- | file_info name = makestring (System.filedate name) handle _ => "";
-
-
-structure OS =
- struct
- structure FileSys =
- struct
- val chDir = PolyML.cd
-
- fun remove name = (*Delete a file *)
- let val (is, os) = ExtendedIO.execute ("rm " ^ name)
- in close_in is; close_out os end;
-
- (*Get pathname of current working directory *)
- fun getDir () =
- let val (is, os) = ExtendedIO.execute ("pwd")
- val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
- (explode (ExtendedIO.input_line is))
- in close_in is; close_out os; implode path end;
-
- end
- end;
-
-
-
-(*** ML command execution ***)
-
-val use_string =
- let fun exec command =
- let val firstLine = ref true;
-
- fun getLine () =
- if !firstLine
- then (firstLine := false; command)
- else raise Io "use_string: buffer exhausted"
- in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
- in seq exec end;
-
-end;
-
-
-(*** System command execution ***)
-
-(*Execute an Unix command which doesn't take any input from stdin and
- sends its output to stdout.*)
-fun execute command =
- let val (is, os) = ExtendedIO.execute command;
- val result = input (is, 999999);
- in close_out os;
- close_in is;
- result
- end;
-
-
-(*Non-printing and 8-bit chars are forbidden in string constants*)
-val needs_filtered_use = true;