# HG changeset patch
# User wenzelm
# Date 1457038761 -3600
# Node ID d0b68218ea5524e95bc5b7354ce12d0427b94013
# Parent  15c36c181130c06a6da590ce2a9ee7ef58d19345
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;

diff -r 15c36c181130 -r d0b68218ea55 src/Pure/Concurrent/multithreading.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/multithreading.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,196 @@
+(*  Title:      Pure/Concurrent/multithreading.ML
+    Author:     Makarius
+
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
+*)
+
+signature BASIC_MULTITHREADING =
+sig
+  val interruptible: ('a -> 'b) -> 'a -> 'b
+  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+end;
+
+signature MULTITHREADING =
+sig
+  include BASIC_MULTITHREADING
+  val no_interrupts: Thread.threadAttribute list
+  val public_interrupts: Thread.threadAttribute list
+  val private_interrupts: Thread.threadAttribute list
+  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+  val interrupted: unit -> unit  (*exception Interrupt*)
+  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
+  val max_threads_value: unit -> int
+  val max_threads_update: int -> unit
+  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
+  val enabled: unit -> bool
+  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
+    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
+  val trace: int ref
+  val tracing: int -> (unit -> string) -> unit
+  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
+  val real_time: ('a -> unit) -> 'a -> Time.time
+  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
+  val serial: unit -> int
+end;
+
+structure Multithreading: MULTITHREADING =
+struct
+
+(* thread attributes *)
+
+val no_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+
+val test_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
+val public_interrupts =
+  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+
+val private_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
+val sync_interrupts = map
+  (fn x as Thread.InterruptState Thread.InterruptDefer => x
+    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
+    | x => x);
+
+val safe_interrupts = map
+  (fn Thread.InterruptState Thread.InterruptAsynch =>
+      Thread.InterruptState Thread.InterruptAsynchOnce
+    | x => x);
+
+fun interrupted () =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val _ = Thread.setAttributes test_interrupts;
+    val test = Exn.capture Thread.testInterrupt ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release test end;
+
+fun with_attributes new_atts e =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val result = Exn.capture (fn () =>
+      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release result end;
+
+
+(* portable wrappers *)
+
+fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
+
+fun uninterruptible f x =
+  with_attributes no_interrupts (fn atts =>
+    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+
+
+(* options *)
+
+fun num_processors () =
+  (case Thread.numPhysicalProcessors () of
+    SOME n => n
+  | NONE => Thread.numProcessors ());
+
+fun max_threads_result m =
+  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
+
+val max_threads = ref 1;
+
+fun max_threads_value () = ! max_threads;
+
+fun max_threads_update m = max_threads := max_threads_result m;
+
+fun max_threads_setmp m f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val max_threads_orig = ! max_threads;
+      val _ = max_threads_update m;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = max_threads := max_threads_orig;
+    in Exn.release result end) ();
+
+fun enabled () = max_threads_value () > 1;
+
+
+(* synchronous wait *)
+
+fun sync_wait opt_atts time cond lock =
+  with_attributes
+    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+    (fn _ =>
+      (case time of
+        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
+      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
+      handle exn => Exn.Exn exn);
+
+
+(* tracing *)
+
+val trace = ref 0;
+
+fun tracing level msg =
+  if level > ! trace then ()
+  else uninterruptible (fn _ => fn () =>
+    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
+      handle _ (*sic*) => ()) ();
+
+fun tracing_time detailed time =
+  tracing
+   (if not detailed then 5
+    else if Time.>= (time, seconds 1.0) then 1
+    else if Time.>= (time, seconds 0.1) then 2
+    else if Time.>= (time, seconds 0.01) then 3
+    else if Time.>= (time, seconds 0.001) then 4 else 5);
+
+fun real_time f x =
+  let
+    val timer = Timer.startRealTimer ();
+    val () = f x;
+    val time = Timer.checkRealTimer timer;
+  in time end;
+
+
+(* synchronized evaluation *)
+
+fun synchronized name lock e =
+  Exn.release (uninterruptible (fn restore_attributes => fn () =>
+    let
+      val immediate =
+        if Mutex.trylock lock then true
+        else
+          let
+            val _ = tracing 5 (fn () => name ^ ": locking ...");
+            val time = real_time Mutex.lock lock;
+            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
+          in false end;
+      val result = Exn.capture (restore_attributes e) ();
+      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
+      val _ = Mutex.unlock lock;
+    in result end) ());
+
+
+(* serial numbers *)
+
+local
+
+val serial_lock = Mutex.mutex ();
+val serial_count = ref 0;
+
+in
+
+val serial = uninterruptible (fn _ => fn () =>
+  let
+    val _ = Mutex.lock serial_lock;
+    val _ = serial_count := ! serial_count + 1;
+    val res = ! serial_count;
+    val _ = Mutex.unlock serial_lock;
+  in res end);
+
+end;
+
+end;
+
+structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
+open Basic_Multithreading;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/Concurrent/unsynchronized.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/unsynchronized.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,30 @@
+(*  Title:      Pure/Concurrent/unsynchronized.ML
+    Author:     Makarius
+
+Raw ML references as unsynchronized state variables.
+*)
+
+structure Unsynchronized =
+struct
+
+datatype ref = datatype ref;
+
+val op := = op :=;
+val ! = !;
+
+fun change r f = r := f (! r);
+fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
+
+fun inc i = (i := ! i + (1: int); ! i);
+fun dec i = (i := ! i - (1: int); ! i);
+
+fun setmp flag value f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val orig_value = ! flag;
+      val _ = flag := value;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = flag := orig_value;
+    in Exn.release result end) ();
+
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/General/exn.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,134 @@
+(*  Title:      Pure/General/exn.ML
+    Author:     Makarius
+
+Support for exceptions.
+*)
+
+signature BASIC_EXN =
+sig
+  exception ERROR of string
+  val error: string -> 'a
+  val cat_error: string -> string -> 'a
+end;
+
+signature EXN =
+sig
+  include BASIC_EXN
+  val reraise: exn -> 'a
+  datatype 'a result = Res of 'a | Exn of exn
+  val get_res: 'a result -> 'a option
+  val get_exn: 'a result -> exn option
+  val capture: ('a -> 'b) -> 'a -> 'b result
+  val release: 'a result -> 'a
+  val map_res: ('a -> 'b) -> 'a result -> 'b result
+  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
+  val map_exn: (exn -> exn) -> 'a result -> 'a result
+  exception Interrupt
+  val interrupt: unit -> 'a
+  val is_interrupt: exn -> bool
+  val interrupt_exn: 'a result
+  val is_interrupt_exn: 'a result -> bool
+  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val return_code: exn -> int -> int
+  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
+  exception EXCEPTIONS of exn list
+  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
+end;
+
+structure Exn: EXN =
+struct
+
+(* reraise *)
+
+fun reraise exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => raise exn
+  | SOME location => PolyML.raiseWithLocation (exn, location));
+
+
+(* user errors *)
+
+exception ERROR of string;
+
+fun error msg = raise ERROR msg;
+
+fun cat_error "" msg = error msg
+  | cat_error msg "" = error msg
+  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
+
+
+(* exceptions as values *)
+
+datatype 'a result =
+  Res of 'a |
+  Exn of exn;
+
+fun get_res (Res x) = SOME x
+  | get_res _ = NONE;
+
+fun get_exn (Exn exn) = SOME exn
+  | get_exn _ = NONE;
+
+fun capture f x = Res (f x) handle e => Exn e;
+
+fun release (Res y) = y
+  | release (Exn e) = reraise e;
+
+fun map_res f (Res x) = Res (f x)
+  | map_res f (Exn e) = Exn e;
+
+fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
+
+fun map_exn f (Res x) = Res x
+  | map_exn f (Exn e) = Exn (f e);
+
+
+(* interrupts *)
+
+exception Interrupt = SML90.Interrupt;
+
+fun interrupt () = raise Interrupt;
+
+fun is_interrupt Interrupt = true
+  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
+  | is_interrupt _ = false;
+
+val interrupt_exn = Exn Interrupt;
+
+fun is_interrupt_exn (Exn exn) = is_interrupt exn
+  | is_interrupt_exn _ = false;
+
+fun interruptible_capture f x =
+  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
+
+
+(* POSIX return code *)
+
+fun return_code exn rc =
+  if is_interrupt exn then (130: int) else rc;
+
+fun capture_exit rc f x =
+  f x handle exn => exit (return_code exn rc);
+
+
+(* concatenated exceptions *)
+
+exception EXCEPTIONS of exn list;
+
+
+(* low-level trace *)
+
+fun trace exn_message output e =
+  PolyML.Exception.traceException
+    (e, fn (trace, exn) =>
+      let
+        val title = "Exception trace - " ^ exn_message exn;
+        val () = output (String.concatWith "\n" (title :: trace));
+      in reraise exn end);
+
+end;
+
+datatype illegal = Interrupt;
+
+structure Basic_Exn: BASIC_EXN = Exn;
+open Basic_Exn;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/General/exn.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.scala	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,137 @@
+/*  Title:      Pure/General/exn.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Support for exceptions (arbitrary throwables).
+*/
+
+package isabelle
+
+
+object Exn
+{
+  /* user errors */
+
+  class User_Error(message: String) extends RuntimeException(message)
+  {
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: User_Error => message == other.getMessage
+        case _ => false
+      }
+    override def hashCode: Int = message.hashCode
+
+    override def toString: String = "ERROR(" + message + ")"
+  }
+
+  object ERROR
+  {
+    def apply(message: String): User_Error = new User_Error(message)
+    def unapply(exn: Throwable): Option[String] = user_message(exn)
+  }
+
+  def error(message: String): Nothing = throw ERROR(message)
+
+  def cat_message(msg1: String, msg2: String): String =
+    if (msg1 == "") msg2
+    else if (msg2 == "") msg1
+    else msg1 + "\n" + msg2
+
+  def cat_error(msg1: String, msg2: String): Nothing =
+    error(cat_message(msg1, msg2))
+
+
+  /* exceptions as values */
+
+  sealed abstract class Result[A]
+  {
+    def user_error: Result[A] =
+      this match {
+        case Exn(ERROR(msg)) => Exn(ERROR(msg))
+        case _ => this
+      }
+  }
+  case class Res[A](res: A) extends Result[A]
+  case class Exn[A](exn: Throwable) extends Result[A]
+
+  def capture[A](e: => A): Result[A] =
+    try { Res(e) }
+    catch { case exn: Throwable => Exn[A](exn) }
+
+  def release[A](result: Result[A]): A =
+    result match {
+      case Res(x) => x
+      case Exn(exn) => throw exn
+    }
+
+  def release_first[A](results: List[Result[A]]): List[A] =
+    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
+      case Some(Exn(exn)) => throw exn
+      case _ => results.map(release(_))
+    }
+
+
+  /* interrupts */
+
+  def is_interrupt(exn: Throwable): Boolean =
+  {
+    var found_interrupt = false
+    var e = exn
+    while (!found_interrupt && e != null) {
+      found_interrupt |= e.isInstanceOf[InterruptedException]
+      e = e.getCause
+    }
+    found_interrupt
+  }
+
+  object Interrupt
+  {
+    def apply(): Throwable = new InterruptedException
+    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+
+    def expose() { if (Thread.interrupted) throw apply() }
+    def impose() { Thread.currentThread.interrupt }
+
+    def postpone[A](body: => A): Option[A] =
+    {
+      val interrupted = Thread.interrupted
+      val result = capture { body }
+      if (interrupted) impose()
+      result match {
+        case Res(x) => Some(x)
+        case Exn(e) =>
+          if (is_interrupt(e)) { impose(); None }
+          else throw e
+      }
+    }
+
+    val return_code = 130
+  }
+
+
+  /* POSIX return code */
+
+  def return_code(exn: Throwable, rc: Int): Int =
+    if (is_interrupt(exn)) Interrupt.return_code else rc
+
+
+  /* message */
+
+  def user_message(exn: Throwable): Option[String] =
+    if (exn.getClass == classOf[RuntimeException] ||
+        exn.getClass == classOf[User_Error])
+    {
+      val msg = exn.getMessage
+      Some(if (msg == null || msg == "") "Error" else msg)
+    }
+    else if (exn.isInstanceOf[java.io.IOException])
+    {
+      val msg = exn.getMessage
+      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
+    }
+    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
+    else None
+
+  def message(exn: Throwable): String =
+    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
+}
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/General/secure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/secure.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,27 @@
+(*  Title:      Pure/General/secure.ML
+    Author:     Makarius
+
+Secure critical operations.
+*)
+
+signature SECURE =
+sig
+  val set_secure: unit -> unit
+  val is_secure: unit -> bool
+  val deny: string -> unit
+  val deny_ml: unit -> unit
+end;
+
+structure Secure: SECURE =
+struct
+
+val secure = Unsynchronized.ref false;
+
+fun set_secure () = secure := true;
+fun is_secure () = ! secure;
+
+fun deny msg = if is_secure () then error msg else ();
+
+fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
+
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/fixed_int_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/fixed_int_dummy.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,6 @@
+(*  Title:      Pure/ML/fixed_int_dummy.ML
+
+FixedInt dummy that is not fixed (up to Poly/ML 5.6).
+*)
+
+structure FixedInt = IntInf;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_compiler0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler0.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,110 @@
+(*  Title:      Pure/ML/ml_compiler0.ML
+
+Runtime compilation and evaluation (bootstrap version of
+Pure/ML/ml_compiler.ML).
+*)
+
+signature ML_COMPILER0 =
+sig
+  type context =
+   {name_space: ML_Name_Space.T,
+    here: int -> string -> string,
+    print: string -> unit,
+    error: string -> unit}
+  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
+  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
+  val debug_option: bool option -> bool
+  val use_operations: (bool option -> string -> unit) ->
+    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
+end;
+
+structure ML_Compiler0: ML_COMPILER0 =
+struct
+
+type context =
+ {name_space: ML_Name_Space.T,
+  here: int -> string -> string,
+  print: string -> unit,
+  error: string -> unit};
+
+fun drop_newline s =
+  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+  else s;
+
+fun ml_positions start_line name txt =
+  let
+    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+          in positions line cs (s :: res) end
+      | positions line (c :: cs) res =
+          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+      | positions _ [] res = rev res;
+  in String.concat (positions start_line (String.explode txt) []) end;
+
+fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
+  let
+    val _ = Secure.deny_ml ();
+
+    val current_line = Unsynchronized.ref line;
+    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
+    val out_buffer = Unsynchronized.ref ([]: string list);
+    fun output () = drop_newline (implode (rev (! out_buffer)));
+
+    fun get () =
+      (case ! in_buffer of
+        [] => NONE
+      | c :: cs =>
+          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+    fun put s = out_buffer := s :: ! out_buffer;
+    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
+     (put (if hard then "Error: " else "Warning: ");
+      PolyML.prettyPrint (put, 76) msg1;
+      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
+
+    val parameters =
+     [PolyML.Compiler.CPOutStream put,
+      PolyML.Compiler.CPNameSpace name_space,
+      PolyML.Compiler.CPErrorMessageProc put_message,
+      PolyML.Compiler.CPLineNo (fn () => ! current_line),
+      PolyML.Compiler.CPFileName file,
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+      PolyML.Compiler.CPDebug debug];
+    val _ =
+      (while not (List.null (! in_buffer)) do
+        PolyML.compiler (get, parameters) ())
+      handle exn =>
+        if Exn.is_interrupt exn then Exn.reraise exn
+        else
+         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+          error (output ()); Exn.reraise exn);
+  in if verbose then print (output ()) else () end;
+
+fun use_file context {verbose, debug} file =
+  let
+    val instream = TextIO.openIn file;
+    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+
+
+fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
+  | debug_option (SOME debug) = debug;
+
+fun use_operations (use_ : bool option -> string -> unit) =
+  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
+
+end;
+
+val {use, use_debug, use_no_debug} =
+  let
+    val context: ML_Compiler0.context =
+     {name_space = ML_Name_Space.global,
+      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
+      error = fn s => error s};
+  in
+    ML_Compiler0.use_operations (fn opt_debug => fn file =>
+      ML_Compiler0.use_file context
+        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
+      handle ERROR msg => (#print context msg; raise error "ML error"))
+  end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_debugger.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_debugger.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,72 @@
+(*  Title:      Pure/ML/ml_debugger.ML
+    Author:     Makarius
+
+ML debugger interface -- for Poly/ML 5.6, or later.
+*)
+
+signature ML_DEBUGGER =
+sig
+  type exn_id
+  val exn_id: exn -> exn_id
+  val print_exn_id: exn_id -> string
+  val eq_exn_id: exn_id * exn_id -> bool
+  type location
+  val on_entry: (string * location -> unit) option -> unit
+  val on_exit: (string * location -> unit) option -> unit
+  val on_exit_exception: (string * location -> exn -> unit) option -> unit
+  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
+  type state
+  val state: Thread.thread -> state list
+  val debug_function: state -> string
+  val debug_function_arg: state -> ML_Name_Space.valueVal
+  val debug_function_result: state -> ML_Name_Space.valueVal
+  val debug_location: state -> location
+  val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
+end;
+
+structure ML_Debugger: ML_DEBUGGER =
+struct
+
+(* exceptions *)
+
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
+with
+
+fun exn_id exn =
+  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
+
+fun print_exn_id (Exn_Id (name, _)) = name;
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
+
+end;
+
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+    let val s = print_exn_id exn_id
+    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
+
+
+(* hooks *)
+
+type location = PolyML.location;
+
+val on_entry = PolyML.DebuggerInterface.setOnEntry;
+val on_exit = PolyML.DebuggerInterface.setOnExit;
+val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
+val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
+
+
+(* debugger operations *)
+
+type state = PolyML.DebuggerInterface.debugState;
+
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
+
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_heap.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_heap.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,17 @@
+(*  Title:      Pure/ML/ml_heap.ML
+    Author:     Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+  val share_common_data: unit -> unit
+  val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_name_space.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,41 @@
+(*  Title:      Pure/ML/ml_name_space.ML
+    Author:     Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+
+  type valueVal = Values.value;
+  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
+  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+  val initial_val =
+    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+      (#allVal global ());
+
+  type typeVal = TypeConstrs.typeConstr;
+  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+  val initial_type = #allType global ();
+
+  type fixityVal = Infixes.fixity;
+  fun displayFix (_: string, x) = Infixes.print x;
+  val initial_fixity = #allFix global ();
+
+  type structureVal = Structures.structureVal;
+  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+  val initial_structure = #allStruct global ();
+
+  type signatureVal = Signatures.signatureVal;
+  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+  val initial_signature = #allSig global ();
+
+  type functorVal = Functors.functorVal;
+  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+  val initial_functor = #allFunct global ();
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_pretty.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,84 @@
+(*  Title:      Pure/ML/ml_pretty.ML
+    Author:     Makarius
+
+Minimal support for raw ML pretty printing, notably for toplevel pp.
+*)
+
+signature ML_PRETTY =
+sig
+  datatype pretty =
+    Block of (string * string) * bool * FixedInt.int * pretty list |
+    String of string * FixedInt.int |
+    Break of bool * FixedInt.int * FixedInt.int
+  val block: pretty list -> pretty
+  val str: string -> pretty
+  val brk: FixedInt.int -> pretty
+  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
+  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
+  val to_polyml: pretty -> PolyML.pretty
+  val from_polyml: PolyML.pretty -> pretty
+end;
+
+structure ML_Pretty: ML_PRETTY =
+struct
+
+datatype pretty =
+  Block of (string * string) * bool * FixedInt.int * pretty list |
+  String of string * FixedInt.int |
+  Break of bool * FixedInt.int * FixedInt.int;
+
+fun block prts = Block (("", ""), false, 2, prts);
+fun str s = String (s, FixedInt.fromInt (size s));
+fun brk width = Break (false, width, 0);
+
+fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
+  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+
+fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
+  let
+    fun elems _ [] = []
+      | elems 0 _ = [str "..."]
+      | elems d [x] = [pretty (x, d)]
+      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
+  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
+
+
+(* convert *)
+
+fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
+  | to_polyml (Break (true, _, _)) =
+      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+        [PolyML.PrettyString " "])
+  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
+      let val context =
+        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
+  | to_polyml (String (s, len)) =
+      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
+      else
+        PolyML.PrettyBlock
+          (0, false,
+            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
+
+val from_polyml =
+  let
+    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
+      | convert _ (PolyML.PrettyBlock (_, _,
+            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
+          Break (true, 1, 0)
+      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
+          let
+            fun property name default =
+              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (PolyML.ContextProperty (_, b)) => b
+              | _ => default);
+            val bg = property "begin" "";
+            val en = property "end" "";
+            val len' = property "length" len;
+          in Block ((bg, en), consistent, ind, map (convert len') prts) end
+      | convert len (PolyML.PrettyString s) =
+          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
+  in convert "" end;
+
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_profiling.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_profiling.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/ML/ml_profiling.ML
+    Author:     Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ML/ml_system.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_system.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -0,0 +1,58 @@
+(*  Title:      Pure/ML/ml_system.ML
+    Author:     Makarius
+
+ML system and platform operations.
+*)
+
+signature ML_SYSTEM =
+sig
+  val name: string
+  val platform: string
+  val platform_is_windows: bool
+  val platform_path: string -> string
+  val standard_path: string -> string
+end;
+
+structure ML_System: ML_SYSTEM =
+struct
+
+val SOME name = OS.Process.getEnv "ML_SYSTEM";
+val SOME platform = OS.Process.getEnv "ML_PLATFORM";
+val platform_is_windows = String.isSuffix "windows" platform;
+
+val platform_path =
+  if platform_is_windows then
+    fn path =>
+      if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
+        (case String.tokens (fn c => c = #"/") path of
+          "cygdrive" :: drive :: arcs =>
+            let
+              val vol =
+                (case Char.fromString drive of
+                  NONE => drive ^ ":"
+                | SOME d => String.str (Char.toUpper d) ^ ":");
+            in String.concatWith "\\" (vol :: arcs) end
+        | arcs =>
+            (case OS.Process.getEnv "CYGWIN_ROOT" of
+              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
+            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
+      else String.translate (fn #"/" => "\\" | c => String.str c) path
+  else fn path => path;
+
+val standard_path =
+  if platform_is_windows then
+    fn path =>
+      let
+        val {vol, arcs, isAbs} = OS.Path.fromString path;
+        val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
+      in
+        if isAbs then
+          (case String.explode vol of
+            [d, #":"] =>
+              String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
+          | _ => path')
+        else path'
+      end
+  else fn path => path;
+
+end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_polyml.ML
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML.
-*)
-
-(* initial ML name space *)
-
-use "RAW/ml_system.ML";
-use "RAW/ml_name_space.ML";
-
-if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
-else use "RAW/fixed_int_dummy.ML";
-
-
-(* exceptions *)
-
-use "RAW/exn.ML";
-
-
-(* multithreading *)
-
-val seconds = Time.fromReal;
-
-open Thread;
-use "RAW/multithreading.ML";
-
-use "RAW/unsynchronized.ML";
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-
-(* pervasive environment *)
-
-val _ = PolyML.Compiler.forgetValue "isSome";
-val _ = PolyML.Compiler.forgetValue "getOpt";
-val _ = PolyML.Compiler.forgetValue "valOf";
-val _ = PolyML.Compiler.forgetValue "foldl";
-val _ = PolyML.Compiler.forgetValue "foldr";
-val _ = PolyML.Compiler.forgetValue "print";
-val _ = PolyML.Compiler.forgetValue "explode";
-val _ = PolyML.Compiler.forgetValue "concat";
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-fun quit () = exit 0;
-
-
-(* ML runtime system *)
-
-use "RAW/ml_heap.ML";
-use "RAW/ml_profiling.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-
-(* ML toplevel pretty printing *)
-
-use "RAW/ml_pretty.ML";
-
-local
-  val depth = Unsynchronized.ref 10;
-in
-  fun get_default_print_depth () = ! depth;
-  fun default_print_depth n = (depth := n; PolyML.print_depth n);
-  val _ = default_print_depth 10;
-end;
-
-val error_depth = PolyML.error_depth;
-
-
-(* ML compiler *)
-
-use "RAW/secure.ML";
-use "RAW/ml_compiler0.ML";
-
-PolyML.Compiler.reportUnreferencedIds := true;
-PolyML.Compiler.reportExhaustiveHandlers := true;
-PolyML.Compiler.printInAlphabeticalOrder := false;
-PolyML.Compiler.maxInlineSize := 80;
-PolyML.Compiler.prompt1 := "ML> ";
-PolyML.Compiler.prompt2 := "ML# ";
-
-fun ml_make_string struct_name =
-  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
-    struct_name ^ ".ML_print_depth ()))))))";
-
-
-(* ML debugger *)
-
-use_no_debug "RAW/ml_debugger.ML";
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/exn.ML
--- a/src/Pure/RAW/exn.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(*  Title:      Pure/RAW/exn.ML
-    Author:     Makarius
-
-Support for exceptions.
-*)
-
-signature BASIC_EXN =
-sig
-  exception ERROR of string
-  val error: string -> 'a
-  val cat_error: string -> string -> 'a
-end;
-
-signature EXN =
-sig
-  include BASIC_EXN
-  val reraise: exn -> 'a
-  datatype 'a result = Res of 'a | Exn of exn
-  val get_res: 'a result -> 'a option
-  val get_exn: 'a result -> exn option
-  val capture: ('a -> 'b) -> 'a -> 'b result
-  val release: 'a result -> 'a
-  val map_res: ('a -> 'b) -> 'a result -> 'b result
-  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
-  val map_exn: (exn -> exn) -> 'a result -> 'a result
-  exception Interrupt
-  val interrupt: unit -> 'a
-  val is_interrupt: exn -> bool
-  val interrupt_exn: 'a result
-  val is_interrupt_exn: 'a result -> bool
-  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
-  val return_code: exn -> int -> int
-  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
-  exception EXCEPTIONS of exn list
-  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
-end;
-
-structure Exn: EXN =
-struct
-
-(* reraise *)
-
-fun reraise exn =
-  (case PolyML.exceptionLocation exn of
-    NONE => raise exn
-  | SOME location => PolyML.raiseWithLocation (exn, location));
-
-
-(* user errors *)
-
-exception ERROR of string;
-
-fun error msg = raise ERROR msg;
-
-fun cat_error "" msg = error msg
-  | cat_error msg "" = error msg
-  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
-
-
-(* exceptions as values *)
-
-datatype 'a result =
-  Res of 'a |
-  Exn of exn;
-
-fun get_res (Res x) = SOME x
-  | get_res _ = NONE;
-
-fun get_exn (Exn exn) = SOME exn
-  | get_exn _ = NONE;
-
-fun capture f x = Res (f x) handle e => Exn e;
-
-fun release (Res y) = y
-  | release (Exn e) = reraise e;
-
-fun map_res f (Res x) = Res (f x)
-  | map_res f (Exn e) = Exn e;
-
-fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
-
-fun map_exn f (Res x) = Res x
-  | map_exn f (Exn e) = Exn (f e);
-
-
-(* interrupts *)
-
-exception Interrupt = SML90.Interrupt;
-
-fun interrupt () = raise Interrupt;
-
-fun is_interrupt Interrupt = true
-  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
-  | is_interrupt _ = false;
-
-val interrupt_exn = Exn Interrupt;
-
-fun is_interrupt_exn (Exn exn) = is_interrupt exn
-  | is_interrupt_exn _ = false;
-
-fun interruptible_capture f x =
-  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
-
-
-(* POSIX return code *)
-
-fun return_code exn rc =
-  if is_interrupt exn then (130: int) else rc;
-
-fun capture_exit rc f x =
-  f x handle exn => exit (return_code exn rc);
-
-
-(* concatenated exceptions *)
-
-exception EXCEPTIONS of exn list;
-
-
-(* low-level trace *)
-
-fun trace exn_message output e =
-  PolyML.Exception.traceException
-    (e, fn (trace, exn) =>
-      let
-        val title = "Exception trace - " ^ exn_message exn;
-        val () = output (String.concatWith "\n" (title :: trace));
-      in reraise exn end);
-
-end;
-
-datatype illegal = Interrupt;
-
-structure Basic_Exn: BASIC_EXN = Exn;
-open Basic_Exn;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/exn.scala
--- a/src/Pure/RAW/exn.scala	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-/*  Title:      Pure/RAW/exn.scala
-    Module:     PIDE
-    Author:     Makarius
-
-Support for exceptions (arbitrary throwables).
-*/
-
-package isabelle
-
-
-object Exn
-{
-  /* user errors */
-
-  class User_Error(message: String) extends RuntimeException(message)
-  {
-    override def equals(that: Any): Boolean =
-      that match {
-        case other: User_Error => message == other.getMessage
-        case _ => false
-      }
-    override def hashCode: Int = message.hashCode
-
-    override def toString: String = "ERROR(" + message + ")"
-  }
-
-  object ERROR
-  {
-    def apply(message: String): User_Error = new User_Error(message)
-    def unapply(exn: Throwable): Option[String] = user_message(exn)
-  }
-
-  def error(message: String): Nothing = throw ERROR(message)
-
-  def cat_message(msg1: String, msg2: String): String =
-    if (msg1 == "") msg2
-    else if (msg2 == "") msg1
-    else msg1 + "\n" + msg2
-
-  def cat_error(msg1: String, msg2: String): Nothing =
-    error(cat_message(msg1, msg2))
-
-
-  /* exceptions as values */
-
-  sealed abstract class Result[A]
-  {
-    def user_error: Result[A] =
-      this match {
-        case Exn(ERROR(msg)) => Exn(ERROR(msg))
-        case _ => this
-      }
-  }
-  case class Res[A](res: A) extends Result[A]
-  case class Exn[A](exn: Throwable) extends Result[A]
-
-  def capture[A](e: => A): Result[A] =
-    try { Res(e) }
-    catch { case exn: Throwable => Exn[A](exn) }
-
-  def release[A](result: Result[A]): A =
-    result match {
-      case Res(x) => x
-      case Exn(exn) => throw exn
-    }
-
-  def release_first[A](results: List[Result[A]]): List[A] =
-    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
-      case Some(Exn(exn)) => throw exn
-      case _ => results.map(release(_))
-    }
-
-
-  /* interrupts */
-
-  def is_interrupt(exn: Throwable): Boolean =
-  {
-    var found_interrupt = false
-    var e = exn
-    while (!found_interrupt && e != null) {
-      found_interrupt |= e.isInstanceOf[InterruptedException]
-      e = e.getCause
-    }
-    found_interrupt
-  }
-
-  object Interrupt
-  {
-    def apply(): Throwable = new InterruptedException
-    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
-
-    def expose() { if (Thread.interrupted) throw apply() }
-    def impose() { Thread.currentThread.interrupt }
-
-    def postpone[A](body: => A): Option[A] =
-    {
-      val interrupted = Thread.interrupted
-      val result = capture { body }
-      if (interrupted) impose()
-      result match {
-        case Res(x) => Some(x)
-        case Exn(e) =>
-          if (is_interrupt(e)) { impose(); None }
-          else throw e
-      }
-    }
-
-    val return_code = 130
-  }
-
-
-  /* POSIX return code */
-
-  def return_code(exn: Throwable, rc: Int): Int =
-    if (is_interrupt(exn)) Interrupt.return_code else rc
-
-
-  /* message */
-
-  def user_message(exn: Throwable): Option[String] =
-    if (exn.getClass == classOf[RuntimeException] ||
-        exn.getClass == classOf[User_Error])
-    {
-      val msg = exn.getMessage
-      Some(if (msg == null || msg == "") "Error" else msg)
-    }
-    else if (exn.isInstanceOf[java.io.IOException])
-    {
-      val msg = exn.getMessage
-      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
-    }
-    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
-    else None
-
-  def message(exn: Throwable): String =
-    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
-}
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/fixed_int_dummy.ML
--- a/src/Pure/RAW/fixed_int_dummy.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(*  Title:      Pure/RAW/fixed_int_dummy.ML
-
-FixedInt dummy that is not fixed (up to Poly/ML 5.6).
-*)
-
-structure FixedInt = IntInf;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_compiler0.ML
--- a/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(*  Title:      Pure/RAW/ml_compiler0.ML
-
-Runtime compilation and evaluation (bootstrap version of
-Pure/ML/ml_compiler.ML).
-*)
-
-signature ML_COMPILER0 =
-sig
-  type context =
-   {name_space: ML_Name_Space.T,
-    here: int -> string -> string,
-    print: string -> unit,
-    error: string -> unit}
-  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
-  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
-  val debug_option: bool option -> bool
-  val use_operations: (bool option -> string -> unit) ->
-    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
-end;
-
-structure ML_Compiler0: ML_COMPILER0 =
-struct
-
-type context =
- {name_space: ML_Name_Space.T,
-  here: int -> string -> string,
-  print: string -> unit,
-  error: string -> unit};
-
-fun drop_newline s =
-  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
-  else s;
-
-fun ml_positions start_line name txt =
-  let
-    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
-          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
-          in positions line cs (s :: res) end
-      | positions line (c :: cs) res =
-          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
-      | positions _ [] res = rev res;
-  in String.concat (positions start_line (String.explode txt) []) end;
-
-fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
-  let
-    val _ = Secure.deny_ml ();
-
-    val current_line = Unsynchronized.ref line;
-    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
-    val out_buffer = Unsynchronized.ref ([]: string list);
-    fun output () = drop_newline (implode (rev (! out_buffer)));
-
-    fun get () =
-      (case ! in_buffer of
-        [] => NONE
-      | c :: cs =>
-          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
-    fun put s = out_buffer := s :: ! out_buffer;
-    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
-     (put (if hard then "Error: " else "Warning: ");
-      PolyML.prettyPrint (put, 76) msg1;
-      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
-      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
-
-    val parameters =
-     [PolyML.Compiler.CPOutStream put,
-      PolyML.Compiler.CPNameSpace name_space,
-      PolyML.Compiler.CPErrorMessageProc put_message,
-      PolyML.Compiler.CPLineNo (fn () => ! current_line),
-      PolyML.Compiler.CPFileName file,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
-      PolyML.Compiler.CPDebug debug];
-    val _ =
-      (while not (List.null (! in_buffer)) do
-        PolyML.compiler (get, parameters) ())
-      handle exn =>
-        if Exn.is_interrupt exn then Exn.reraise exn
-        else
-         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-          error (output ()); Exn.reraise exn);
-  in if verbose then print (output ()) else () end;
-
-fun use_file context {verbose, debug} file =
-  let
-    val instream = TextIO.openIn file;
-    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
-
-
-fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
-  | debug_option (SOME debug) = debug;
-
-fun use_operations (use_ : bool option -> string -> unit) =
-  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
-
-end;
-
-val {use, use_debug, use_no_debug} =
-  let
-    val context: ML_Compiler0.context =
-     {name_space = ML_Name_Space.global,
-      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
-      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
-      error = fn s => error s};
-  in
-    ML_Compiler0.use_operations (fn opt_debug => fn file =>
-      ML_Compiler0.use_file context
-        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
-      handle ERROR msg => (#print context msg; raise error "ML error"))
-  end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_debugger.ML
--- a/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      Pure/RAW/ml_debugger.ML
-    Author:     Makarius
-
-ML debugger interface -- for Poly/ML 5.6, or later.
-*)
-
-signature ML_DEBUGGER =
-sig
-  type exn_id
-  val exn_id: exn -> exn_id
-  val print_exn_id: exn_id -> string
-  val eq_exn_id: exn_id * exn_id -> bool
-  type location
-  val on_entry: (string * location -> unit) option -> unit
-  val on_exit: (string * location -> unit) option -> unit
-  val on_exit_exception: (string * location -> exn -> unit) option -> unit
-  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> location
-  val debug_name_space: state -> ML_Name_Space.T
-  val debug_local_name_space: state -> ML_Name_Space.T
-end;
-
-structure ML_Debugger: ML_DEBUGGER =
-struct
-
-(* exceptions *)
-
-abstype exn_id = Exn_Id of string * int Unsynchronized.ref
-with
-
-fun exn_id exn =
-  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
-
-fun print_exn_id (Exn_Id (name, _)) = name;
-fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
-
-end;
-
-val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
-    let val s = print_exn_id exn_id
-    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
-
-
-(* hooks *)
-
-type location = PolyML.location;
-
-val on_entry = PolyML.DebuggerInterface.setOnEntry;
-val on_exit = PolyML.DebuggerInterface.setOnExit;
-val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-
-
-(* debugger operations *)
-
-type state = PolyML.DebuggerInterface.debugState;
-
-val state = PolyML.DebuggerInterface.debugState;
-val debug_function = PolyML.DebuggerInterface.debugFunction;
-val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
-val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
-val debug_location = PolyML.DebuggerInterface.debugLocation;
-val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
-val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
-
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_heap.ML
--- a/src/Pure/RAW/ml_heap.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_heap.ML
-    Author:     Makarius
-
-ML heap operations.
-*)
-
-signature ML_HEAP =
-sig
-  val share_common_data: unit -> unit
-  val save_state: string -> unit
-end;
-
-structure ML_Heap: ML_HEAP =
-struct
-  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_name_space.ML
--- a/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space.ML
-    Author:     Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
-
-  type valueVal = Values.value;
-  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
-  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-  val initial_val =
-    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
-      (#allVal global ());
-
-  type typeVal = TypeConstrs.typeConstr;
-  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-  val initial_type = #allType global ();
-
-  type fixityVal = Infixes.fixity;
-  fun displayFix (_: string, x) = Infixes.print x;
-  val initial_fixity = #allFix global ();
-
-  type structureVal = Structures.structureVal;
-  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-  val initial_structure = #allStruct global ();
-
-  type signatureVal = Signatures.signatureVal;
-  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-  val initial_signature = #allSig global ();
-
-  type functorVal = Functors.functorVal;
-  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-  val initial_functor = #allFunct global ();
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_pretty.ML
--- a/src/Pure/RAW/ml_pretty.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(*  Title:      Pure/RAW/ml_pretty.ML
-    Author:     Makarius
-
-Minimal support for raw ML pretty printing, notably for toplevel pp.
-*)
-
-signature ML_PRETTY =
-sig
-  datatype pretty =
-    Block of (string * string) * bool * FixedInt.int * pretty list |
-    String of string * FixedInt.int |
-    Break of bool * FixedInt.int * FixedInt.int
-  val block: pretty list -> pretty
-  val str: string -> pretty
-  val brk: FixedInt.int -> pretty
-  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
-  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
-  val to_polyml: pretty -> PolyML.pretty
-  val from_polyml: PolyML.pretty -> pretty
-end;
-
-structure ML_Pretty: ML_PRETTY =
-struct
-
-datatype pretty =
-  Block of (string * string) * bool * FixedInt.int * pretty list |
-  String of string * FixedInt.int |
-  Break of bool * FixedInt.int * FixedInt.int;
-
-fun block prts = Block (("", ""), false, 2, prts);
-fun str s = String (s, FixedInt.fromInt (size s));
-fun brk width = Break (false, width, 0);
-
-fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
-  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
-
-fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
-  let
-    fun elems _ [] = []
-      | elems 0 _ = [str "..."]
-      | elems d [x] = [pretty (x, d)]
-      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
-  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
-
-
-(* convert *)
-
-fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
-  | to_polyml (Break (true, _, _)) =
-      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
-        [PolyML.PrettyString " "])
-  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
-      let val context =
-        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
-        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
-      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
-  | to_polyml (String (s, len)) =
-      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
-      else
-        PolyML.PrettyBlock
-          (0, false,
-            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
-
-val from_polyml =
-  let
-    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
-      | convert _ (PolyML.PrettyBlock (_, _,
-            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
-          Break (true, 1, 0)
-      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
-          let
-            fun property name default =
-              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (PolyML.ContextProperty (_, b)) => b
-              | _ => default);
-            val bg = property "begin" "";
-            val en = property "end" "";
-            val len' = property "length" len;
-          in Block ((bg, en), consistent, ind, map (convert len') prts) end
-      | convert len (PolyML.PrettyString s) =
-          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
-  in convert "" end;
-
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_profiling.ML
--- a/src/Pure/RAW/ml_profiling.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/RAW/ml_profiling.ML
-    Author:     Makarius
-
-Profiling for Poly/ML 5.6.
-*)
-
-structure ML_Profiling =
-struct
-
-fun profile_time pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
-
-fun profile_time_thread pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
-
-fun profile_allocations pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
-
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/ml_system.ML
--- a/src/Pure/RAW/ml_system.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      Pure/RAW/ml_system.ML
-    Author:     Makarius
-
-ML system and platform operations.
-*)
-
-signature ML_SYSTEM =
-sig
-  val name: string
-  val platform: string
-  val platform_is_windows: bool
-  val platform_path: string -> string
-  val standard_path: string -> string
-end;
-
-structure ML_System: ML_SYSTEM =
-struct
-
-val SOME name = OS.Process.getEnv "ML_SYSTEM";
-val SOME platform = OS.Process.getEnv "ML_PLATFORM";
-val platform_is_windows = String.isSuffix "windows" platform;
-
-val platform_path =
-  if platform_is_windows then
-    fn path =>
-      if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
-        (case String.tokens (fn c => c = #"/") path of
-          "cygdrive" :: drive :: arcs =>
-            let
-              val vol =
-                (case Char.fromString drive of
-                  NONE => drive ^ ":"
-                | SOME d => String.str (Char.toUpper d) ^ ":");
-            in String.concatWith "\\" (vol :: arcs) end
-        | arcs =>
-            (case OS.Process.getEnv "CYGWIN_ROOT" of
-              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
-            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
-      else String.translate (fn #"/" => "\\" | c => String.str c) path
-  else fn path => path;
-
-val standard_path =
-  if platform_is_windows then
-    fn path =>
-      let
-        val {vol, arcs, isAbs} = OS.Path.fromString path;
-        val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
-      in
-        if isAbs then
-          (case String.explode vol of
-            [d, #":"] =>
-              String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
-          | _ => path')
-        else path'
-      end
-  else fn path => path;
-
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/multithreading.ML
--- a/src/Pure/RAW/multithreading.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,196 +0,0 @@
-(*  Title:      Pure/RAW/multithreading.ML
-    Author:     Makarius
-
-Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
-*)
-
-signature BASIC_MULTITHREADING =
-sig
-  val interruptible: ('a -> 'b) -> 'a -> 'b
-  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-end;
-
-signature MULTITHREADING =
-sig
-  include BASIC_MULTITHREADING
-  val no_interrupts: Thread.threadAttribute list
-  val public_interrupts: Thread.threadAttribute list
-  val private_interrupts: Thread.threadAttribute list
-  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
-  val interrupted: unit -> unit  (*exception Interrupt*)
-  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
-  val max_threads_value: unit -> int
-  val max_threads_update: int -> unit
-  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
-  val enabled: unit -> bool
-  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
-    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
-  val trace: int ref
-  val tracing: int -> (unit -> string) -> unit
-  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
-  val real_time: ('a -> unit) -> 'a -> Time.time
-  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
-  val serial: unit -> int
-end;
-
-structure Multithreading: MULTITHREADING =
-struct
-
-(* thread attributes *)
-
-val no_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-
-val test_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
-
-val public_interrupts =
-  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val private_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val sync_interrupts = map
-  (fn x as Thread.InterruptState Thread.InterruptDefer => x
-    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
-    | x => x);
-
-val safe_interrupts = map
-  (fn Thread.InterruptState Thread.InterruptAsynch =>
-      Thread.InterruptState Thread.InterruptAsynchOnce
-    | x => x);
-
-fun interrupted () =
-  let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val _ = Thread.setAttributes test_interrupts;
-    val test = Exn.capture Thread.testInterrupt ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release test end;
-
-fun with_attributes new_atts e =
-  let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val result = Exn.capture (fn () =>
-      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release result end;
-
-
-(* portable wrappers *)
-
-fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
-
-fun uninterruptible f x =
-  with_attributes no_interrupts (fn atts =>
-    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
-
-(* options *)
-
-fun num_processors () =
-  (case Thread.numPhysicalProcessors () of
-    SOME n => n
-  | NONE => Thread.numProcessors ());
-
-fun max_threads_result m =
-  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
-
-val max_threads = ref 1;
-
-fun max_threads_value () = ! max_threads;
-
-fun max_threads_update m = max_threads := max_threads_result m;
-
-fun max_threads_setmp m f x =
-  uninterruptible (fn restore_attributes => fn () =>
-    let
-      val max_threads_orig = ! max_threads;
-      val _ = max_threads_update m;
-      val result = Exn.capture (restore_attributes f) x;
-      val _ = max_threads := max_threads_orig;
-    in Exn.release result end) ();
-
-fun enabled () = max_threads_value () > 1;
-
-
-(* synchronous wait *)
-
-fun sync_wait opt_atts time cond lock =
-  with_attributes
-    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
-    (fn _ =>
-      (case time of
-        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
-      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
-      handle exn => Exn.Exn exn);
-
-
-(* tracing *)
-
-val trace = ref 0;
-
-fun tracing level msg =
-  if level > ! trace then ()
-  else uninterruptible (fn _ => fn () =>
-    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
-      handle _ (*sic*) => ()) ();
-
-fun tracing_time detailed time =
-  tracing
-   (if not detailed then 5
-    else if Time.>= (time, seconds 1.0) then 1
-    else if Time.>= (time, seconds 0.1) then 2
-    else if Time.>= (time, seconds 0.01) then 3
-    else if Time.>= (time, seconds 0.001) then 4 else 5);
-
-fun real_time f x =
-  let
-    val timer = Timer.startRealTimer ();
-    val () = f x;
-    val time = Timer.checkRealTimer timer;
-  in time end;
-
-
-(* synchronized evaluation *)
-
-fun synchronized name lock e =
-  Exn.release (uninterruptible (fn restore_attributes => fn () =>
-    let
-      val immediate =
-        if Mutex.trylock lock then true
-        else
-          let
-            val _ = tracing 5 (fn () => name ^ ": locking ...");
-            val time = real_time Mutex.lock lock;
-            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
-          in false end;
-      val result = Exn.capture (restore_attributes e) ();
-      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
-      val _ = Mutex.unlock lock;
-    in result end) ());
-
-
-(* serial numbers *)
-
-local
-
-val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
-
-in
-
-val serial = uninterruptible (fn _ => fn () =>
-  let
-    val _ = Mutex.lock serial_lock;
-    val _ = serial_count := ! serial_count + 1;
-    val res = ! serial_count;
-    val _ = Mutex.unlock serial_lock;
-  in res end);
-
-end;
-
-end;
-
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/secure.ML
--- a/src/Pure/RAW/secure.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      Pure/RAW/secure.ML
-    Author:     Makarius
-
-Secure critical operations.
-*)
-
-signature SECURE =
-sig
-  val set_secure: unit -> unit
-  val is_secure: unit -> bool
-  val deny: string -> unit
-  val deny_ml: unit -> unit
-end;
-
-structure Secure: SECURE =
-struct
-
-val secure = Unsynchronized.ref false;
-
-fun set_secure () = secure := true;
-fun is_secure () = ! secure;
-
-fun deny msg = if is_secure () then error msg else ();
-
-fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
-
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/RAW/unsynchronized.ML
--- a/src/Pure/RAW/unsynchronized.ML	Thu Mar 03 21:35:16 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  Title:      Pure/RAW/unsynchronized.ML
-    Author:     Makarius
-
-Raw ML references as unsynchronized state variables.
-*)
-
-structure Unsynchronized =
-struct
-
-datatype ref = datatype ref;
-
-val op := = op :=;
-val ! = !;
-
-fun change r f = r := f (! r);
-fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
-
-fun inc i = (i := ! i + (1: int); ! i);
-fun dec i = (i := ! i - (1: int); ! i);
-
-fun setmp flag value f x =
-  uninterruptible (fn restore_attributes => fn () =>
-    let
-      val orig_value = ! flag;
-      val _ = flag := value;
-      val result = Exn.capture (restore_attributes f) x;
-      val _ = flag := orig_value;
-    in Exn.release result end) ();
-
-end;
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Mar 03 21:35:16 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 03 21:59:21 2016 +0100
@@ -1,39 +1,8 @@
 chapter Pure
 
-session RAW =
-  theories
-  files
-    "RAW/ROOT_polyml.ML"
-    "RAW/exn.ML"
-    "RAW/fixed_int_dummy.ML"
-    "RAW/ml_compiler0.ML"
-    "RAW/ml_debugger.ML"
-    "RAW/ml_heap.ML"
-    "RAW/ml_name_space.ML"
-    "RAW/ml_pretty.ML"
-    "RAW/ml_profiling.ML"
-    "RAW/ml_system.ML"
-    "RAW/multithreading.ML"
-    "RAW/secure.ML"
-    "RAW/unsynchronized.ML"
-
 session Pure =
   global_theories Pure
   files
-    "RAW/ROOT_polyml.ML"
-    "RAW/exn.ML"
-    "RAW/fixed_int_dummy.ML"
-    "RAW/ml_compiler0.ML"
-    "RAW/ml_debugger.ML"
-    "RAW/ml_heap.ML"
-    "RAW/ml_name_space.ML"
-    "RAW/ml_pretty.ML"
-    "RAW/ml_profiling.ML"
-    "RAW/ml_system.ML"
-    "RAW/multithreading.ML"
-    "RAW/secure.ML"
-    "RAW/unsynchronized.ML"
-
     "Concurrent/bash.ML"
     "Concurrent/bash_windows.ML"
     "Concurrent/cache.ML"
@@ -42,6 +11,7 @@
     "Concurrent/future.ML"
     "Concurrent/lazy.ML"
     "Concurrent/mailbox.ML"
+    "Concurrent/multithreading.ML"
     "Concurrent/par_exn.ML"
     "Concurrent/par_list.ML"
     "Concurrent/random.ML"
@@ -50,6 +20,7 @@
     "Concurrent/synchronized.ML"
     "Concurrent/task_queue.ML"
     "Concurrent/time_limit.ML"
+    "Concurrent/unsynchronized.ML"
     "General/alist.ML"
     "General/antiquote.ML"
     "General/balanced_tree.ML"
@@ -58,6 +29,7 @@
     "General/buffer.ML"
     "General/change_table.ML"
     "General/completion.ML"
+    "General/exn.ML"
     "General/file.ML"
     "General/graph.ML"
     "General/graph_display.ML"
@@ -77,6 +49,7 @@
     "General/queue.ML"
     "General/same.ML"
     "General/scan.ML"
+    "General/secure.ML"
     "General/seq.ML"
     "General/sha1.ML"
     "General/sha1_polyml.ML"
@@ -130,17 +103,25 @@
     "ML/exn_debugger.ML"
     "ML/exn_output.ML"
     "ML/exn_properties.ML"
+    "ML/fixed_int_dummy.ML"
     "ML/install_pp_polyml.ML"
     "ML/ml_antiquotation.ML"
     "ML/ml_compiler.ML"
+    "ML/ml_compiler0.ML"
     "ML/ml_context.ML"
+    "ML/ml_debugger.ML"
     "ML/ml_env.ML"
     "ML/ml_file.ML"
+    "ML/ml_heap.ML"
     "ML/ml_lex.ML"
+    "ML/ml_name_space.ML"
     "ML/ml_options.ML"
+    "ML/ml_pretty.ML"
+    "ML/ml_profiling.ML"
     "ML/ml_statistics.ML"
     "ML/ml_statistics_dummy.ML"
     "ML/ml_syntax.ML"
+    "ML/ml_system.ML"
     "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/command_span.ML"
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 03 21:35:16 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 03 21:59:21 2016 +0100
@@ -1,6 +1,14 @@
-(*** Isabelle/Pure bootstrap from "RAW" environment ***)
+(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
+
+(** bootstrap phase 0: Poly/ML setup **)
+
+(* initial ML name space *)
 
-(** bootstrap phase 0: towards ML within position context *)
+use "ML/ml_system.ML";
+use "ML/ml_name_space.ML";
+
+if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
+else use "ML/fixed_int_dummy.ML";
 
 structure Distribution =     (*filled-in by makedist*)
 struct
@@ -10,6 +18,87 @@
 end;
 
 
+(* multithreading *)
+
+use "General/exn.ML";
+
+val seconds = Time.fromReal;
+
+open Thread;
+use "Concurrent/multithreading.ML";
+
+use "Concurrent/unsynchronized.ML";
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
+
+
+(* pervasive environment *)
+
+val _ = PolyML.Compiler.forgetValue "isSome";
+val _ = PolyML.Compiler.forgetValue "getOpt";
+val _ = PolyML.Compiler.forgetValue "valOf";
+val _ = PolyML.Compiler.forgetValue "foldl";
+val _ = PolyML.Compiler.forgetValue "foldr";
+val _ = PolyML.Compiler.forgetValue "print";
+val _ = PolyML.Compiler.forgetValue "explode";
+val _ = PolyML.Compiler.forgetValue "concat";
+
+val ord = SML90.ord;
+val chr = SML90.chr;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+fun quit () = exit 0;
+
+
+(* ML runtime system *)
+
+use "ML/ml_heap.ML";
+use "ML/ml_profiling.ML";
+
+val pointer_eq = PolyML.pointerEq;
+
+
+(* ML toplevel pretty printing *)
+
+use "ML/ml_pretty.ML";
+
+local
+  val depth = Unsynchronized.ref 10;
+in
+  fun get_default_print_depth () = ! depth;
+  fun default_print_depth n = (depth := n; PolyML.print_depth n);
+  val _ = default_print_depth 10;
+end;
+
+val error_depth = PolyML.error_depth;
+
+
+(* ML compiler *)
+
+use "General/secure.ML";
+use "ML/ml_compiler0.ML";
+
+PolyML.Compiler.reportUnreferencedIds := true;
+PolyML.Compiler.reportExhaustiveHandlers := true;
+PolyML.Compiler.printInAlphabeticalOrder := false;
+PolyML.Compiler.maxInlineSize := 80;
+PolyML.Compiler.prompt1 := "ML> ";
+PolyML.Compiler.prompt2 := "ML# ";
+
+fun ml_make_string struct_name =
+  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
+    struct_name ^ ".ML_print_depth ()))))))";
+
+
+(* ML debugger *)
+
+use_no_debug "ML/ml_debugger.ML";
+
+
+
+(** bootstrap phase 1: towards ML within position context *)
+
 (* library of general tools *)
 
 use "General/basics.ML";
@@ -52,7 +141,7 @@
 
 
 
-(** bootstrap phase 1: towards ML within Isar context *)
+(** bootstrap phase 2: towards ML within Isar context *)
 
 (* library of general tools *)
 
@@ -236,7 +325,7 @@
 
 
 
-(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
+(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
 
 (*basic proof engine*)
 use "par_tactical.ML";
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 03 21:35:16 2016 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 03 21:59:21 2016 +0100
@@ -54,7 +54,7 @@
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }
 
-  def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
+  def is_pure(name: String): Boolean = name == "Pure"
 
   def session_info(options: Options, select: Boolean, dir: Path,
       chapter: String, entry: Session_Entry): (String, Session_Info) =
@@ -581,33 +581,13 @@
       """
       . "$ISABELLE_HOME/lib/scripts/timestart.bash"
       """ +
-      (if (is_pure(name)) {
-        val ml_system = Isabelle_System.getenv("ML_SYSTEM")
-        val ml_system_base = Library.space_explode('-', ml_system).headOption getOrElse ml_system
-        val ml_root =
-          List(ml_system, ml_system_base).map(a => "RAW/ROOT_" + a + ".ML").
-            find(b => Path.explode("~~/src/Pure/" + b).file.isFile) getOrElse
-            error("Missing compatibility file for ML system " + quote(ml_system))
-
-        if (name == "RAW") {
-          """
-            rm -f "$OUTPUT"
-            "$ISABELLE_PROCESS" \
-              -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
-              -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
-              -q RAW_ML_SYSTEM
-          """
-        }
-        else {
-          """
-            rm -f "$OUTPUT"
-            "$ISABELLE_PROCESS" \
-              -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
-              -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
-              -q RAW_ML_SYSTEM
-          """
-        }
-      }
+      (if (is_pure(name))
+        """
+          rm -f "$OUTPUT"
+          "$ISABELLE_PROCESS" -f "ROOT.ML" \
+            -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
+            -q RAW_ML_SYSTEM
+        """
       else
         """
         rm -f "$OUTPUT"
diff -r 15c36c181130 -r d0b68218ea55 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Mar 03 21:35:16 2016 +0100
+++ b/src/Pure/build-jars	Thu Mar 03 21:59:21 2016 +0100
@@ -28,6 +28,7 @@
   General/antiquote.scala
   General/bytes.scala
   General/completion.scala
+  General/exn.scala
   General/file.scala
   General/graph.scala
   General/graph_display.scala
@@ -71,7 +72,6 @@
   PIDE/text.scala
   PIDE/xml.scala
   PIDE/yxml.scala
-  RAW/exn.scala
   ROOT.scala
   System/command_line.scala
   System/cygwin.scala