# HG changeset patch
# User wenzelm
# Date 967581096 -7200
# Node ID 203e5552496b7a60711b3acd597506ef053360a0
# Parent  3a9f1931b30c4e013886b2eaac5372e9f16c1c32
added ML-Systems/polyml-4.0.ML;

diff -r 3a9f1931b30c -r 203e5552496b src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Aug 29 20:15:04 2000 +0200
+++ b/src/Pure/IsaMakefile	Tue Aug 29 22:31:36 2000 +0200
@@ -36,7 +36,7 @@
   Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML		\
   Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML		\
   Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML \
-  ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML	\
+  ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/polyml-4.0.ML ML-Systems/smlnj-0.93.ML	\
   ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML		\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
diff -r 3a9f1931b30c -r 203e5552496b src/Pure/ML-Systems/polyml-4.0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-4.0.ML	Tue Aug 29 22:31:36 2000 +0200
@@ -0,0 +1,140 @@
+(*  Title:      Pure/ML-Systems/polyml.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+Compatibility file for Poly/ML (versions 2.x and 3.x).
+*)
+
+(** ML system related **)
+
+open PolyML;
+
+
+(* restore old-style character / string functions *)
+
+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;
+
+
+(*Note start point for timing*)
+fun startTiming() =
+  let val CPUtimer = Timer.startCPUTimer();
+      val time = Timer.checkCPUTimer(CPUtimer)
+  in  (CPUtimer,time)  end;
+
+(*Finish timing and return string*)
+fun endTiming (CPUtimer, {sys,usr}) =
+  let open Time  (*...for Time.toString, Time.+ and Time.- *)
+      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
+  in  "User " ^ toString (usr2-usr) ^
+      "  All "^ toString (sys2-sys + usr2-usr) ^
+      " secs"
+      handle Time => ""
+  end;
+
+
+(* prompts *)
+
+fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
+
+
+(* toplevel pretty printing (see also Pure/install_pp.ML) *)
+
+fun make_pp path pprint = ();
+fun install_pp _ = ();
+(* FIXME
+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);
+*)
+
+
+(* ML command execution -- 'eval' *)
+
+local
+
+fun drop_last [] = []
+  | drop_last [x] = []
+  | drop_last (x :: xs) = x :: drop_last xs;
+
+val drop_last_char = implode o drop_last o explode;
+
+in
+
+fun use_text print verbose txt =
+  let
+    val in_buffer = ref (explode txt);
+    val out_buffer = ref ([]: string list);
+
+    fun get () =
+      (case ! in_buffer of
+        [] => ""
+      | c :: cs => (in_buffer := cs; c));
+    fun put s = out_buffer := s :: ! out_buffer;
+
+    fun exec () =
+      (case ! in_buffer of
+        [] => ()
+      | _ => (PolyML.compiler (get, put) (); exec ()));
+
+    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
+  in
+    exec () handle exn => (show_output (); raise exn);
+    if verbose then show_output () else ()
+  end;
+
+end;
+
+
+
+(** interrupts **)      (*Note: may get into race conditions*)
+
+fun mask_interrupt f x = f x;
+fun unmask_interrupt f x = f x;
+fun exhibit_interrupt f x = f x;
+
+
+
+(** OS related **)
+
+(* system command execution *)
+
+(*execute Unix command which doesn't take any input from stdin and
+  sends its output to stdout; could be done more easily by Unix.execute,
+  but that function doesn't use the PATH*)
+fun execute command =
+  let
+    val tmp_name = OS.FileSys.tmpName ();
+    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;
+
+(*plain version; with return code*)
+fun system cmd =
+  if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
+
+
+(* file handling *)
+
+(*get time of last modification*)
+fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
+
+
+(* getenv *)
+
+fun getenv var =
+  (case OS.Process.getEnv var of
+    NONE => ""
+  | SOME txt => txt);
+
+
+(* non-ASCII input (see also Thy/use.ML) *)
+
+val needs_filtered_use = true;