added ML-Systems/polyml-4.0.ML;
authorwenzelm
Tue Aug 29 22:31:36 2000 +0200 (2000-08-29)
changeset 9735203e5552496b
parent 9734 3a9f1931b30c
child 9736 332fab43628f
added ML-Systems/polyml-4.0.ML;
src/Pure/IsaMakefile
src/Pure/ML-Systems/polyml-4.0.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Aug 29 20:15:04 2000 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Aug 29 22:31:36 2000 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML		\
     1.5    Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML		\
     1.6    Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML \
     1.7 -  ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML	\
     1.8 +  ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/polyml-4.0.ML ML-Systems/smlnj-0.93.ML	\
     1.9    ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML		\
    1.10    Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
    1.11    Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML		\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/polyml-4.0.ML	Tue Aug 29 22:31:36 2000 +0200
     2.3 @@ -0,0 +1,140 @@
     2.4 +(*  Title:      Pure/ML-Systems/polyml.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1991  University of Cambridge
     2.8 +
     2.9 +Compatibility file for Poly/ML (versions 2.x and 3.x).
    2.10 +*)
    2.11 +
    2.12 +(** ML system related **)
    2.13 +
    2.14 +open PolyML;
    2.15 +
    2.16 +
    2.17 +(* restore old-style character / string functions *)
    2.18 +
    2.19 +fun ord s = Char.ord (String.sub (s, 0));
    2.20 +val chr = str o Char.chr;
    2.21 +val explode = (map str) o String.explode;
    2.22 +val implode = String.concat;
    2.23 +
    2.24 +
    2.25 +(*Note start point for timing*)
    2.26 +fun startTiming() =
    2.27 +  let val CPUtimer = Timer.startCPUTimer();
    2.28 +      val time = Timer.checkCPUTimer(CPUtimer)
    2.29 +  in  (CPUtimer,time)  end;
    2.30 +
    2.31 +(*Finish timing and return string*)
    2.32 +fun endTiming (CPUtimer, {sys,usr}) =
    2.33 +  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    2.34 +      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    2.35 +  in  "User " ^ toString (usr2-usr) ^
    2.36 +      "  All "^ toString (sys2-sys + usr2-usr) ^
    2.37 +      " secs"
    2.38 +      handle Time => ""
    2.39 +  end;
    2.40 +
    2.41 +
    2.42 +(* prompts *)
    2.43 +
    2.44 +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    2.45 +
    2.46 +
    2.47 +(* toplevel pretty printing (see also Pure/install_pp.ML) *)
    2.48 +
    2.49 +fun make_pp path pprint = ();
    2.50 +fun install_pp _ = ();
    2.51 +(* FIXME
    2.52 +fun make_pp _ pprint (str, blk, brk, en) obj =
    2.53 +  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    2.54 +    fn () => brk (99999, 0), en);
    2.55 +*)
    2.56 +
    2.57 +
    2.58 +(* ML command execution -- 'eval' *)
    2.59 +
    2.60 +local
    2.61 +
    2.62 +fun drop_last [] = []
    2.63 +  | drop_last [x] = []
    2.64 +  | drop_last (x :: xs) = x :: drop_last xs;
    2.65 +
    2.66 +val drop_last_char = implode o drop_last o explode;
    2.67 +
    2.68 +in
    2.69 +
    2.70 +fun use_text print verbose txt =
    2.71 +  let
    2.72 +    val in_buffer = ref (explode txt);
    2.73 +    val out_buffer = ref ([]: string list);
    2.74 +
    2.75 +    fun get () =
    2.76 +      (case ! in_buffer of
    2.77 +        [] => ""
    2.78 +      | c :: cs => (in_buffer := cs; c));
    2.79 +    fun put s = out_buffer := s :: ! out_buffer;
    2.80 +
    2.81 +    fun exec () =
    2.82 +      (case ! in_buffer of
    2.83 +        [] => ()
    2.84 +      | _ => (PolyML.compiler (get, put) (); exec ()));
    2.85 +
    2.86 +    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
    2.87 +  in
    2.88 +    exec () handle exn => (show_output (); raise exn);
    2.89 +    if verbose then show_output () else ()
    2.90 +  end;
    2.91 +
    2.92 +end;
    2.93 +
    2.94 +
    2.95 +
    2.96 +(** interrupts **)      (*Note: may get into race conditions*)
    2.97 +
    2.98 +fun mask_interrupt f x = f x;
    2.99 +fun unmask_interrupt f x = f x;
   2.100 +fun exhibit_interrupt f x = f x;
   2.101 +
   2.102 +
   2.103 +
   2.104 +(** OS related **)
   2.105 +
   2.106 +(* system command execution *)
   2.107 +
   2.108 +(*execute Unix command which doesn't take any input from stdin and
   2.109 +  sends its output to stdout; could be done more easily by Unix.execute,
   2.110 +  but that function doesn't use the PATH*)
   2.111 +fun execute command =
   2.112 +  let
   2.113 +    val tmp_name = OS.FileSys.tmpName ();
   2.114 +    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
   2.115 +    val result = TextIO.inputAll is;
   2.116 +  in
   2.117 +    TextIO.closeIn is;
   2.118 +    OS.FileSys.remove tmp_name;
   2.119 +    result
   2.120 +  end;
   2.121 +
   2.122 +(*plain version; with return code*)
   2.123 +fun system cmd =
   2.124 +  if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
   2.125 +
   2.126 +
   2.127 +(* file handling *)
   2.128 +
   2.129 +(*get time of last modification*)
   2.130 +fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
   2.131 +
   2.132 +
   2.133 +(* getenv *)
   2.134 +
   2.135 +fun getenv var =
   2.136 +  (case OS.Process.getEnv var of
   2.137 +    NONE => ""
   2.138 +  | SOME txt => txt);
   2.139 +
   2.140 +
   2.141 +(* non-ASCII input (see also Thy/use.ML) *)
   2.142 +
   2.143 +val needs_filtered_use = true;