# HG changeset patch
# User wenzelm
# Date 1213457170 -7200
# Node ID 1a604efd267d5c7d7bb0238267254a48bdc4de38
# Parent  e0323036bcf2d4b6cf903f2bf796784cd89b17dd
removed experimental Poplog/PML support;

diff -r e0323036bcf2 -r 1a604efd267d etc/settings
--- a/etc/settings	Sat Jun 14 17:26:09 2008 +0200
+++ b/etc/settings	Sat Jun 14 17:26:10 2008 +0200
@@ -67,13 +67,6 @@
 #ML_OPTIONS=""
 #ML_PLATFORM=""
 
-# Poplog/PML version 15.6/2.1 (experimental!)
-#ML_SYSTEM=poplogml
-#ML_HOME="/usr/local/poplog/current-poplog/bin"
-#ML_OPTIONS="-noinit"
-#ML_SUFFIX=".psv"
-#ML_PLATFORM=""
-
 
 ###
 ### Interactive sessions (cf. isatool tty)
diff -r e0323036bcf2 -r 1a604efd267d lib/scripts/run-poplogml
--- a/lib/scripts/run-poplogml	Sat Jun 14 17:26:09 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# Poplog/PML startup script (version 15.6/2.1).
-
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
-  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
-  exit 2
-}
-
-function check_mlhome_file()
-{
-  if [ ! -f "$1" ]; then
-    echo "Unable to locate $1" >&2
-    echo "Please check your ML_HOME setting!" >&2
-    exit 2
-  fi
-}
-
-function check_heap_file()
-{
-  if [ ! -f "$1" ]; then
-    echo "Expected to find ML heap file $1" >&2
-    return 1
-  else
-    return 0
-  fi
-}
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
-  EXIT="fun exit (i: int) = OS.execve \"/bin/sh\" [\"sh\", \"-c\", \"exit \" ^ makestring i] (OS.envlist());"
-  USE='pop11
-section $-ml;
-
-ml_exception Use of string;
-
-ml_val use : string -> unit =
-procedure(name) with_props use;
-        lvars name, path;
-        lconstant UseExn = exception("Use");
-
-        define dlocal pop_exception_handler(n, msg, idstring, severity);
-                returnunless(severity == `E` or severity == `R`)(false);
-                erasenum(n);
-                raise(UseExn(name));
-        enddefine;
-
-        unless sourcefile(name) ->> path then raise(UseExn(name)) endunless;
-        ml_load(path);
-        ml_unit;
-endprocedure;
-
-ml_val use_string : string -> unit =
-procedure(str) with_props use_string;
-        lvars str;
-        lconstant UseExn = exception("Use");
-
-        define dlocal pop_exception_handler(n, msg, idstring, severity);
-                [n ^n msg ^msg  idstring ^idstring severity ^severity] ==>
-                returnunless(severity == `E` or severity == `R`)(false);
-                erasenum(n);
-                raise(UseExn(str));
-        enddefine;
-
-        ml_compile(stringin(str));
-        ml_unit;
-endprocedure;
-
-endsection;
-ml'
-  DB=""
-else
-  EXIT=""
-  USE=""
-  DB="+$INFILE"
-fi
-
-if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);'
-else
-  ML_OPTIONS="$ML_OPTIONS -nort"
-  if [ -z "$NOWRITE" ]; then
-    COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;"
-  else
-    COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = true, share = true, banner = false, init = false} then System.restart() else true;"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-POPLOG="$ML_HOME/poplog"
-check_mlhome_file "$POPLOG"
-
-INIT="$ISABELLE_TMP/init.ml"
-echo 'pop11
-section $-ml;
-false -> ml_quiet;
-endsection;
-ml' > "$INIT"
-
-echo "$EXIT $USE $COMMIT $MLTEXT" >> "$INIT"
-
-if [ -n "$TERMINATE" ]; then
-  ML_OPTIONS="$ML_OPTIONS -nostdin"
-  echo "commit();" >> "$INIT"
-fi
-
-"$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
-RC="$?"
-
-rm -f "$INIT"
-
-if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then
-  [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-  rm -f "$OUTFILE-"
-fi
-
-exit "$RC"
diff -r e0323036bcf2 -r 1a604efd267d src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Sat Jun 14 17:26:09 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,378 +0,0 @@
-(*  Title:      Pure/ML-Systems/poplogml.ML
-    ID:         $Id$
-    Author:     Makarius
-
-Compatibility file for Poplog/PML (version 15.6/2.1).
-*)
-
-(* Compiler and runtime options *)
-
-val ml_system_fix_ints = false;
-
-val _ = Compile.filetype := ".ML";
-val _ = Memory.hilim := let fun MB n = n div 4 * 1024 * 1024 in MB 120 end;
-val _ = Memory.stacklim := 10 * ! Memory.stacklim;
-
-fun pointer_eq (_: 'a, _: 'a) = false;
-
-
-(* ML toplevel *)
-
-fun ml_prompts p1 p2 = ();
-
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-fun get_print_depth () = 10;
-fun print_depth _ = ();
-
-fun exception_trace f = f ();
-fun profile (n: int) f x = f x;
-
-
-
-(** Basis structures **)
-
-structure General =
-struct
-  exception Subscript = Array.Subscript;
-  exception Size;
-  exception Fail of string;
-  fun exnMessage (exn: exn) = "exception " ^ makestring exn ^ " raised";
-  datatype order = LESS | EQUAL | GREATER;
-end;
-open General;
-
-structure Bool =
-struct
-  val toString: bool -> string = makestring;
-end;
-
-structure Option =
-struct
-  open Option;
-  exception Option;
-
-  fun valOf (SOME x) = x
-    | valOf NONE = raise Option;
-
-  fun getOpt (SOME x, _) = x
-    | getOpt (NONE, x) = x;
-
-  fun isSome (SOME _) = true
-    | isSome NONE = false;
-end;
-open Option;
-
-structure Option =
-struct
-  open Option;
-  fun map f (SOME x) = SOME (f x)
-    | map _ NONE = NONE;
-end;
-
-structure Int =
-struct
-  open Int;
-  type int = int;
-  val toString: int -> string = makestring;
-  fun fromInt (i: int) = i;
-  val fromString = String.stringint;
-  val op + = op + : int * int -> int;
-  val op - = op - : int * int -> int;
-  val op * = op * : int * int -> int;
-  val op div = op div : int * int -> int;
-  val op mod = op mod : int * int -> int;
-  fun pow (x, y) = power x y : int;
-  val op < = op < : int * int -> bool;
-  val op > = op > : int * int -> bool;
-  val op <= = op <= : int * int -> bool;
-  val op >= = op >= : int * int -> bool;
-  val abs = abs: int -> int;
-  val sign = sign: int -> int;
-  fun max (x, y) : int = if x < y then y else x;
-  fun min (x, y) : int = if x < y then x else y;
-  fun compare (x: int, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
-end;
-
-structure IntInf = Int;
-
-structure Real =
-struct
-  open Real;
-  val toString: real -> string = makestring;
-  fun max (x, y) : real = if x < y then y else x;
-  fun min (x, y) : real = if x < y then x else y;
-  val real = real;
-  val floor = floor;
-  val realFloor = real o floor;
-  fun ceil x = ~1 - floor (~ (x + 1.0));
-  fun round x = floor (x + 0.5);  (*does not do round-to-nearest*)
-  fun trunc x = if x < 0.0 then ceil x else floor x;
-end;
-
-structure String =
-struct
-  open String;
-  type char = string
-  fun str (c: char) = c: string;
-  val translate = mapstring;
-  val isPrefix = isprefix;
-  val isSuffix = issuffix;
-  val size = size;
-  fun compare (x: string, y) = if x = y then EQUAL else if x < y then LESS else GREATER;
-  fun substring (s, i, n) = String.substring i (i + n) s
-    handle String.Substring => raise Subscript;
-end;
-
-structure List =
-struct
-  open List;
-
-  exception Empty;
-  fun null [] = true | null _ = false;
-  fun hd (x :: _) = x | hd _ = raise Empty;
-  fun tl (_ :: xs) = xs | tl _ = raise Empty;
-  val map = map;
-
-  fun foldl f b [] = b
-    | foldl f b (x :: xs) = foldl f (f (x, b)) xs;
-
-  fun foldr f b [] = b
-    | foldr f b (x :: xs) = f (x, foldr f b xs);
-
-  fun last []      = raise Empty
-    | last [x]     = x
-    | last (x::xs) = last xs;
-
-  fun nth (xs, n) =
-      let fun h []      _ = raise Subscript
-            | h (x::xs) n = if n=0 then x else h xs (n-1)
-      in if n<0 then raise Subscript else h xs n end;
-
-  fun drop (xs, n) =
-      let fun h xs      0 = xs
-            | h []      n = raise Subscript
-            | h (x::xs) n = h xs (n-1)
-      in if n<0 then raise Subscript else h xs n end;
-
-  fun take (xs, n) =
-      let fun h xs      0 = []
-            | h []      n = raise Subscript
-            | h (x::xs) n = x :: h xs (n-1)
-      in if n<0 then raise Subscript else h xs n end;
-
-  fun concat []      = []
-    | concat (l::ls) = l @ concat ls;
-
-  fun mapPartial f []      = []
-    | mapPartial f (x::xs) =
-         (case f x of NONE   => mapPartial f xs
-                    | SOME y => y :: mapPartial f xs);
-
-  fun find _ []        = NONE
-    | find p (x :: xs) = if p x then SOME x else find p xs;
-
-
-  (*copy the list preserving elements that satisfy the predicate*)
-  fun filter p [] = []
-    | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
-
-  (*Partition list into elements that satisfy predicate and those that don't.
-    Preserves order of elements in both lists.*)
-  fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
-      let fun part ([], answer) = answer
-            | part (x::xs, (ys, ns)) = if p(x)
-              then  part (xs, (x::ys, ns))
-              else  part (xs, (ys, x::ns))
-      in  part (rev ys, ([], []))  end;
-
-end;
-exception Empty = List.Empty;
-val null = List.null;
-val hd = List.hd;
-val tl = List.tl;
-val map = List.map;
-val foldl = List.foldl;
-val foldr = List.foldr;
-val app = List.app;
-val length = List.length;
-
-structure ListPair =
-struct
-  fun zip ([], [])      = []
-    | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
-
-  fun unzip [] = ([],[])
-    | unzip((x,y)::pairs) =
-          let val (xs,ys) = unzip pairs
-          in  (x::xs, y::ys)  end;
-
-  fun app f (x::xs, y::ys) = (f (x, y); app f (xs, ys))
-    | app f _ = ();
-
-  fun map f ([], [])      = []
-    | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
-
-  fun exists p =
-    let fun boolf ([], [])      = false
-          | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
-    in boolf end;
-
-  fun all p =
-    let fun boolf ([], [])      = true
-          | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
-    in boolf end;
-end;
-
-structure TextIO =
-struct
-  type instream = instream;
-  type outstream = outstream;
-  exception Io = Io;
-  val stdIn = std_in;
-  val stdOut = std_out;
-  val stdErr = std_err;
-  val openIn = open_in;
-  val openAppend = open_append;
-  val openOut = open_out;
-  val closeIn = close_in;
-  val closeOut = close_out;
-  val inputN = input;
-  val inputAll = fn is => inputN (is, 1000000000);
-  val inputLine = input_line;
-  val endOfStream = end_of_stream;
-  val output = output;
-  val flushOut = flush_out;
-end;
-
-
-
-(** Compiler-independent timing functions **)
-
-fun start_timing() = "FIXME";
-fun end_timing (s: string) = s;
-fun check_timer _ = (0, 0, 0);
-
-structure Timer =
-struct
-  type cpu_timer = int;
-  fun startCPUTimer () = 0;
-end;
-
-structure Time =
-struct
-  exception Time;
-  type time = int;
-  val toString: time -> string = makestring;
-  val zeroTime = 0;
-  fun now () = 0;
-  fun (x: int) + y = x + y;
-  fun (x: int) - y = x - y;
-end;
-
-
-
-(** interrupts **)      (*Note: may get into race conditions*)
-
-fun interruptible f x = f x;
-fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
-
-
-
-(** OS related **)
-
-val tmp_name =
-  let val count = ref 0 in
-    fn () => (count := ! count + 1;
-      "/tmp/pml" ^ Int.toString (OS.pid ()) ^ "." ^ Int.toString (! count))
-  end;
-
-local
-
-fun shell cmdline = OS.execve "/bin/sh" ["sh", "-c", cmdline] (OS.envlist());
-
-fun execute_rc cmdline =
-  let
-    fun wait pid =
-      (case OS.wait () of
-        NONE => wait pid
-      | SOME (pid', rc) =>
-          if pid = pid' then rc div 256 else raise OS.Error ("wait", "wrong pid", ""));
-  in
-    (case OS.fork () of
-      NONE => shell cmdline
-    | SOME pid => wait pid)
-  end;
-
-fun squote s = "'" ^ s ^ "'";
-fun remove name = (execute_rc ("/bin/rm -- " ^ squote name); ());
-fun is_dir name = execute_rc ("perl -e \"exit (-d " ^ squote name ^ " ? 0 : 1)\"") = 0;
-
-fun execute_result cmdline =
-  let
-    val tmp = tmp_name ();
-    val rc = execute_rc (cmdline  ^ " > " ^ tmp);
-    val instream = TextIO.openIn tmp;
-    val result = TextIO.inputAll instream;
-    val _ = TextIO.closeIn instream;
-    val _ = remove tmp;
-  in (rc, result) end;
-
-in
-
-fun exit rc = shell ("exit " ^ Int.toString rc);
-fun quit () = exit 0;
-
-fun execute cmdline = #2 (execute_result cmdline);
-
-fun system cmdline =
-  let val (rc, result) = execute_result cmdline
-  in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end;
-
-val string_of_pid: int -> string = makestring;
-
-fun getenv var = (case OS.translate var of NONE => "" | SOME s => s);
-
-structure OS =
-struct
-  structure FileSys =
-  struct
-    val tmpName = tmp_name;
-    val chDir = OS.cd;
-    val getDir = OS.pwd;
-    val remove = remove;
-    val isDir = is_dir;
-    val compare = Int.compare;
-
-    fun modTime name =
-      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[9]'") of
-        "" => raise TextIO.Io "OS.FileSys.modTime"
-      | s => Int.fromString s);
-    fun fileId name =
-      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
-        "" => raise TextIO.Io "OS.FileSys.fileId"
-      | s => Int.fromString s);
-  end;
-end;
-
-end;
-
-
-(* use *)
-
-local val pml_use = use in
-
-fun use name =
-  if name = "ROOT.ML" then   (*workaround error about looping compilations*)
-    let
-      val instream = TextIO.openIn name;
-      val txt = TextIO.inputAll instream;
-      val _ = TextIO.closeIn;
-    in use_string txt end
-  else pml_use name;
-
-end;
-
-fun use_text _ _ _ _ txt = use_string txt;
-fun use_file _ _ _ name = use name;