clarified directory structure;
authorwenzelm
Wed Dec 23 23:09:13 2015 +0100 (2015-12-23)
changeset 61925ab52f183f020
parent 61924 55b3d21ab5e5
child 61926 17ba31a2303b
clarified directory structure;
src/Pure/General/exn.ML
src/Pure/General/exn.scala
src/Pure/ML-Systems/compiler_polyml.ML
src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
src/Pure/ML-Systems/ml_compiler_parameters.ML
src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML
src/Pure/ML-Systems/ml_debugger.ML
src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML
src/Pure/ML-Systems/ml_name_space.ML
src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML
src/Pure/ML-Systems/ml_name_space_polyml.ML
src/Pure/ML-Systems/ml_parse_tree.ML
src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML
src/Pure/ML-Systems/ml_positions.ML
src/Pure/ML-Systems/ml_pretty.ML
src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML
src/Pure/ML-Systems/ml_profiling_polyml.ML
src/Pure/ML-Systems/ml_stack_dummy.ML
src/Pure/ML-Systems/ml_stack_polyml-5.6.ML
src/Pure/ML-Systems/ml_system.ML
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/overloading_smlnj.ML
src/Pure/ML-Systems/polyml-5.5.2.ML
src/Pure/ML-Systems/polyml-5.6.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/pp_dummy.ML
src/Pure/ML-Systems/proper_int.ML
src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML
src/Pure/ML-Systems/single_assignment.ML
src/Pure/ML-Systems/single_assignment_polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/thread_dummy.ML
src/Pure/ML-Systems/universal.ML
src/Pure/ML-Systems/unsynchronized.ML
src/Pure/ML-Systems/use_context.ML
src/Pure/ML-Systems/windows_path.ML
src/Pure/RAW/compiler_polyml.ML
src/Pure/RAW/exn.ML
src/Pure/RAW/exn.scala
src/Pure/RAW/exn_trace_polyml-5.5.1.ML
src/Pure/RAW/ml_compiler_parameters.ML
src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
src/Pure/RAW/ml_debugger.ML
src/Pure/RAW/ml_debugger_polyml-5.6.ML
src/Pure/RAW/ml_name_space.ML
src/Pure/RAW/ml_name_space_polyml-5.6.ML
src/Pure/RAW/ml_name_space_polyml.ML
src/Pure/RAW/ml_parse_tree.ML
src/Pure/RAW/ml_parse_tree_polyml-5.6.ML
src/Pure/RAW/ml_positions.ML
src/Pure/RAW/ml_pretty.ML
src/Pure/RAW/ml_profiling_polyml-5.6.ML
src/Pure/RAW/ml_profiling_polyml.ML
src/Pure/RAW/ml_stack_dummy.ML
src/Pure/RAW/ml_stack_polyml-5.6.ML
src/Pure/RAW/ml_system.ML
src/Pure/RAW/multithreading.ML
src/Pure/RAW/multithreading_polyml.ML
src/Pure/RAW/overloading_smlnj.ML
src/Pure/RAW/polyml-5.5.2.ML
src/Pure/RAW/polyml-5.6.ML
src/Pure/RAW/polyml.ML
src/Pure/RAW/pp_dummy.ML
src/Pure/RAW/proper_int.ML
src/Pure/RAW/share_common_data_polyml-5.3.0.ML
src/Pure/RAW/single_assignment.ML
src/Pure/RAW/single_assignment_polyml.ML
src/Pure/RAW/smlnj.ML
src/Pure/RAW/thread_dummy.ML
src/Pure/RAW/universal.ML
src/Pure/RAW/unsynchronized.ML
src/Pure/RAW/use_context.ML
src/Pure/RAW/windows_path.ML
src/Pure/ROOT
src/Pure/build
src/Pure/build-jars
     1.1 --- a/src/Pure/General/exn.ML	Wed Dec 23 21:15:26 2015 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,92 +0,0 @@
     1.4 -(*  Title:      Pure/General/exn.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Support for exceptions.
     1.8 -*)
     1.9 -
    1.10 -signature EXN =
    1.11 -sig
    1.12 -  datatype 'a result = Res of 'a | Exn of exn
    1.13 -  val get_res: 'a result -> 'a option
    1.14 -  val get_exn: 'a result -> exn option
    1.15 -  val capture: ('a -> 'b) -> 'a -> 'b result
    1.16 -  val release: 'a result -> 'a
    1.17 -  val map_res: ('a -> 'b) -> 'a result -> 'b result
    1.18 -  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
    1.19 -  val map_exn: (exn -> exn) -> 'a result -> 'a result
    1.20 -  exception Interrupt
    1.21 -  val interrupt: unit -> 'a
    1.22 -  val is_interrupt: exn -> bool
    1.23 -  val interrupt_exn: 'a result
    1.24 -  val is_interrupt_exn: 'a result -> bool
    1.25 -  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
    1.26 -  val return_code: exn -> int -> int
    1.27 -  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
    1.28 -  exception EXCEPTIONS of exn list
    1.29 -end;
    1.30 -
    1.31 -structure Exn: EXN =
    1.32 -struct
    1.33 -
    1.34 -(* exceptions as values *)
    1.35 -
    1.36 -datatype 'a result =
    1.37 -  Res of 'a |
    1.38 -  Exn of exn;
    1.39 -
    1.40 -fun get_res (Res x) = SOME x
    1.41 -  | get_res _ = NONE;
    1.42 -
    1.43 -fun get_exn (Exn exn) = SOME exn
    1.44 -  | get_exn _ = NONE;
    1.45 -
    1.46 -fun capture f x = Res (f x) handle e => Exn e;
    1.47 -
    1.48 -fun release (Res y) = y
    1.49 -  | release (Exn e) = reraise e;
    1.50 -
    1.51 -fun map_res f (Res x) = Res (f x)
    1.52 -  | map_res f (Exn e) = Exn e;
    1.53 -
    1.54 -fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
    1.55 -
    1.56 -fun map_exn f (Res x) = Res x
    1.57 -  | map_exn f (Exn e) = Exn (f e);
    1.58 -
    1.59 -
    1.60 -(* interrupts *)
    1.61 -
    1.62 -exception Interrupt = Interrupt;
    1.63 -
    1.64 -fun interrupt () = raise Interrupt;
    1.65 -
    1.66 -fun is_interrupt Interrupt = true
    1.67 -  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
    1.68 -  | is_interrupt _ = false;
    1.69 -
    1.70 -val interrupt_exn = Exn Interrupt;
    1.71 -
    1.72 -fun is_interrupt_exn (Exn exn) = is_interrupt exn
    1.73 -  | is_interrupt_exn _ = false;
    1.74 -
    1.75 -fun interruptible_capture f x =
    1.76 -  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    1.77 -
    1.78 -
    1.79 -(* POSIX return code *)
    1.80 -
    1.81 -fun return_code exn rc =
    1.82 -  if is_interrupt exn then (130: int) else rc;
    1.83 -
    1.84 -fun capture_exit rc f x =
    1.85 -  f x handle exn => exit (return_code exn rc);
    1.86 -
    1.87 -
    1.88 -(* concatenated exceptions *)
    1.89 -
    1.90 -exception EXCEPTIONS of exn list;
    1.91 -
    1.92 -end;
    1.93 -
    1.94 -datatype illegal = Interrupt;
    1.95 -
     2.1 --- a/src/Pure/General/exn.scala	Wed Dec 23 21:15:26 2015 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,106 +0,0 @@
     2.4 -/*  Title:      Pure/General/exn.scala
     2.5 -    Module:     PIDE
     2.6 -    Author:     Makarius
     2.7 -
     2.8 -Support for exceptions (arbitrary throwables).
     2.9 -*/
    2.10 -
    2.11 -package isabelle
    2.12 -
    2.13 -
    2.14 -object Exn
    2.15 -{
    2.16 -  /* exceptions as values */
    2.17 -
    2.18 -  sealed abstract class Result[A]
    2.19 -  {
    2.20 -    def user_error: Result[A] =
    2.21 -      this match {
    2.22 -        case Exn(ERROR(msg)) => Exn(ERROR(msg))
    2.23 -        case _ => this
    2.24 -      }
    2.25 -  }
    2.26 -  case class Res[A](res: A) extends Result[A]
    2.27 -  case class Exn[A](exn: Throwable) extends Result[A]
    2.28 -
    2.29 -  def capture[A](e: => A): Result[A] =
    2.30 -    try { Res(e) }
    2.31 -    catch { case exn: Throwable => Exn[A](exn) }
    2.32 -
    2.33 -  def release[A](result: Result[A]): A =
    2.34 -    result match {
    2.35 -      case Res(x) => x
    2.36 -      case Exn(exn) => throw exn
    2.37 -    }
    2.38 -
    2.39 -  def release_first[A](results: List[Result[A]]): List[A] =
    2.40 -    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
    2.41 -      case Some(Exn(exn)) => throw exn
    2.42 -      case _ => results.map(release(_))
    2.43 -    }
    2.44 -
    2.45 -
    2.46 -  /* interrupts */
    2.47 -
    2.48 -  def is_interrupt(exn: Throwable): Boolean =
    2.49 -  {
    2.50 -    var found_interrupt = false
    2.51 -    var e = exn
    2.52 -    while (!found_interrupt && e != null) {
    2.53 -      found_interrupt |= e.isInstanceOf[InterruptedException]
    2.54 -      e = e.getCause
    2.55 -    }
    2.56 -    found_interrupt
    2.57 -  }
    2.58 -
    2.59 -  object Interrupt
    2.60 -  {
    2.61 -    def apply(): Throwable = new InterruptedException
    2.62 -    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
    2.63 -
    2.64 -    def expose() { if (Thread.interrupted) throw apply() }
    2.65 -    def impose() { Thread.currentThread.interrupt }
    2.66 -
    2.67 -    def postpone[A](body: => A): Option[A] =
    2.68 -    {
    2.69 -      val interrupted = Thread.interrupted
    2.70 -      val result = capture { body }
    2.71 -      if (interrupted) impose()
    2.72 -      result match {
    2.73 -        case Res(x) => Some(x)
    2.74 -        case Exn(e) =>
    2.75 -          if (is_interrupt(e)) { impose(); None }
    2.76 -          else throw e
    2.77 -      }
    2.78 -    }
    2.79 -
    2.80 -    val return_code = 130
    2.81 -  }
    2.82 -
    2.83 -
    2.84 -  /* POSIX return code */
    2.85 -
    2.86 -  def return_code(exn: Throwable, rc: Int): Int =
    2.87 -    if (is_interrupt(exn)) Interrupt.return_code else rc
    2.88 -
    2.89 -
    2.90 -  /* message */
    2.91 -
    2.92 -  def user_message(exn: Throwable): Option[String] =
    2.93 -    if (exn.getClass == classOf[RuntimeException] ||
    2.94 -        exn.getClass == classOf[Library.User_Error])
    2.95 -    {
    2.96 -      val msg = exn.getMessage
    2.97 -      Some(if (msg == null || msg == "") "Error" else msg)
    2.98 -    }
    2.99 -    else if (exn.isInstanceOf[java.io.IOException])
   2.100 -    {
   2.101 -      val msg = exn.getMessage
   2.102 -      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
   2.103 -    }
   2.104 -    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
   2.105 -    else None
   2.106 -
   2.107 -  def message(exn: Throwable): String =
   2.108 -    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
   2.109 -}
     3.1 --- a/src/Pure/ML-Systems/compiler_polyml.ML	Wed Dec 23 21:15:26 2015 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,59 +0,0 @@
     3.4 -(*  Title:      Pure/ML-Systems/compiler_polyml.ML
     3.5 -
     3.6 -Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
     3.7 -*)
     3.8 -
     3.9 -local
    3.10 -
    3.11 -fun drop_newline s =
    3.12 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    3.13 -  else s;
    3.14 -
    3.15 -in
    3.16 -
    3.17 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    3.18 -    {line, file, verbose, debug} text =
    3.19 -  let
    3.20 -    val current_line = Unsynchronized.ref line;
    3.21 -    val in_buffer =
    3.22 -      Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
    3.23 -    val out_buffer = Unsynchronized.ref ([]: string list);
    3.24 -    fun output () = drop_newline (implode (rev (! out_buffer)));
    3.25 -
    3.26 -    fun get () =
    3.27 -      (case ! in_buffer of
    3.28 -        [] => NONE
    3.29 -      | c :: cs =>
    3.30 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    3.31 -    fun put s = out_buffer := s :: ! out_buffer;
    3.32 -    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
    3.33 -     (put (if hard then "Error: " else "Warning: ");
    3.34 -      PolyML.prettyPrint (put, 76) msg1;
    3.35 -      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    3.36 -      put ("At" ^ str_of_pos message_line file ^ "\n"));
    3.37 -
    3.38 -    val parameters =
    3.39 -     [PolyML.Compiler.CPOutStream put,
    3.40 -      PolyML.Compiler.CPNameSpace name_space,
    3.41 -      PolyML.Compiler.CPErrorMessageProc put_message,
    3.42 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    3.43 -      PolyML.Compiler.CPFileName file,
    3.44 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
    3.45 -      ML_Compiler_Parameters.debug debug;
    3.46 -    val _ =
    3.47 -      (while not (List.null (! in_buffer)) do
    3.48 -        PolyML.compiler (get, parameters) ())
    3.49 -      handle exn =>
    3.50 -        if Exn.is_interrupt exn then reraise exn
    3.51 -        else
    3.52 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    3.53 -          error (output ()); reraise exn);
    3.54 -  in if verbose then print (output ()) else () end;
    3.55 -
    3.56 -fun use_file context {verbose, debug} file =
    3.57 -  let
    3.58 -    val instream = TextIO.openIn file;
    3.59 -    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    3.60 -  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    3.61 -
    3.62 -end;
     4.1 --- a/src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML	Wed Dec 23 21:15:26 2015 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,16 +0,0 @@
     4.4 -(*  Title:      Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Exception trace for Poly/ML 5.5.1 via ML output.
     4.8 -*)
     4.9 -
    4.10 -fun print_exception_trace exn_message output e =
    4.11 -  PolyML.Exception.traceException
    4.12 -    (e, fn (trace, exn) =>
    4.13 -      let
    4.14 -        val title = "Exception trace - " ^ exn_message exn;
    4.15 -        val _ = output (String.concatWith "\n" (title :: trace));
    4.16 -      in reraise exn end);
    4.17 -
    4.18 -PolyML.Compiler.reportExhaustiveHandlers := true;
    4.19 -
     5.1 --- a/src/Pure/ML-Systems/ml_compiler_parameters.ML	Wed Dec 23 21:15:26 2015 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,17 +0,0 @@
     5.4 -(*  Title:      Pure/ML/ml_compiler_parameters.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Additional ML compiler parameters for Poly/ML.
     5.8 -*)
     5.9 -
    5.10 -signature ML_COMPILER_PARAMETERS =
    5.11 -sig
    5.12 -  val debug: bool -> PolyML.Compiler.compilerParameters list
    5.13 -end;
    5.14 -
    5.15 -structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
    5.16 -struct
    5.17 -
    5.18 -fun debug _ = [];
    5.19 -
    5.20 -end;
    5.21 \ No newline at end of file
     6.1 --- a/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,12 +0,0 @@
     6.4 -(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.6.ML
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Additional ML compiler parameters for Poly/ML 5.6, or later.
     6.8 -*)
     6.9 -
    6.10 -structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
    6.11 -struct
    6.12 -
    6.13 -fun debug b = [PolyML.Compiler.CPDebug b];
    6.14 -
    6.15 -end;
    6.16 \ No newline at end of file
     7.1 --- a/src/Pure/ML-Systems/ml_debugger.ML	Wed Dec 23 21:15:26 2015 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,64 +0,0 @@
     7.4 -(*  Title:      Pure/ML/ml_debugger.ML
     7.5 -    Author:     Makarius
     7.6 -
     7.7 -ML debugger interface -- dummy version.
     7.8 -*)
     7.9 -
    7.10 -signature ML_DEBUGGER =
    7.11 -sig
    7.12 -  type exn_id
    7.13 -  val exn_id: exn -> exn_id
    7.14 -  val print_exn_id: exn_id -> string
    7.15 -  val eq_exn_id: exn_id * exn_id -> bool
    7.16 -  val on_entry: (string * 'location -> unit) option -> unit
    7.17 -  val on_exit: (string * 'location -> unit) option -> unit
    7.18 -  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
    7.19 -  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
    7.20 -  type state
    7.21 -  val state: Thread.thread -> state list
    7.22 -  val debug_function: state -> string
    7.23 -  val debug_function_arg: state -> ML_Name_Space.valueVal
    7.24 -  val debug_function_result: state -> ML_Name_Space.valueVal
    7.25 -  val debug_location: state -> 'location
    7.26 -  val debug_name_space: state -> ML_Name_Space.T
    7.27 -  val debug_local_name_space: state -> ML_Name_Space.T
    7.28 -end;
    7.29 -
    7.30 -structure ML_Debugger: ML_DEBUGGER =
    7.31 -struct
    7.32 -
    7.33 -(* exceptions *)
    7.34 -
    7.35 -abstype exn_id = Exn_Id of string
    7.36 -with
    7.37 -
    7.38 -fun exn_id exn = Exn_Id (General.exnName exn);
    7.39 -fun print_exn_id (Exn_Id name) = name;
    7.40 -fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
    7.41 -
    7.42 -end;
    7.43 -
    7.44 -
    7.45 -(* hooks *)
    7.46 -
    7.47 -fun on_entry _ = ();
    7.48 -fun on_exit _ = ();
    7.49 -fun on_exit_exception _ = ();
    7.50 -fun on_breakpoint _ = ();
    7.51 -
    7.52 -
    7.53 -(* debugger *)
    7.54 -
    7.55 -fun fail () = raise Fail "No debugger support on this ML platform";
    7.56 -
    7.57 -type state = unit;
    7.58 -
    7.59 -fun state _ = [];
    7.60 -fun debug_function () = fail ();
    7.61 -fun debug_function_arg () = fail ();
    7.62 -fun debug_function_result () = fail ();
    7.63 -fun debug_location () = fail ();
    7.64 -fun debug_name_space () = fail ();
    7.65 -fun debug_local_name_space () = fail ();
    7.66 -
    7.67 -end;
     8.1 --- a/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,72 +0,0 @@
     8.4 -(*  Title:      Pure/ML-Systems/ml_debugger_polyml-5.6.ML
     8.5 -    Author:     Makarius
     8.6 -
     8.7 -ML debugger interface -- for Poly/ML 5.6, or later.
     8.8 -*)
     8.9 -
    8.10 -signature ML_DEBUGGER =
    8.11 -sig
    8.12 -  type exn_id
    8.13 -  val exn_id: exn -> exn_id
    8.14 -  val print_exn_id: exn_id -> string
    8.15 -  val eq_exn_id: exn_id * exn_id -> bool
    8.16 -  type location
    8.17 -  val on_entry: (string * location -> unit) option -> unit
    8.18 -  val on_exit: (string * location -> unit) option -> unit
    8.19 -  val on_exit_exception: (string * location -> exn -> unit) option -> unit
    8.20 -  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
    8.21 -  type state
    8.22 -  val state: Thread.thread -> state list
    8.23 -  val debug_function: state -> string
    8.24 -  val debug_function_arg: state -> ML_Name_Space.valueVal
    8.25 -  val debug_function_result: state -> ML_Name_Space.valueVal
    8.26 -  val debug_location: state -> location
    8.27 -  val debug_name_space: state -> ML_Name_Space.T
    8.28 -  val debug_local_name_space: state -> ML_Name_Space.T
    8.29 -end;
    8.30 -
    8.31 -structure ML_Debugger: ML_DEBUGGER =
    8.32 -struct
    8.33 -
    8.34 -(* exceptions *)
    8.35 -
    8.36 -abstype exn_id = Exn_Id of string * int Unsynchronized.ref
    8.37 -with
    8.38 -
    8.39 -fun exn_id exn =
    8.40 -  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
    8.41 -
    8.42 -fun print_exn_id (Exn_Id (name, _)) = name;
    8.43 -fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
    8.44 -
    8.45 -end;
    8.46 -
    8.47 -val _ =
    8.48 -  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
    8.49 -    let val s = print_exn_id exn_id
    8.50 -    in ml_pretty (ML_Pretty.String (s, size s)) end);
    8.51 -
    8.52 -
    8.53 -(* hooks *)
    8.54 -
    8.55 -type location = PolyML.location;
    8.56 -
    8.57 -val on_entry = PolyML.DebuggerInterface.setOnEntry;
    8.58 -val on_exit = PolyML.DebuggerInterface.setOnExit;
    8.59 -val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
    8.60 -val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
    8.61 -
    8.62 -
    8.63 -(* debugger operations *)
    8.64 -
    8.65 -type state = PolyML.DebuggerInterface.debugState;
    8.66 -
    8.67 -val state = PolyML.DebuggerInterface.debugState;
    8.68 -val debug_function = PolyML.DebuggerInterface.debugFunction;
    8.69 -val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
    8.70 -val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
    8.71 -val debug_location = PolyML.DebuggerInterface.debugLocation;
    8.72 -val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
    8.73 -val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
    8.74 -
    8.75 -end;
     9.1 --- a/src/Pure/ML-Systems/ml_name_space.ML	Wed Dec 23 21:15:26 2015 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,68 +0,0 @@
     9.4 -(*  Title:      Pure/ML-Systems/ml_name_space.ML
     9.5 -    Author:     Makarius
     9.6 -
     9.7 -ML name space -- dummy version of Poly/ML 5.2 facility.
     9.8 -*)
     9.9 -
    9.10 -structure ML_Name_Space =
    9.11 -struct
    9.12 -
    9.13 -type valueVal = unit;
    9.14 -type typeVal = unit;
    9.15 -type fixityVal = unit;
    9.16 -type structureVal = unit;
    9.17 -type signatureVal = unit;
    9.18 -type functorVal = unit;
    9.19 -
    9.20 -type T =
    9.21 - {lookupVal:    string -> valueVal option,
    9.22 -  lookupType:   string -> typeVal option,
    9.23 -  lookupFix:    string -> fixityVal option,
    9.24 -  lookupStruct: string -> structureVal option,
    9.25 -  lookupSig:    string -> signatureVal option,
    9.26 -  lookupFunct:  string -> functorVal option,
    9.27 -  enterVal:     string * valueVal -> unit,
    9.28 -  enterType:    string * typeVal -> unit,
    9.29 -  enterFix:     string * fixityVal -> unit,
    9.30 -  enterStruct:  string * structureVal -> unit,
    9.31 -  enterSig:     string * signatureVal -> unit,
    9.32 -  enterFunct:   string * functorVal -> unit,
    9.33 -  allVal:       unit -> (string * valueVal) list,
    9.34 -  allType:      unit -> (string * typeVal) list,
    9.35 -  allFix:       unit -> (string * fixityVal) list,
    9.36 -  allStruct:    unit -> (string * structureVal) list,
    9.37 -  allSig:       unit -> (string * signatureVal) list,
    9.38 -  allFunct:     unit -> (string * functorVal) list};
    9.39 -
    9.40 -val global: T =
    9.41 - {lookupVal = fn _ => NONE,
    9.42 -  lookupType = fn _ => NONE,
    9.43 -  lookupFix = fn _ => NONE,
    9.44 -  lookupStruct = fn _ => NONE,
    9.45 -  lookupSig = fn _ => NONE,
    9.46 -  lookupFunct = fn _ => NONE,
    9.47 -  enterVal = fn _ => (),
    9.48 -  enterType = fn _ => (),
    9.49 -  enterFix = fn _ => (),
    9.50 -  enterStruct = fn _ => (),
    9.51 -  enterSig = fn _ => (),
    9.52 -  enterFunct = fn _ => (),
    9.53 -  allVal = fn _ => [],
    9.54 -  allType = fn _ => [],
    9.55 -  allFix = fn _ => [],
    9.56 -  allStruct = fn _ => [],
    9.57 -  allSig = fn _ => [],
    9.58 -  allFunct = fn _ => []};
    9.59 -
    9.60 -val initial_val : (string * valueVal) list = [];
    9.61 -val initial_type : (string * typeVal) list = [];
    9.62 -val initial_fixity : (string * fixityVal) list = [];
    9.63 -val initial_structure : (string * structureVal) list = [];
    9.64 -val initial_signature : (string * signatureVal) list = [];
    9.65 -val initial_functor : (string * functorVal) list = [];
    9.66 -
    9.67 -fun forget_global_structure (_: string) = ();
    9.68 -
    9.69 -fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
    9.70 -
    9.71 -end;
    10.1 --- a/src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,33 +0,0 @@
    10.4 -(*  Title:      Pure/ML-Systems/ml_name_space_polyml-5.6.ML
    10.5 -    Author:     Makarius
    10.6 -
    10.7 -Name space for Poly/ML.
    10.8 -*)
    10.9 -
   10.10 -structure ML_Name_Space =
   10.11 -struct
   10.12 -  open PolyML.NameSpace;
   10.13 -
   10.14 -  type T = PolyML.NameSpace.nameSpace;
   10.15 -  val global = PolyML.globalNameSpace;
   10.16 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
   10.17 -
   10.18 -  type valueVal = Values.value;
   10.19 -  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   10.20 -  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
   10.21 -
   10.22 -  type typeVal = TypeConstrs.typeConstr;
   10.23 -  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   10.24 -
   10.25 -  type fixityVal = Infixes.fixity;
   10.26 -  fun displayFix (_: string, x) = Infixes.print x;
   10.27 -
   10.28 -  type structureVal = Structures.structureVal;
   10.29 -  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   10.30 -
   10.31 -  type signatureVal = Signatures.signatureVal;
   10.32 -  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
   10.33 -
   10.34 -  type functorVal = Functors.functorVal;
   10.35 -  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
   10.36 -end;
    11.1 --- a/src/Pure/ML-Systems/ml_name_space_polyml.ML	Wed Dec 23 21:15:26 2015 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,13 +0,0 @@
    11.4 -(*  Title:      Pure/ML-Systems/ml_name_space_polyml.ML
    11.5 -    Author:     Makarius
    11.6 -
    11.7 -Name space for Poly/ML.
    11.8 -*)
    11.9 -
   11.10 -structure ML_Name_Space =
   11.11 -struct
   11.12 -  open PolyML.NameSpace;
   11.13 -  type T = nameSpace;
   11.14 -  val global = PolyML.globalNameSpace;
   11.15 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
   11.16 -end;
    12.1 --- a/src/Pure/ML-Systems/ml_parse_tree.ML	Wed Dec 23 21:15:26 2015 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,19 +0,0 @@
    12.4 -(*  Title:      Pure/ML/ml_parse_tree.ML
    12.5 -    Author:     Makarius
    12.6 -
    12.7 -Additional ML parse tree components for Poly/ML.
    12.8 -*)
    12.9 -
   12.10 -signature ML_PARSE_TREE =
   12.11 -sig
   12.12 -  val completions: PolyML.ptProperties -> string list option
   12.13 -  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
   12.14 -end;
   12.15 -
   12.16 -structure ML_Parse_Tree: ML_PARSE_TREE =
   12.17 -struct
   12.18 -
   12.19 -fun completions _ = NONE;
   12.20 -fun breakpoint _ = NONE;
   12.21 -
   12.22 -end;
   12.23 \ No newline at end of file
    13.1 --- a/src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,16 +0,0 @@
    13.4 -(*  Title:      Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML
    13.5 -    Author:     Makarius
    13.6 -
    13.7 -Additional ML parse tree components for Poly/ML 5.6, or later.
    13.8 -*)
    13.9 -
   13.10 -structure ML_Parse_Tree: ML_PARSE_TREE =
   13.11 -struct
   13.12 -
   13.13 -fun completions (PolyML.PTcompletions x) = SOME x
   13.14 -  | completions _ = NONE;
   13.15 -
   13.16 -fun breakpoint (PolyML.PTbreakPoint x) = SOME x
   13.17 -  | breakpoint _ = NONE;
   13.18 -
   13.19 -end;
   13.20 \ No newline at end of file
    14.1 --- a/src/Pure/ML-Systems/ml_positions.ML	Wed Dec 23 21:15:26 2015 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,16 +0,0 @@
    14.4 -(*  Title:      Pure/ML-Systems/ml_positions.ML
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
    14.8 -*)
    14.9 -
   14.10 -fun ml_positions start_line name txt =
   14.11 -  let
   14.12 -    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
   14.13 -          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
   14.14 -          in positions line cs (s :: res) end
   14.15 -      | positions line (c :: cs) res =
   14.16 -          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
   14.17 -      | positions _ [] res = rev res;
   14.18 -  in String.concat (positions start_line (String.explode txt) []) end;
   14.19 -
    15.1 --- a/src/Pure/ML-Systems/ml_pretty.ML	Wed Dec 23 21:15:26 2015 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,30 +0,0 @@
    15.4 -(*  Title:      Pure/ML-Systems/ml_pretty.ML
    15.5 -    Author:     Makarius
    15.6 -
    15.7 -Minimal support for raw ML pretty printing -- for boot-strapping only.
    15.8 -*)
    15.9 -
   15.10 -structure ML_Pretty =
   15.11 -struct
   15.12 -
   15.13 -datatype pretty =
   15.14 -  Block of (string * string) * bool * int * pretty list |
   15.15 -  String of string * int |
   15.16 -  Break of bool * int * int;
   15.17 -
   15.18 -fun block prts = Block (("", ""), false, 2, prts);
   15.19 -fun str s = String (s, size s);
   15.20 -fun brk width = Break (false, width, 0);
   15.21 -
   15.22 -fun pair pretty1 pretty2 ((x, y), depth: int) =
   15.23 -  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
   15.24 -
   15.25 -fun enum sep lpar rpar pretty (args, depth) =
   15.26 -  let
   15.27 -    fun elems _ [] = []
   15.28 -      | elems 0 _ = [str "..."]
   15.29 -      | elems d [x] = [pretty (x, d)]
   15.30 -      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
   15.31 -  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
   15.32 -
   15.33 -end;
    16.1 --- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,19 +0,0 @@
    16.4 -(*  Title:      Pure/ML-Systems/ml_profiling_polyml-5.6.ML
    16.5 -    Author:     Makarius
    16.6 -
    16.7 -Profiling for Poly/ML 5.6.
    16.8 -*)
    16.9 -
   16.10 -structure ML_Profiling =
   16.11 -struct
   16.12 -
   16.13 -fun profile_time pr f x =
   16.14 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   16.15 -
   16.16 -fun profile_time_thread pr f x =
   16.17 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   16.18 -
   16.19 -fun profile_allocations pr f x =
   16.20 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   16.21 -
   16.22 -end;
    17.1 --- a/src/Pure/ML-Systems/ml_profiling_polyml.ML	Wed Dec 23 21:15:26 2015 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,27 +0,0 @@
    17.4 -(*  Title:      Pure/ML-Systems/ml_profiling_polyml.ML
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Profiling for Poly/ML.
    17.8 -*)
    17.9 -
   17.10 -structure ML_Profiling =
   17.11 -struct
   17.12 -
   17.13 -local
   17.14 -
   17.15 -fun profile n f x =
   17.16 -  let
   17.17 -    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   17.18 -    val res = Exn.capture f x;
   17.19 -    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   17.20 -  in Exn.release res end;
   17.21 -
   17.22 -in
   17.23 -
   17.24 -fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
   17.25 -fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
   17.26 -fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
   17.27 -
   17.28 -end;
   17.29 -
   17.30 -end;
    18.1 --- a/src/Pure/ML-Systems/ml_stack_dummy.ML	Wed Dec 23 21:15:26 2015 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,16 +0,0 @@
    18.4 -(*  Title:      Pure/ML-Systems/ml_stack_dummy.ML
    18.5 -
    18.6 -Maximum stack size (in words) for ML threads -- dummy version.
    18.7 -*)
    18.8 -
    18.9 -signature ML_STACK =
   18.10 -sig
   18.11 -  val limit: int option -> Thread.threadAttribute list
   18.12 -end;
   18.13 -
   18.14 -structure ML_Stack: ML_STACK =
   18.15 -struct
   18.16 -
   18.17 -fun limit (_: int option) : Thread.threadAttribute list = [];
   18.18 -
   18.19 -end;
    19.1 --- a/src/Pure/ML-Systems/ml_stack_polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,16 +0,0 @@
    19.4 -(*  Title:      Pure/ML-Systems/ml_stack_polyml-5.6.ML
    19.5 -
    19.6 -Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
    19.7 -*)
    19.8 -
    19.9 -signature ML_STACK =
   19.10 -sig
   19.11 -  val limit: int option -> Thread.threadAttribute list
   19.12 -end;
   19.13 -
   19.14 -structure ML_Stack: ML_STACK =
   19.15 -struct
   19.16 -
   19.17 -fun limit m = [Thread.MaximumMLStack m];
   19.18 -
   19.19 -end;
    20.1 --- a/src/Pure/ML-Systems/ml_system.ML	Wed Dec 23 21:15:26 2015 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,32 +0,0 @@
    20.4 -(*  Title:      Pure/ML-Systems/ml_system.ML
    20.5 -    Author:     Makarius
    20.6 -
    20.7 -ML system and platform operations.
    20.8 -*)
    20.9 -
   20.10 -signature ML_SYSTEM =
   20.11 -sig
   20.12 -  val name: string
   20.13 -  val is_polyml: bool
   20.14 -  val is_smlnj: bool
   20.15 -  val platform: string
   20.16 -  val platform_is_windows: bool
   20.17 -  val share_common_data: unit -> unit
   20.18 -  val save_state: string -> unit
   20.19 -end;
   20.20 -
   20.21 -structure ML_System: ML_SYSTEM =
   20.22 -struct
   20.23 -
   20.24 -val SOME name = OS.Process.getEnv "ML_SYSTEM";
   20.25 -val is_polyml = String.isPrefix "polyml" name;
   20.26 -val is_smlnj = String.isPrefix "smlnj" name;
   20.27 -
   20.28 -val SOME platform = OS.Process.getEnv "ML_PLATFORM";
   20.29 -val platform_is_windows = String.isSuffix "windows" platform;
   20.30 -
   20.31 -fun share_common_data () = ();
   20.32 -fun save_state _ = raise Fail "Cannot save state -- undefined operation";
   20.33 -
   20.34 -end;
   20.35 -
    21.1 --- a/src/Pure/ML-Systems/multithreading.ML	Wed Dec 23 21:15:26 2015 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,75 +0,0 @@
    21.4 -(*  Title:      Pure/ML-Systems/multithreading.ML
    21.5 -    Author:     Makarius
    21.6 -
    21.7 -Dummy implementation of multithreading setup.
    21.8 -*)
    21.9 -
   21.10 -signature MULTITHREADING =
   21.11 -sig
   21.12 -  val available: bool
   21.13 -  val max_threads_value: unit -> int
   21.14 -  val max_threads_update: int -> unit
   21.15 -  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
   21.16 -  val enabled: unit -> bool
   21.17 -  val no_interrupts: Thread.threadAttribute list
   21.18 -  val public_interrupts: Thread.threadAttribute list
   21.19 -  val private_interrupts: Thread.threadAttribute list
   21.20 -  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
   21.21 -  val interrupted: unit -> unit  (*exception Interrupt*)
   21.22 -  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   21.23 -  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
   21.24 -    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   21.25 -  val trace: int ref
   21.26 -  val tracing: int -> (unit -> string) -> unit
   21.27 -  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   21.28 -  val real_time: ('a -> unit) -> 'a -> Time.time
   21.29 -  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
   21.30 -  val serial: unit -> int
   21.31 -end;
   21.32 -
   21.33 -structure Multithreading: MULTITHREADING =
   21.34 -struct
   21.35 -
   21.36 -(* options *)
   21.37 -
   21.38 -val available = false;
   21.39 -fun max_threads_value () = 1: int;
   21.40 -fun max_threads_update _ = ();
   21.41 -fun max_threads_setmp _ f x = f x;
   21.42 -fun enabled () = false;
   21.43 -
   21.44 -
   21.45 -(* attributes *)
   21.46 -
   21.47 -val no_interrupts = [];
   21.48 -val public_interrupts = [];
   21.49 -val private_interrupts = [];
   21.50 -fun sync_interrupts _ = [];
   21.51 -
   21.52 -fun interrupted () = ();
   21.53 -
   21.54 -fun with_attributes _ e = e [];
   21.55 -
   21.56 -fun sync_wait _ _ _ _ = Exn.Res true;
   21.57 -
   21.58 -
   21.59 -(* tracing *)
   21.60 -
   21.61 -val trace = ref (0: int);
   21.62 -fun tracing _ _ = ();
   21.63 -fun tracing_time _ _ _ = ();
   21.64 -fun real_time f x = (f x; Time.zeroTime);
   21.65 -
   21.66 -
   21.67 -(* synchronized evaluation *)
   21.68 -
   21.69 -fun synchronized _ _ e = e ();
   21.70 -
   21.71 -
   21.72 -(* serial numbers *)
   21.73 -
   21.74 -local val count = ref (0: int)
   21.75 -in fun serial () = (count := ! count + 1; ! count) end;
   21.76 -
   21.77 -end;
   21.78 -
    22.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Dec 23 21:15:26 2015 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,172 +0,0 @@
    22.4 -(*  Title:      Pure/ML-Systems/multithreading_polyml.ML
    22.5 -    Author:     Makarius
    22.6 -
    22.7 -Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
    22.8 -*)
    22.9 -
   22.10 -signature MULTITHREADING =
   22.11 -sig
   22.12 -  include MULTITHREADING
   22.13 -  val interruptible: ('a -> 'b) -> 'a -> 'b
   22.14 -  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   22.15 -end;
   22.16 -
   22.17 -structure Multithreading: MULTITHREADING =
   22.18 -struct
   22.19 -
   22.20 -(* thread attributes *)
   22.21 -
   22.22 -val no_interrupts =
   22.23 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
   22.24 -
   22.25 -val test_interrupts =
   22.26 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
   22.27 -
   22.28 -val public_interrupts =
   22.29 -  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
   22.30 -
   22.31 -val private_interrupts =
   22.32 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
   22.33 -
   22.34 -val sync_interrupts = map
   22.35 -  (fn x as Thread.InterruptState Thread.InterruptDefer => x
   22.36 -    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
   22.37 -    | x => x);
   22.38 -
   22.39 -val safe_interrupts = map
   22.40 -  (fn Thread.InterruptState Thread.InterruptAsynch =>
   22.41 -      Thread.InterruptState Thread.InterruptAsynchOnce
   22.42 -    | x => x);
   22.43 -
   22.44 -fun interrupted () =
   22.45 -  let
   22.46 -    val orig_atts = safe_interrupts (Thread.getAttributes ());
   22.47 -    val _ = Thread.setAttributes test_interrupts;
   22.48 -    val test = Exn.capture Thread.testInterrupt ();
   22.49 -    val _ = Thread.setAttributes orig_atts;
   22.50 -  in Exn.release test end;
   22.51 -
   22.52 -fun with_attributes new_atts e =
   22.53 -  let
   22.54 -    val orig_atts = safe_interrupts (Thread.getAttributes ());
   22.55 -    val result = Exn.capture (fn () =>
   22.56 -      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
   22.57 -    val _ = Thread.setAttributes orig_atts;
   22.58 -  in Exn.release result end;
   22.59 -
   22.60 -
   22.61 -(* portable wrappers *)
   22.62 -
   22.63 -fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
   22.64 -
   22.65 -fun uninterruptible f x =
   22.66 -  with_attributes no_interrupts (fn atts =>
   22.67 -    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
   22.68 -
   22.69 -
   22.70 -(* options *)
   22.71 -
   22.72 -val available = true;
   22.73 -
   22.74 -fun max_threads_result m =
   22.75 -  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
   22.76 -
   22.77 -val max_threads = ref 1;
   22.78 -
   22.79 -fun max_threads_value () = ! max_threads;
   22.80 -
   22.81 -fun max_threads_update m = max_threads := max_threads_result m;
   22.82 -
   22.83 -fun max_threads_setmp m f x =
   22.84 -  uninterruptible (fn restore_attributes => fn () =>
   22.85 -    let
   22.86 -      val max_threads_orig = ! max_threads;
   22.87 -      val _ = max_threads_update m;
   22.88 -      val result = Exn.capture (restore_attributes f) x;
   22.89 -      val _ = max_threads := max_threads_orig;
   22.90 -    in Exn.release result end) ();
   22.91 -
   22.92 -fun enabled () = max_threads_value () > 1;
   22.93 -
   22.94 -
   22.95 -(* synchronous wait *)
   22.96 -
   22.97 -fun sync_wait opt_atts time cond lock =
   22.98 -  with_attributes
   22.99 -    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
  22.100 -    (fn _ =>
  22.101 -      (case time of
  22.102 -        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
  22.103 -      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
  22.104 -      handle exn => Exn.Exn exn);
  22.105 -
  22.106 -
  22.107 -(* tracing *)
  22.108 -
  22.109 -val trace = ref 0;
  22.110 -
  22.111 -fun tracing level msg =
  22.112 -  if level > ! trace then ()
  22.113 -  else uninterruptible (fn _ => fn () =>
  22.114 -    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
  22.115 -      handle _ (*sic*) => ()) ();
  22.116 -
  22.117 -fun tracing_time detailed time =
  22.118 -  tracing
  22.119 -   (if not detailed then 5
  22.120 -    else if Time.>= (time, seconds 1.0) then 1
  22.121 -    else if Time.>= (time, seconds 0.1) then 2
  22.122 -    else if Time.>= (time, seconds 0.01) then 3
  22.123 -    else if Time.>= (time, seconds 0.001) then 4 else 5);
  22.124 -
  22.125 -fun real_time f x =
  22.126 -  let
  22.127 -    val timer = Timer.startRealTimer ();
  22.128 -    val () = f x;
  22.129 -    val time = Timer.checkRealTimer timer;
  22.130 -  in time end;
  22.131 -
  22.132 -
  22.133 -(* synchronized evaluation *)
  22.134 -
  22.135 -fun synchronized name lock e =
  22.136 -  Exn.release (uninterruptible (fn restore_attributes => fn () =>
  22.137 -    let
  22.138 -      val immediate =
  22.139 -        if Mutex.trylock lock then true
  22.140 -        else
  22.141 -          let
  22.142 -            val _ = tracing 5 (fn () => name ^ ": locking ...");
  22.143 -            val time = real_time Mutex.lock lock;
  22.144 -            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
  22.145 -          in false end;
  22.146 -      val result = Exn.capture (restore_attributes e) ();
  22.147 -      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
  22.148 -      val _ = Mutex.unlock lock;
  22.149 -    in result end) ());
  22.150 -
  22.151 -
  22.152 -(* serial numbers *)
  22.153 -
  22.154 -local
  22.155 -
  22.156 -val serial_lock = Mutex.mutex ();
  22.157 -val serial_count = ref 0;
  22.158 -
  22.159 -in
  22.160 -
  22.161 -val serial = uninterruptible (fn _ => fn () =>
  22.162 -  let
  22.163 -    val _ = Mutex.lock serial_lock;
  22.164 -    val _ = serial_count := ! serial_count + 1;
  22.165 -    val res = ! serial_count;
  22.166 -    val _ = Mutex.unlock serial_lock;
  22.167 -  in res end);
  22.168 -
  22.169 -end;
  22.170 -
  22.171 -end;
  22.172 -
  22.173 -val interruptible = Multithreading.interruptible;
  22.174 -val uninterruptible = Multithreading.uninterruptible;
  22.175 -
    23.1 --- a/src/Pure/ML-Systems/overloading_smlnj.ML	Wed Dec 23 21:15:26 2015 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,41 +0,0 @@
    23.4 -(*  Title:      Pure/ML-Systems/overloading_smlnj.ML
    23.5 -    Author:     Makarius
    23.6 -
    23.7 -Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
    23.8 -*)
    23.9 -
   23.10 -Control.overloadKW := true;
   23.11 -
   23.12 -overload ~ : ('a -> 'a) as
   23.13 -  IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
   23.14 -  Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
   23.15 -overload + : ('a * 'a -> 'a) as
   23.16 -  IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
   23.17 -  Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
   23.18 -overload - : ('a * 'a -> 'a) as
   23.19 -  IntInf.- and Int31.- and Int32.- and Int64.- and
   23.20 -  Word.- and Word8.- and Word32.- and Word64.- and Real.-;
   23.21 -overload * : ('a * 'a -> 'a) as
   23.22 -  IntInf.* and Int31.* and Int32.* and Int64.* and
   23.23 -  Word.* and Word8.* and Word32.* and Word64.* and Real.*;
   23.24 -overload div: ('a * 'a -> 'a) as
   23.25 -  IntInf.div and Int31.div and Int32.div and Int64.div and
   23.26 -  Word.div and Word8.div and Word32.div and Word64.div;
   23.27 -overload mod: ('a * 'a -> 'a) as
   23.28 -  IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
   23.29 -  Word.mod and Word8.mod and Word32.mod and Word64.mod;
   23.30 -overload < : ('a * 'a -> bool) as
   23.31 -  IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
   23.32 -  Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
   23.33 -overload <= : ('a * 'a -> bool) as
   23.34 -  IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
   23.35 -  Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
   23.36 -overload > : ('a * 'a -> bool) as
   23.37 -  IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
   23.38 -  Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
   23.39 -overload >= : ('a * 'a -> bool) as
   23.40 -  IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
   23.41 -  Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
   23.42 -overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
   23.43 -
   23.44 -Control.overloadKW := false;
    24.1 --- a/src/Pure/ML-Systems/polyml-5.5.2.ML	Wed Dec 23 21:15:26 2015 +0100
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,23 +0,0 @@
    24.4 -(*  Title:      Pure/ML-Systems/polyml-5.5.2.ML
    24.5 -    Author:     Makarius
    24.6 -
    24.7 -Compatibility wrapper for Poly/ML 5.5.2.
    24.8 -*)
    24.9 -
   24.10 -structure Thread =
   24.11 -struct
   24.12 -  open Thread;
   24.13 -
   24.14 -  structure Thread =
   24.15 -  struct
   24.16 -    open Thread;
   24.17 -
   24.18 -    fun numProcessors () =
   24.19 -      (case Thread.numPhysicalProcessors () of
   24.20 -        SOME n => n
   24.21 -      | NONE => Thread.numProcessors ());
   24.22 -  end;
   24.23 -end;
   24.24 -
   24.25 -use "ML-Systems/polyml.ML";
   24.26 -
    25.1 --- a/src/Pure/ML-Systems/polyml-5.6.ML	Wed Dec 23 21:15:26 2015 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,22 +0,0 @@
    25.4 -(*  Title:      Pure/ML-Systems/polyml-5.6.ML
    25.5 -    Author:     Makarius
    25.6 -
    25.7 -Compatibility wrapper for Poly/ML 5.6.
    25.8 -*)
    25.9 -
   25.10 -structure Thread =
   25.11 -struct
   25.12 -  open Thread;
   25.13 -
   25.14 -  structure Thread =
   25.15 -  struct
   25.16 -    open Thread;
   25.17 -
   25.18 -    fun numProcessors () =
   25.19 -      (case Thread.numPhysicalProcessors () of
   25.20 -        SOME n => n
   25.21 -      | NONE => Thread.numProcessors ());
   25.22 -  end;
   25.23 -end;
   25.24 -
   25.25 -use "ML-Systems/polyml.ML";
    26.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Dec 23 21:15:26 2015 +0100
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,207 +0,0 @@
    26.4 -(*  Title:      Pure/ML-Systems/polyml.ML
    26.5 -    Author:     Makarius
    26.6 -
    26.7 -Compatibility wrapper for Poly/ML.
    26.8 -*)
    26.9 -
   26.10 -(* initial ML name space *)
   26.11 -
   26.12 -use "ML-Systems/ml_system.ML";
   26.13 -
   26.14 -if ML_System.name = "polyml-5.6"
   26.15 -then use "ML-Systems/ml_name_space_polyml-5.6.ML"
   26.16 -else use "ML-Systems/ml_name_space_polyml.ML";
   26.17 -
   26.18 -structure ML_Name_Space =
   26.19 -struct
   26.20 -  open ML_Name_Space;
   26.21 -  val initial_val =
   26.22 -    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
   26.23 -      (#allVal global ());
   26.24 -  val initial_type = #allType global ();
   26.25 -  val initial_fixity = #allFix global ();
   26.26 -  val initial_structure = #allStruct global ();
   26.27 -  val initial_signature = #allSig global ();
   26.28 -  val initial_functor = #allFunct global ();
   26.29 -end;
   26.30 -
   26.31 -
   26.32 -(* ML system operations *)
   26.33 -
   26.34 -if ML_System.name = "polyml-5.3.0"
   26.35 -then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
   26.36 -else ();
   26.37 -
   26.38 -fun ml_platform_path (s: string) = s;
   26.39 -fun ml_standard_path (s: string) = s;
   26.40 -
   26.41 -if ML_System.platform_is_windows then use "ML-Systems/windows_path.ML" else ();
   26.42 -
   26.43 -structure ML_System =
   26.44 -struct
   26.45 -  open ML_System;
   26.46 -  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   26.47 -  val save_state = PolyML.SaveState.saveState o ml_platform_path;
   26.48 -end;
   26.49 -
   26.50 -
   26.51 -(* exceptions *)
   26.52 -
   26.53 -fun reraise exn =
   26.54 -  (case PolyML.exceptionLocation exn of
   26.55 -    NONE => raise exn
   26.56 -  | SOME location => PolyML.raiseWithLocation (exn, location));
   26.57 -
   26.58 -exception Interrupt = SML90.Interrupt;
   26.59 -
   26.60 -use "General/exn.ML";
   26.61 -
   26.62 -fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
   26.63 -
   26.64 -if ML_System.name = "polyml-5.5.1"
   26.65 -  orelse ML_System.name = "polyml-5.5.2"
   26.66 -  orelse ML_System.name = "polyml-5.6"
   26.67 -then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
   26.68 -else ();
   26.69 -
   26.70 -
   26.71 -(* multithreading *)
   26.72 -
   26.73 -val seconds = Time.fromReal;
   26.74 -
   26.75 -if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
   26.76 -then ()
   26.77 -else use "ML-Systems/single_assignment_polyml.ML";
   26.78 -
   26.79 -open Thread;
   26.80 -use "ML-Systems/multithreading.ML";
   26.81 -use "ML-Systems/multithreading_polyml.ML";
   26.82 -
   26.83 -if ML_System.name = "polyml-5.6"
   26.84 -then use "ML-Systems/ml_stack_polyml-5.6.ML"
   26.85 -else use "ML-Systems/ml_stack_dummy.ML";
   26.86 -
   26.87 -use "ML-Systems/unsynchronized.ML";
   26.88 -val _ = PolyML.Compiler.forgetValue "ref";
   26.89 -val _ = PolyML.Compiler.forgetType "ref";
   26.90 -
   26.91 -
   26.92 -(* pervasive environment *)
   26.93 -
   26.94 -val _ = PolyML.Compiler.forgetValue "isSome";
   26.95 -val _ = PolyML.Compiler.forgetValue "getOpt";
   26.96 -val _ = PolyML.Compiler.forgetValue "valOf";
   26.97 -val _ = PolyML.Compiler.forgetValue "foldl";
   26.98 -val _ = PolyML.Compiler.forgetValue "foldr";
   26.99 -val _ = PolyML.Compiler.forgetValue "print";
  26.100 -val _ = PolyML.Compiler.forgetValue "explode";
  26.101 -val _ = PolyML.Compiler.forgetValue "concat";
  26.102 -
  26.103 -val ord = SML90.ord;
  26.104 -val chr = SML90.chr;
  26.105 -val raw_explode = SML90.explode;
  26.106 -val implode = SML90.implode;
  26.107 -
  26.108 -val io_buffer_size = 4096;
  26.109 -
  26.110 -fun quit () = exit 0;
  26.111 -
  26.112 -
  26.113 -(* ML runtime system *)
  26.114 -
  26.115 -if ML_System.name = "polyml-5.6"
  26.116 -then use "ML-Systems/ml_profiling_polyml-5.6.ML"
  26.117 -else use "ML-Systems/ml_profiling_polyml.ML";
  26.118 -
  26.119 -val pointer_eq = PolyML.pointerEq;
  26.120 -
  26.121 -
  26.122 -(* ML toplevel pretty printing *)
  26.123 -
  26.124 -use "ML-Systems/ml_pretty.ML";
  26.125 -
  26.126 -local
  26.127 -  val depth = Unsynchronized.ref 10;
  26.128 -in
  26.129 -  fun get_default_print_depth () = ! depth;
  26.130 -  fun default_print_depth n = (depth := n; PolyML.print_depth n);
  26.131 -  val _ = default_print_depth 10;
  26.132 -end;
  26.133 -
  26.134 -val error_depth = PolyML.error_depth;
  26.135 -
  26.136 -val pretty_ml =
  26.137 -  let
  26.138 -    fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
  26.139 -      | convert _ (PolyML.PrettyBlock (_, _,
  26.140 -            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
  26.141 -          ML_Pretty.Break (true, 1, 0)
  26.142 -      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
  26.143 -          let
  26.144 -            fun property name default =
  26.145 -              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
  26.146 -                SOME (PolyML.ContextProperty (_, b)) => b
  26.147 -              | _ => default);
  26.148 -            val bg = property "begin" "";
  26.149 -            val en = property "end" "";
  26.150 -            val len' = property "length" len;
  26.151 -          in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
  26.152 -      | convert len (PolyML.PrettyString s) =
  26.153 -          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
  26.154 -  in convert "" end;
  26.155 -
  26.156 -fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
  26.157 -  | ml_pretty (ML_Pretty.Break (true, _, _)) =
  26.158 -      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
  26.159 -        [PolyML.PrettyString " "])
  26.160 -  | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
  26.161 -      let val context =
  26.162 -        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
  26.163 -        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
  26.164 -      in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
  26.165 -  | ml_pretty (ML_Pretty.String (s, len)) =
  26.166 -      if len = size s then PolyML.PrettyString s
  26.167 -      else PolyML.PrettyBlock
  26.168 -        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
  26.169 -
  26.170 -
  26.171 -(* ML compiler *)
  26.172 -
  26.173 -structure ML_Name_Space =
  26.174 -struct
  26.175 -  open ML_Name_Space;
  26.176 -  val display_val = pretty_ml o displayVal;
  26.177 -end;
  26.178 -
  26.179 -use "ML-Systems/ml_compiler_parameters.ML";
  26.180 -if ML_System.name = "polyml-5.6"
  26.181 -then use "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" else ();
  26.182 -
  26.183 -use "ML-Systems/use_context.ML";
  26.184 -use "ML-Systems/ml_positions.ML";
  26.185 -use "ML-Systems/compiler_polyml.ML";
  26.186 -
  26.187 -PolyML.Compiler.reportUnreferencedIds := true;
  26.188 -PolyML.Compiler.printInAlphabeticalOrder := false;
  26.189 -PolyML.Compiler.maxInlineSize := 80;
  26.190 -
  26.191 -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
  26.192 -
  26.193 -use "ML-Systems/ml_parse_tree.ML";
  26.194 -if ML_System.name = "polyml-5.6"
  26.195 -then use "ML-Systems/ml_parse_tree_polyml-5.6.ML" else ();
  26.196 -
  26.197 -fun toplevel_pp context (_: string list) pp =
  26.198 -  use_text context {line = 1, file = "pp", verbose = false, debug = false}
  26.199 -    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
  26.200 -
  26.201 -fun ml_make_string struct_name =
  26.202 -  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
  26.203 -    struct_name ^ ".ML_print_depth ())))))";
  26.204 -
  26.205 -
  26.206 -(* ML debugger *)
  26.207 -
  26.208 -if ML_System.name = "polyml-5.6"
  26.209 -then use "ML-Systems/ml_debugger_polyml-5.6.ML"
  26.210 -else use "ML-Systems/ml_debugger.ML";
    27.1 --- a/src/Pure/ML-Systems/pp_dummy.ML	Wed Dec 23 21:15:26 2015 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,16 +0,0 @@
    27.4 -(*  Title:      Pure/ML-Systems/pp_dummy.ML
    27.5 -
    27.6 -Dummy setup for toplevel pretty printing.
    27.7 -*)
    27.8 -
    27.9 -fun ml_pretty _ = raise Fail "ml_pretty dummy";
   27.10 -fun pretty_ml _ = raise Fail "pretty_ml dummy";
   27.11 -
   27.12 -structure PolyML =
   27.13 -struct
   27.14 -  fun addPrettyPrinter _ = ();
   27.15 -  fun prettyRepresentation _ =
   27.16 -    raise Fail "PolyML.prettyRepresentation dummy";
   27.17 -  open PolyML;
   27.18 -end;
   27.19 -
    28.1 --- a/src/Pure/ML-Systems/proper_int.ML	Wed Dec 23 21:15:26 2015 +0100
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,289 +0,0 @@
    28.4 -(*  Title:      Pure/ML-Systems/proper_int.ML
    28.5 -    Author:     Makarius
    28.6 -
    28.7 -SML basis with type int representing proper integers, not machine
    28.8 -words.
    28.9 -*)
   28.10 -
   28.11 -val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
   28.12 -val dest_int = IntInf.toInt: IntInf.int -> Int.int;
   28.13 -
   28.14 -
   28.15 -(* Int *)
   28.16 -
   28.17 -type int = IntInf.int;
   28.18 -
   28.19 -structure IntInf =
   28.20 -struct
   28.21 -  open IntInf;
   28.22 -  fun fromInt (a: int) = a;
   28.23 -  fun toInt (a: int) = a;
   28.24 -  val log2 = mk_int o IntInf.log2;
   28.25 -  val sign = mk_int o IntInf.sign;
   28.26 -end;
   28.27 -
   28.28 -structure Int = IntInf;
   28.29 -
   28.30 -
   28.31 -(* List *)
   28.32 -
   28.33 -structure List =
   28.34 -struct
   28.35 -  open List;
   28.36 -  fun length a = mk_int (List.length a);
   28.37 -  fun nth (a, b) = List.nth (a, dest_int b);
   28.38 -  fun take (a, b) = List.take (a, dest_int b);
   28.39 -  fun drop (a, b) = List.drop (a, dest_int b);
   28.40 -  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
   28.41 -end;
   28.42 -
   28.43 -val length = List.length;
   28.44 -
   28.45 -
   28.46 -(* Array *)
   28.47 -
   28.48 -structure Array =
   28.49 -struct
   28.50 -  open Array;
   28.51 -  val maxLen = mk_int Array.maxLen;
   28.52 -  fun array (a, b) = Array.array (dest_int a, b);
   28.53 -  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
   28.54 -  fun length a = mk_int (Array.length a);
   28.55 -  fun sub (a, b) = Array.sub (a, dest_int b);
   28.56 -  fun update (a, b, c) = Array.update (a, dest_int b, c);
   28.57 -  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
   28.58 -  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
   28.59 -  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
   28.60 -  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
   28.61 -  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   28.62 -  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   28.63 -  fun findi a b =
   28.64 -    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
   28.65 -      NONE => NONE
   28.66 -    | SOME (c, d) => SOME (mk_int c, d));
   28.67 -end;
   28.68 -
   28.69 -
   28.70 -(* Vector *)
   28.71 -
   28.72 -structure Vector =
   28.73 -struct
   28.74 -  open Vector;
   28.75 -  val maxLen = mk_int Vector.maxLen;
   28.76 -  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
   28.77 -  fun length a = mk_int (Vector.length a);
   28.78 -  fun sub (a, b) = Vector.sub (a, dest_int b);
   28.79 -  fun update (a, b, c) = Vector.update (a, dest_int b, c);
   28.80 -  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
   28.81 -  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
   28.82 -  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   28.83 -  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   28.84 -  fun findi a b =
   28.85 -    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
   28.86 -      NONE => NONE
   28.87 -    | SOME (c, d) => SOME (mk_int c, d));
   28.88 -end;
   28.89 -
   28.90 -
   28.91 -(* CharVector *)
   28.92 -
   28.93 -structure CharVector =
   28.94 -struct
   28.95 -  open CharVector;
   28.96 -  fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
   28.97 -end;
   28.98 -
   28.99 -
  28.100 -(* Word8VectorSlice *)
  28.101 -
  28.102 -structure Word8VectorSlice =
  28.103 -struct
  28.104 -  open Word8VectorSlice;
  28.105 -  val length = mk_int o Word8VectorSlice.length;
  28.106 -  fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
  28.107 -end;
  28.108 -
  28.109 -
  28.110 -(* Char *)
  28.111 -
  28.112 -structure Char =
  28.113 -struct
  28.114 -  open Char;
  28.115 -  val maxOrd = mk_int Char.maxOrd;
  28.116 -  val chr = Char.chr o dest_int;
  28.117 -  val ord = mk_int o Char.ord;
  28.118 -end;
  28.119 -
  28.120 -val chr = Char.chr;
  28.121 -val ord = Char.ord;
  28.122 -
  28.123 -
  28.124 -(* String *)
  28.125 -
  28.126 -structure String =
  28.127 -struct
  28.128 -  open String;
  28.129 -  val maxSize = mk_int String.maxSize;
  28.130 -  val size = mk_int o String.size;
  28.131 -  fun sub (a, b) = String.sub (a, dest_int b);
  28.132 -  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
  28.133 -  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
  28.134 -end;
  28.135 -
  28.136 -val size = String.size;
  28.137 -val substring = String.substring;
  28.138 -
  28.139 -
  28.140 -(* Substring *)
  28.141 -
  28.142 -structure Substring =
  28.143 -struct
  28.144 -  open Substring;
  28.145 -  fun sub (a, b) = Substring.sub (a, dest_int b);
  28.146 -  val size = mk_int o Substring.size;
  28.147 -  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
  28.148 -  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
  28.149 -  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
  28.150 -  fun triml a b = Substring.triml (dest_int a) b;
  28.151 -  fun trimr a b = Substring.trimr (dest_int a) b;
  28.152 -  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
  28.153 -  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
  28.154 -end;
  28.155 -
  28.156 -
  28.157 -(* StringCvt *)
  28.158 -
  28.159 -structure StringCvt =
  28.160 -struct
  28.161 -  open StringCvt;
  28.162 -  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
  28.163 -  fun realfmt fmt = Real.fmt
  28.164 -    (case fmt of
  28.165 -      EXACT => StringCvt.EXACT
  28.166 -    | FIX NONE => StringCvt.FIX NONE
  28.167 -    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
  28.168 -    | GEN NONE => StringCvt.GEN NONE
  28.169 -    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
  28.170 -    | SCI NONE => StringCvt.SCI NONE
  28.171 -    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
  28.172 -  fun padRight a b c = StringCvt.padRight a (dest_int b) c;
  28.173 -  fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
  28.174 -end;
  28.175 -
  28.176 -
  28.177 -(* Word *)
  28.178 -
  28.179 -structure Word =
  28.180 -struct
  28.181 -  open Word;
  28.182 -  val wordSize = mk_int Word.wordSize;
  28.183 -  val toInt = Word.toLargeInt;
  28.184 -  val toIntX = Word.toLargeIntX;
  28.185 -  val fromInt = Word.fromLargeInt;
  28.186 -end;
  28.187 -
  28.188 -structure Word8 =
  28.189 -struct
  28.190 -  open Word8;
  28.191 -  val wordSize = mk_int Word8.wordSize;
  28.192 -  val toInt = Word8.toLargeInt;
  28.193 -  val toIntX = Word8.toLargeIntX;
  28.194 -  val fromInt = Word8.fromLargeInt;
  28.195 -end;
  28.196 -
  28.197 -structure Word32 =
  28.198 -struct
  28.199 -  open Word32;
  28.200 -  val wordSize = mk_int Word32.wordSize;
  28.201 -  val toInt = Word32.toLargeInt;
  28.202 -  val toIntX = Word32.toLargeIntX;
  28.203 -  val fromInt = Word32.fromLargeInt;
  28.204 -end;
  28.205 -
  28.206 -structure LargeWord =
  28.207 -struct
  28.208 -  open LargeWord;
  28.209 -  val wordSize = mk_int LargeWord.wordSize;
  28.210 -  val toInt = LargeWord.toLargeInt;
  28.211 -  val toIntX = LargeWord.toLargeIntX;
  28.212 -  val fromInt = LargeWord.fromLargeInt;
  28.213 -end;
  28.214 -
  28.215 -
  28.216 -(* Real *)
  28.217 -
  28.218 -structure Real =
  28.219 -struct
  28.220 -  open Real;
  28.221 -  val radix = mk_int Real.radix;
  28.222 -  val precision = mk_int Real.precision;
  28.223 -  fun sign a = mk_int (Real.sign a);
  28.224 -  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
  28.225 -  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
  28.226 -  val ceil = mk_int o Real.ceil;
  28.227 -  val floor = mk_int o Real.floor;
  28.228 -  val real = Real.fromInt o dest_int;
  28.229 -  val round = mk_int o Real.round;
  28.230 -  val trunc = mk_int o Real.trunc;
  28.231 -  fun toInt a b = mk_int (Real.toInt a b);
  28.232 -  fun fromInt a = Real.fromInt (dest_int a);
  28.233 -  val fmt = StringCvt.realfmt;
  28.234 -end;
  28.235 -
  28.236 -val ceil = Real.ceil;
  28.237 -val floor = Real.floor;
  28.238 -val real = Real.real;
  28.239 -val round = Real.round;
  28.240 -val trunc = Real.trunc;
  28.241 -
  28.242 -
  28.243 -(* TextIO *)
  28.244 -
  28.245 -structure TextIO =
  28.246 -struct
  28.247 -  open TextIO;
  28.248 -  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
  28.249 -  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
  28.250 -end;
  28.251 -
  28.252 -
  28.253 -(* BinIO *)
  28.254 -
  28.255 -structure BinIO =
  28.256 -struct
  28.257 -  open BinIO;
  28.258 -  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
  28.259 -  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
  28.260 -end;
  28.261 -
  28.262 -
  28.263 -(* Time *)
  28.264 -
  28.265 -structure Time =
  28.266 -struct
  28.267 -  open Time;
  28.268 -  fun fmt a b = Time.fmt (dest_int a) b;
  28.269 -end;
  28.270 -
  28.271 -
  28.272 -(* Sockets *)
  28.273 -
  28.274 -structure INetSock =
  28.275 -struct
  28.276 -  open INetSock;
  28.277 -  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
  28.278 -  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
  28.279 -end;
  28.280 -
  28.281 -
  28.282 -(* OS.FileSys *)
  28.283 -
  28.284 -structure OS =
  28.285 -struct
  28.286 -  open OS;
  28.287 -  structure FileSys =
  28.288 -  struct
  28.289 -    open FileSys;
  28.290 -    fun fileSize a = mk_int (FileSys.fileSize a);
  28.291 -  end;
  28.292 -end;
    29.1 --- a/src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML	Wed Dec 23 21:15:26 2015 +0100
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,11 +0,0 @@
    29.4 -(*  Title:      Pure/ML-Systems/share_common_data_polyml-5.3.0.ML
    29.5 -
    29.6 -Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
    29.7 -anymore.
    29.8 -*)
    29.9 -
   29.10 -structure PolyML =
   29.11 -struct
   29.12 -  open PolyML;
   29.13 -  fun shareCommonData _ = ();
   29.14 -end;
    30.1 --- a/src/Pure/ML-Systems/single_assignment.ML	Wed Dec 23 21:15:26 2015 +0100
    30.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.3 @@ -1,33 +0,0 @@
    30.4 -(*  Title:      Pure/ML-Systems/single_assignment.ML
    30.5 -    Author:     Makarius
    30.6 -
    30.7 -References with single assignment.  Unsynchronized!
    30.8 -*)
    30.9 -
   30.10 -signature SINGLE_ASSIGNMENT =
   30.11 -sig
   30.12 -  type 'a saref
   30.13 -  exception Locked
   30.14 -  val saref: unit -> 'a saref
   30.15 -  val savalue: 'a saref -> 'a option
   30.16 -  val saset: 'a saref * 'a -> unit
   30.17 -end;
   30.18 -
   30.19 -structure SingleAssignment: SINGLE_ASSIGNMENT =
   30.20 -struct
   30.21 -
   30.22 -exception Locked;
   30.23 -
   30.24 -abstype 'a saref = SARef of 'a option ref
   30.25 -with
   30.26 -
   30.27 -fun saref () = SARef (ref NONE);
   30.28 -
   30.29 -fun savalue (SARef r) = ! r;
   30.30 -
   30.31 -fun saset (SARef (r as ref NONE), x) = r := SOME x
   30.32 -  | saset _ = raise Locked;
   30.33 -
   30.34 -end;
   30.35 -
   30.36 -end;
    31.1 --- a/src/Pure/ML-Systems/single_assignment_polyml.ML	Wed Dec 23 21:15:26 2015 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,35 +0,0 @@
    31.4 -(*  Title:      Pure/ML-Systems/single_assignment_polyml.ML
    31.5 -    Author:     Makarius
    31.6 -
    31.7 -References with single assignment.  Unsynchronized!  Emulates
    31.8 -structure SingleAssignment from Poly/ML 5.4.
    31.9 -*)
   31.10 -
   31.11 -signature SINGLE_ASSIGNMENT =
   31.12 -sig
   31.13 -  type 'a saref
   31.14 -  exception Locked
   31.15 -  val saref: unit -> 'a saref
   31.16 -  val savalue: 'a saref -> 'a option
   31.17 -  val saset: 'a saref * 'a -> unit
   31.18 -end;
   31.19 -
   31.20 -structure SingleAssignment: SINGLE_ASSIGNMENT =
   31.21 -struct
   31.22 -
   31.23 -exception Locked;
   31.24 -
   31.25 -abstype 'a saref = SARef of 'a option ref
   31.26 -with
   31.27 -
   31.28 -fun saref () = SARef (ref NONE);
   31.29 -
   31.30 -fun savalue (SARef r) = ! r;
   31.31 -
   31.32 -fun saset (SARef (r as ref NONE), x) =
   31.33 -      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
   31.34 -  | saset _ = raise Locked;
   31.35 -
   31.36 -end;
   31.37 -
   31.38 -end;
    32.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Dec 23 21:15:26 2015 +0100
    32.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.3 @@ -1,194 +0,0 @@
    32.4 -(*  Title:      Pure/ML-Systems/smlnj.ML
    32.5 -
    32.6 -Compatibility file for Standard ML of New Jersey.
    32.7 -*)
    32.8 -
    32.9 -val io_buffer_size = 4096;
   32.10 -use "ML-Systems/proper_int.ML";
   32.11 -
   32.12 -exception Interrupt;
   32.13 -fun reraise exn = raise exn;
   32.14 -
   32.15 -fun exit rc = Posix.Process.exit (Word8.fromInt rc);
   32.16 -fun quit () = exit 0;
   32.17 -
   32.18 -use "ML-Systems/overloading_smlnj.ML";
   32.19 -use "General/exn.ML";
   32.20 -use "ML-Systems/single_assignment.ML";
   32.21 -use "ML-Systems/universal.ML";
   32.22 -use "ML-Systems/thread_dummy.ML";
   32.23 -use "ML-Systems/multithreading.ML";
   32.24 -use "ML-Systems/ml_stack_dummy.ML";
   32.25 -use "ML-Systems/ml_pretty.ML";
   32.26 -use "ML-Systems/ml_name_space.ML";
   32.27 -structure PolyML = struct end;
   32.28 -use "ML-Systems/pp_dummy.ML";
   32.29 -use "ML-Systems/use_context.ML";
   32.30 -use "ML-Systems/ml_positions.ML";
   32.31 -
   32.32 -
   32.33 -val seconds = Time.fromReal;
   32.34 -
   32.35 -(*low-level pointer equality*)
   32.36 -CM.autoload "$smlnj/init/init.cmi";
   32.37 -val pointer_eq = InlineT.ptreql;
   32.38 -
   32.39 -
   32.40 -(* restore old-style character / string functions *)
   32.41 -
   32.42 -val ord = mk_int o SML90.ord;
   32.43 -val chr = SML90.chr o dest_int;
   32.44 -val raw_explode = SML90.explode;
   32.45 -val implode = SML90.implode;
   32.46 -
   32.47 -
   32.48 -(* New Jersey ML parameters *)
   32.49 -
   32.50 -val _ =
   32.51 - (Control.Print.printLength := 1000;
   32.52 -  Control.Print.printDepth := 350;
   32.53 -  Control.Print.stringDepth := 250;
   32.54 -  Control.Print.signatures := 2;
   32.55 -  Control.MC.matchRedundantError := false);
   32.56 -
   32.57 -
   32.58 -(* Poly/ML emulation *)
   32.59 -
   32.60 -(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
   32.61 -local
   32.62 -  val depth = ref (10: int);
   32.63 -in
   32.64 -  fun get_default_print_depth () = ! depth;
   32.65 -  fun default_print_depth n =
   32.66 -   (depth := n;
   32.67 -    Control.Print.printDepth := dest_int n div 2;
   32.68 -    Control.Print.printLength := dest_int n);
   32.69 -  val _ = default_print_depth 10;
   32.70 -end;
   32.71 -
   32.72 -fun ml_make_string (_: string) = "(fn _ => \"?\")";
   32.73 -
   32.74 -
   32.75 -(*prompts*)
   32.76 -fun ml_prompts p1 p2 =
   32.77 -  (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
   32.78 -
   32.79 -(*dummy implementation*)
   32.80 -structure ML_Profiling =
   32.81 -struct
   32.82 -  fun profile_time (_: (int * string) list -> unit) f x = f x;
   32.83 -  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
   32.84 -  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
   32.85 -end;
   32.86 -
   32.87 -(*dummy implementation*)
   32.88 -fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
   32.89 -
   32.90 -
   32.91 -(* ML command execution *)
   32.92 -
   32.93 -fun use_text ({tune_source, print, error, ...}: use_context)
   32.94 -    {line, file, verbose, debug = _: bool} text =
   32.95 -  let
   32.96 -    val ref out_orig = Control.Print.out;
   32.97 -
   32.98 -    val out_buffer = ref ([]: string list);
   32.99 -    val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
  32.100 -    fun output () =
  32.101 -      let val str = implode (rev (! out_buffer))
  32.102 -      in String.substring (str, 0, Int.max (0, size str - 1)) end;
  32.103 -  in
  32.104 -    Control.Print.out := out;
  32.105 -    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
  32.106 -      handle exn =>
  32.107 -        (Control.Print.out := out_orig;
  32.108 -          error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
  32.109 -    Control.Print.out := out_orig;
  32.110 -    if verbose then print (output ()) else ()
  32.111 -  end;
  32.112 -
  32.113 -fun use_file context {verbose, debug} file =
  32.114 -  let
  32.115 -    val instream = TextIO.openIn file;
  32.116 -    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
  32.117 -  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
  32.118 -
  32.119 -
  32.120 -(* toplevel pretty printing *)
  32.121 -
  32.122 -fun ml_pprint pps =
  32.123 -  let
  32.124 -    fun str "" = ()
  32.125 -      | str s = PrettyPrint.string pps s;
  32.126 -    fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
  32.127 -         (str bg;
  32.128 -          (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
  32.129 -            (PrettyPrint.Rel (dest_int ind));
  32.130 -          List.app pprint prts; PrettyPrint.closeBox pps;
  32.131 -          str en)
  32.132 -      | pprint (ML_Pretty.String (s, _)) = str s
  32.133 -      | pprint (ML_Pretty.Break (false, width, offset)) =
  32.134 -          PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
  32.135 -      | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
  32.136 -  in pprint end;
  32.137 -
  32.138 -fun toplevel_pp context path pp =
  32.139 -  use_text context {line = 1, file = "pp", verbose = false, debug = false}
  32.140 -    ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
  32.141 -      "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
  32.142 -
  32.143 -
  32.144 -
  32.145 -(** interrupts **)
  32.146 -
  32.147 -local
  32.148 -
  32.149 -fun change_signal new_handler f x =
  32.150 -  let
  32.151 -    val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
  32.152 -    val result = Exn.capture (f old_handler) x;
  32.153 -    val _ = Signals.setHandler (Signals.sigINT, old_handler);
  32.154 -  in Exn.release result end;
  32.155 -
  32.156 -in
  32.157 -
  32.158 -fun interruptible (f: 'a -> 'b) x =
  32.159 -  let
  32.160 -    val result = ref (Exn.interrupt_exn: 'b Exn.result);
  32.161 -    val old_handler = Signals.inqHandler Signals.sigINT;
  32.162 -  in
  32.163 -    SMLofNJ.Cont.callcc (fn cont =>
  32.164 -      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
  32.165 -        result := Exn.capture f x));
  32.166 -    Signals.setHandler (Signals.sigINT, old_handler);
  32.167 -    Exn.release (! result)
  32.168 -  end;
  32.169 -
  32.170 -fun uninterruptible f =
  32.171 -  change_signal Signals.IGNORE
  32.172 -    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
  32.173 -
  32.174 -end;
  32.175 -
  32.176 -
  32.177 -use "ML-Systems/unsynchronized.ML";
  32.178 -use "ML-Systems/ml_debugger.ML";
  32.179 -
  32.180 -
  32.181 -(* ML system operations *)
  32.182 -
  32.183 -fun ml_platform_path (s: string) = s;
  32.184 -fun ml_standard_path (s: string) = s;
  32.185 -
  32.186 -use "ML-Systems/ml_system.ML";
  32.187 -
  32.188 -structure ML_System =
  32.189 -struct
  32.190 -
  32.191 -open ML_System;
  32.192 -
  32.193 -fun save_state name =
  32.194 -  if SMLofNJ.exportML name then ()
  32.195 -  else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
  32.196 -
  32.197 -end;
    33.1 --- a/src/Pure/ML-Systems/thread_dummy.ML	Wed Dec 23 21:15:26 2015 +0100
    33.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.3 @@ -1,82 +0,0 @@
    33.4 -(*  Title:      Pure/ML-Systems/thread_dummy.ML
    33.5 -    Author:     Makarius
    33.6 -
    33.7 -Default (mostly dummy) implementation of thread structures
    33.8 -(cf. polyml/basis/Thread.sml).
    33.9 -*)
   33.10 -
   33.11 -exception Thread of string;
   33.12 -
   33.13 -local fun fail _ = raise Thread "No multithreading support on this ML platform" in
   33.14 -
   33.15 -structure Mutex =
   33.16 -struct
   33.17 -  type mutex = unit;
   33.18 -  fun mutex _ = ();
   33.19 -  fun lock _ = fail ();
   33.20 -  fun unlock _ = fail ();
   33.21 -  fun trylock _ = fail ();
   33.22 -end;
   33.23 -
   33.24 -structure ConditionVar =
   33.25 -struct
   33.26 -  type conditionVar = unit;
   33.27 -  fun conditionVar _ = ();
   33.28 -  fun wait _ = fail ();
   33.29 -  fun waitUntil _ = fail ();
   33.30 -  fun signal _ = fail ();
   33.31 -  fun broadcast _ = fail ();
   33.32 -end;
   33.33 -
   33.34 -structure Thread =
   33.35 -struct
   33.36 -  type thread = unit;
   33.37 -
   33.38 -  datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
   33.39 -    and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
   33.40 -
   33.41 -  fun unavailable () = fail ();
   33.42 -
   33.43 -  fun fork _ = fail ();
   33.44 -  fun exit _ = fail ();
   33.45 -  fun isActive _ = fail ();
   33.46 -
   33.47 -  fun equal _ = fail ();
   33.48 -  fun self _ = fail ();
   33.49 -
   33.50 -  fun interrupt _ = fail ();
   33.51 -  fun broadcastInterrupt _ = fail ();
   33.52 -  fun testInterrupt _ = fail ();
   33.53 -
   33.54 -  fun kill _ = fail ();
   33.55 -
   33.56 -  fun setAttributes _ = fail ();
   33.57 -  fun getAttributes _ = fail ();
   33.58 -
   33.59 -  fun numProcessors _ = fail ();
   33.60 -
   33.61 -
   33.62 -(* thread data *)
   33.63 -
   33.64 -local
   33.65 -
   33.66 -val data = ref ([]: Universal.universal  ref list);
   33.67 -
   33.68 -fun find_data tag =
   33.69 -  let
   33.70 -    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
   33.71 -      | find [] = NONE;
   33.72 -  in find (! data) end;
   33.73 -
   33.74 -in
   33.75 -
   33.76 -fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
   33.77 -
   33.78 -fun setLocal (tag, x) =
   33.79 -  (case find_data tag of
   33.80 -    SOME r => r := Universal.tagInject tag x
   33.81 -  | NONE => data :=  ref (Universal.tagInject tag x) :: ! data);
   33.82 -
   33.83 -end;
   33.84 -end;
   33.85 -end;
    34.1 --- a/src/Pure/ML-Systems/universal.ML	Wed Dec 23 21:15:26 2015 +0100
    34.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.3 @@ -1,41 +0,0 @@
    34.4 -(*  Title:      Pure/ML-Systems/universal.ML
    34.5 -    Author:     Makarius
    34.6 -
    34.7 -Universal values via tagged union.  Emulates structure Universal
    34.8 -from Poly/ML 5.1.
    34.9 -*)
   34.10 -
   34.11 -signature UNIVERSAL =
   34.12 -sig
   34.13 -  type universal
   34.14 -  type 'a tag
   34.15 -  val tag: unit -> 'a tag
   34.16 -  val tagIs: 'a tag -> universal -> bool
   34.17 -  val tagInject: 'a tag -> 'a -> universal
   34.18 -  val tagProject: 'a tag -> universal -> 'a
   34.19 -end;
   34.20 -
   34.21 -structure Universal: UNIVERSAL =
   34.22 -struct
   34.23 -
   34.24 -type universal = exn;
   34.25 -
   34.26 -datatype 'a tag = Tag of
   34.27 - {is: universal -> bool,
   34.28 -  inject: 'a -> universal,
   34.29 -  project: universal -> 'a};
   34.30 -
   34.31 -fun tag () =
   34.32 -  let exception Universal of 'a in
   34.33 -   Tag {
   34.34 -    is = fn Universal _ => true | _ => false,
   34.35 -    inject = Universal,
   34.36 -    project = fn Universal x => x}
   34.37 -  end;
   34.38 -
   34.39 -fun tagIs (Tag {is, ...}) = is;
   34.40 -fun tagInject (Tag {inject, ...}) = inject;
   34.41 -fun tagProject (Tag {project, ...}) = project;
   34.42 -
   34.43 -end;
   34.44 -
    35.1 --- a/src/Pure/ML-Systems/unsynchronized.ML	Wed Dec 23 21:15:26 2015 +0100
    35.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.3 @@ -1,30 +0,0 @@
    35.4 -(*  Title:      Pure/ML-Systems/unsynchronized.ML
    35.5 -    Author:     Makarius
    35.6 -
    35.7 -Raw ML references as unsynchronized state variables.
    35.8 -*)
    35.9 -
   35.10 -structure Unsynchronized =
   35.11 -struct
   35.12 -
   35.13 -datatype ref = datatype ref;
   35.14 -
   35.15 -val op := = op :=;
   35.16 -val ! = !;
   35.17 -
   35.18 -fun change r f = r := f (! r);
   35.19 -fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
   35.20 -
   35.21 -fun inc i = (i := ! i + (1: int); ! i);
   35.22 -fun dec i = (i := ! i - (1: int); ! i);
   35.23 -
   35.24 -fun setmp flag value f x =
   35.25 -  uninterruptible (fn restore_attributes => fn () =>
   35.26 -    let
   35.27 -      val orig_value = ! flag;
   35.28 -      val _ = flag := value;
   35.29 -      val result = Exn.capture (restore_attributes f) x;
   35.30 -      val _ = flag := orig_value;
   35.31 -    in Exn.release result end) ();
   35.32 -
   35.33 -end;
    36.1 --- a/src/Pure/ML-Systems/use_context.ML	Wed Dec 23 21:15:26 2015 +0100
    36.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    36.3 @@ -1,13 +0,0 @@
    36.4 -(*  Title:      Pure/ML-Systems/use_context.ML
    36.5 -    Author:     Makarius
    36.6 -
    36.7 -Common context for "use" operations (compiler invocation).
    36.8 -*)
    36.9 -
   36.10 -type use_context =
   36.11 - {tune_source: string -> string,
   36.12 -  name_space: ML_Name_Space.T,
   36.13 -  str_of_pos: int -> string -> string,
   36.14 -  print: string -> unit,
   36.15 -  error: string -> unit};
   36.16 -
    37.1 --- a/src/Pure/ML-Systems/windows_path.ML	Wed Dec 23 21:15:26 2015 +0100
    37.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.3 @@ -1,34 +0,0 @@
    37.4 -(*  Title:      Pure/ML-Systems/windows_path.ML
    37.5 -    Author:     Makarius
    37.6 -
    37.7 -Windows file-system paths.
    37.8 -*)
    37.9 -
   37.10 -fun ml_platform_path path =
   37.11 -  if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
   37.12 -    (case String.tokens (fn c => c = #"/") path of
   37.13 -      "cygdrive" :: drive :: arcs =>
   37.14 -        let
   37.15 -          val vol =
   37.16 -            (case Char.fromString drive of
   37.17 -              NONE => drive ^ ":"
   37.18 -            | SOME d => String.str (Char.toUpper d) ^ ":");
   37.19 -        in String.concatWith "\\" (vol :: arcs) end
   37.20 -    | arcs =>
   37.21 -        (case OS.Process.getEnv "CYGWIN_ROOT" of
   37.22 -          SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
   37.23 -        | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
   37.24 -  else String.translate (fn #"/" => "\\" | c => String.str c) path;
   37.25 -
   37.26 -fun ml_standard_path path =
   37.27 -  let
   37.28 -    val {vol, arcs, isAbs} = OS.Path.fromString path;
   37.29 -    val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
   37.30 -  in
   37.31 -    if isAbs then
   37.32 -      (case String.explode vol of
   37.33 -        [d, #":"] =>
   37.34 -          String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
   37.35 -      | _ => path')
   37.36 -    else path'
   37.37 -  end;
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/src/Pure/RAW/compiler_polyml.ML	Wed Dec 23 23:09:13 2015 +0100
    38.3 @@ -0,0 +1,59 @@
    38.4 +(*  Title:      Pure/RAW/compiler_polyml.ML
    38.5 +
    38.6 +Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
    38.7 +*)
    38.8 +
    38.9 +local
   38.10 +
   38.11 +fun drop_newline s =
   38.12 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   38.13 +  else s;
   38.14 +
   38.15 +in
   38.16 +
   38.17 +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
   38.18 +    {line, file, verbose, debug} text =
   38.19 +  let
   38.20 +    val current_line = Unsynchronized.ref line;
   38.21 +    val in_buffer =
   38.22 +      Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
   38.23 +    val out_buffer = Unsynchronized.ref ([]: string list);
   38.24 +    fun output () = drop_newline (implode (rev (! out_buffer)));
   38.25 +
   38.26 +    fun get () =
   38.27 +      (case ! in_buffer of
   38.28 +        [] => NONE
   38.29 +      | c :: cs =>
   38.30 +          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
   38.31 +    fun put s = out_buffer := s :: ! out_buffer;
   38.32 +    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
   38.33 +     (put (if hard then "Error: " else "Warning: ");
   38.34 +      PolyML.prettyPrint (put, 76) msg1;
   38.35 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
   38.36 +      put ("At" ^ str_of_pos message_line file ^ "\n"));
   38.37 +
   38.38 +    val parameters =
   38.39 +     [PolyML.Compiler.CPOutStream put,
   38.40 +      PolyML.Compiler.CPNameSpace name_space,
   38.41 +      PolyML.Compiler.CPErrorMessageProc put_message,
   38.42 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
   38.43 +      PolyML.Compiler.CPFileName file,
   38.44 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
   38.45 +      ML_Compiler_Parameters.debug debug;
   38.46 +    val _ =
   38.47 +      (while not (List.null (! in_buffer)) do
   38.48 +        PolyML.compiler (get, parameters) ())
   38.49 +      handle exn =>
   38.50 +        if Exn.is_interrupt exn then reraise exn
   38.51 +        else
   38.52 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   38.53 +          error (output ()); reraise exn);
   38.54 +  in if verbose then print (output ()) else () end;
   38.55 +
   38.56 +fun use_file context {verbose, debug} file =
   38.57 +  let
   38.58 +    val instream = TextIO.openIn file;
   38.59 +    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   38.60 +  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
   38.61 +
   38.62 +end;
    39.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    39.2 +++ b/src/Pure/RAW/exn.ML	Wed Dec 23 23:09:13 2015 +0100
    39.3 @@ -0,0 +1,92 @@
    39.4 +(*  Title:      Pure/RAW/exn.ML
    39.5 +    Author:     Makarius
    39.6 +
    39.7 +Support for exceptions.
    39.8 +*)
    39.9 +
   39.10 +signature EXN =
   39.11 +sig
   39.12 +  datatype 'a result = Res of 'a | Exn of exn
   39.13 +  val get_res: 'a result -> 'a option
   39.14 +  val get_exn: 'a result -> exn option
   39.15 +  val capture: ('a -> 'b) -> 'a -> 'b result
   39.16 +  val release: 'a result -> 'a
   39.17 +  val map_res: ('a -> 'b) -> 'a result -> 'b result
   39.18 +  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
   39.19 +  val map_exn: (exn -> exn) -> 'a result -> 'a result
   39.20 +  exception Interrupt
   39.21 +  val interrupt: unit -> 'a
   39.22 +  val is_interrupt: exn -> bool
   39.23 +  val interrupt_exn: 'a result
   39.24 +  val is_interrupt_exn: 'a result -> bool
   39.25 +  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
   39.26 +  val return_code: exn -> int -> int
   39.27 +  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   39.28 +  exception EXCEPTIONS of exn list
   39.29 +end;
   39.30 +
   39.31 +structure Exn: EXN =
   39.32 +struct
   39.33 +
   39.34 +(* exceptions as values *)
   39.35 +
   39.36 +datatype 'a result =
   39.37 +  Res of 'a |
   39.38 +  Exn of exn;
   39.39 +
   39.40 +fun get_res (Res x) = SOME x
   39.41 +  | get_res _ = NONE;
   39.42 +
   39.43 +fun get_exn (Exn exn) = SOME exn
   39.44 +  | get_exn _ = NONE;
   39.45 +
   39.46 +fun capture f x = Res (f x) handle e => Exn e;
   39.47 +
   39.48 +fun release (Res y) = y
   39.49 +  | release (Exn e) = reraise e;
   39.50 +
   39.51 +fun map_res f (Res x) = Res (f x)
   39.52 +  | map_res f (Exn e) = Exn e;
   39.53 +
   39.54 +fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
   39.55 +
   39.56 +fun map_exn f (Res x) = Res x
   39.57 +  | map_exn f (Exn e) = Exn (f e);
   39.58 +
   39.59 +
   39.60 +(* interrupts *)
   39.61 +
   39.62 +exception Interrupt = Interrupt;
   39.63 +
   39.64 +fun interrupt () = raise Interrupt;
   39.65 +
   39.66 +fun is_interrupt Interrupt = true
   39.67 +  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
   39.68 +  | is_interrupt _ = false;
   39.69 +
   39.70 +val interrupt_exn = Exn Interrupt;
   39.71 +
   39.72 +fun is_interrupt_exn (Exn exn) = is_interrupt exn
   39.73 +  | is_interrupt_exn _ = false;
   39.74 +
   39.75 +fun interruptible_capture f x =
   39.76 +  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
   39.77 +
   39.78 +
   39.79 +(* POSIX return code *)
   39.80 +
   39.81 +fun return_code exn rc =
   39.82 +  if is_interrupt exn then (130: int) else rc;
   39.83 +
   39.84 +fun capture_exit rc f x =
   39.85 +  f x handle exn => exit (return_code exn rc);
   39.86 +
   39.87 +
   39.88 +(* concatenated exceptions *)
   39.89 +
   39.90 +exception EXCEPTIONS of exn list;
   39.91 +
   39.92 +end;
   39.93 +
   39.94 +datatype illegal = Interrupt;
   39.95 +
    40.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    40.2 +++ b/src/Pure/RAW/exn.scala	Wed Dec 23 23:09:13 2015 +0100
    40.3 @@ -0,0 +1,106 @@
    40.4 +/*  Title:      Pure/RAW/exn.scala
    40.5 +    Module:     PIDE
    40.6 +    Author:     Makarius
    40.7 +
    40.8 +Support for exceptions (arbitrary throwables).
    40.9 +*/
   40.10 +
   40.11 +package isabelle
   40.12 +
   40.13 +
   40.14 +object Exn
   40.15 +{
   40.16 +  /* exceptions as values */
   40.17 +
   40.18 +  sealed abstract class Result[A]
   40.19 +  {
   40.20 +    def user_error: Result[A] =
   40.21 +      this match {
   40.22 +        case Exn(ERROR(msg)) => Exn(ERROR(msg))
   40.23 +        case _ => this
   40.24 +      }
   40.25 +  }
   40.26 +  case class Res[A](res: A) extends Result[A]
   40.27 +  case class Exn[A](exn: Throwable) extends Result[A]
   40.28 +
   40.29 +  def capture[A](e: => A): Result[A] =
   40.30 +    try { Res(e) }
   40.31 +    catch { case exn: Throwable => Exn[A](exn) }
   40.32 +
   40.33 +  def release[A](result: Result[A]): A =
   40.34 +    result match {
   40.35 +      case Res(x) => x
   40.36 +      case Exn(exn) => throw exn
   40.37 +    }
   40.38 +
   40.39 +  def release_first[A](results: List[Result[A]]): List[A] =
   40.40 +    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
   40.41 +      case Some(Exn(exn)) => throw exn
   40.42 +      case _ => results.map(release(_))
   40.43 +    }
   40.44 +
   40.45 +
   40.46 +  /* interrupts */
   40.47 +
   40.48 +  def is_interrupt(exn: Throwable): Boolean =
   40.49 +  {
   40.50 +    var found_interrupt = false
   40.51 +    var e = exn
   40.52 +    while (!found_interrupt && e != null) {
   40.53 +      found_interrupt |= e.isInstanceOf[InterruptedException]
   40.54 +      e = e.getCause
   40.55 +    }
   40.56 +    found_interrupt
   40.57 +  }
   40.58 +
   40.59 +  object Interrupt
   40.60 +  {
   40.61 +    def apply(): Throwable = new InterruptedException
   40.62 +    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
   40.63 +
   40.64 +    def expose() { if (Thread.interrupted) throw apply() }
   40.65 +    def impose() { Thread.currentThread.interrupt }
   40.66 +
   40.67 +    def postpone[A](body: => A): Option[A] =
   40.68 +    {
   40.69 +      val interrupted = Thread.interrupted
   40.70 +      val result = capture { body }
   40.71 +      if (interrupted) impose()
   40.72 +      result match {
   40.73 +        case Res(x) => Some(x)
   40.74 +        case Exn(e) =>
   40.75 +          if (is_interrupt(e)) { impose(); None }
   40.76 +          else throw e
   40.77 +      }
   40.78 +    }
   40.79 +
   40.80 +    val return_code = 130
   40.81 +  }
   40.82 +
   40.83 +
   40.84 +  /* POSIX return code */
   40.85 +
   40.86 +  def return_code(exn: Throwable, rc: Int): Int =
   40.87 +    if (is_interrupt(exn)) Interrupt.return_code else rc
   40.88 +
   40.89 +
   40.90 +  /* message */
   40.91 +
   40.92 +  def user_message(exn: Throwable): Option[String] =
   40.93 +    if (exn.getClass == classOf[RuntimeException] ||
   40.94 +        exn.getClass == classOf[Library.User_Error])
   40.95 +    {
   40.96 +      val msg = exn.getMessage
   40.97 +      Some(if (msg == null || msg == "") "Error" else msg)
   40.98 +    }
   40.99 +    else if (exn.isInstanceOf[java.io.IOException])
  40.100 +    {
  40.101 +      val msg = exn.getMessage
  40.102 +      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
  40.103 +    }
  40.104 +    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
  40.105 +    else None
  40.106 +
  40.107 +  def message(exn: Throwable): String =
  40.108 +    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
  40.109 +}
    41.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    41.2 +++ b/src/Pure/RAW/exn_trace_polyml-5.5.1.ML	Wed Dec 23 23:09:13 2015 +0100
    41.3 @@ -0,0 +1,16 @@
    41.4 +(*  Title:      Pure/RAW/exn_trace_polyml-5.5.1.ML
    41.5 +    Author:     Makarius
    41.6 +
    41.7 +Exception trace for Poly/ML 5.5.1 via ML output.
    41.8 +*)
    41.9 +
   41.10 +fun print_exception_trace exn_message output e =
   41.11 +  PolyML.Exception.traceException
   41.12 +    (e, fn (trace, exn) =>
   41.13 +      let
   41.14 +        val title = "Exception trace - " ^ exn_message exn;
   41.15 +        val _ = output (String.concatWith "\n" (title :: trace));
   41.16 +      in reraise exn end);
   41.17 +
   41.18 +PolyML.Compiler.reportExhaustiveHandlers := true;
   41.19 +
    42.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    42.2 +++ b/src/Pure/RAW/ml_compiler_parameters.ML	Wed Dec 23 23:09:13 2015 +0100
    42.3 @@ -0,0 +1,17 @@
    42.4 +(*  Title:      Pure/ML/ml_compiler_parameters.ML
    42.5 +    Author:     Makarius
    42.6 +
    42.7 +Additional ML compiler parameters for Poly/ML.
    42.8 +*)
    42.9 +
   42.10 +signature ML_COMPILER_PARAMETERS =
   42.11 +sig
   42.12 +  val debug: bool -> PolyML.Compiler.compilerParameters list
   42.13 +end;
   42.14 +
   42.15 +structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
   42.16 +struct
   42.17 +
   42.18 +fun debug _ = [];
   42.19 +
   42.20 +end;
   42.21 \ No newline at end of file
    43.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    43.2 +++ b/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    43.3 @@ -0,0 +1,12 @@
    43.4 +(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.6.ML
    43.5 +    Author:     Makarius
    43.6 +
    43.7 +Additional ML compiler parameters for Poly/ML 5.6, or later.
    43.8 +*)
    43.9 +
   43.10 +structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
   43.11 +struct
   43.12 +
   43.13 +fun debug b = [PolyML.Compiler.CPDebug b];
   43.14 +
   43.15 +end;
   43.16 \ No newline at end of file
    44.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    44.2 +++ b/src/Pure/RAW/ml_debugger.ML	Wed Dec 23 23:09:13 2015 +0100
    44.3 @@ -0,0 +1,64 @@
    44.4 +(*  Title:      Pure/ML/ml_debugger.ML
    44.5 +    Author:     Makarius
    44.6 +
    44.7 +ML debugger interface -- dummy version.
    44.8 +*)
    44.9 +
   44.10 +signature ML_DEBUGGER =
   44.11 +sig
   44.12 +  type exn_id
   44.13 +  val exn_id: exn -> exn_id
   44.14 +  val print_exn_id: exn_id -> string
   44.15 +  val eq_exn_id: exn_id * exn_id -> bool
   44.16 +  val on_entry: (string * 'location -> unit) option -> unit
   44.17 +  val on_exit: (string * 'location -> unit) option -> unit
   44.18 +  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
   44.19 +  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
   44.20 +  type state
   44.21 +  val state: Thread.thread -> state list
   44.22 +  val debug_function: state -> string
   44.23 +  val debug_function_arg: state -> ML_Name_Space.valueVal
   44.24 +  val debug_function_result: state -> ML_Name_Space.valueVal
   44.25 +  val debug_location: state -> 'location
   44.26 +  val debug_name_space: state -> ML_Name_Space.T
   44.27 +  val debug_local_name_space: state -> ML_Name_Space.T
   44.28 +end;
   44.29 +
   44.30 +structure ML_Debugger: ML_DEBUGGER =
   44.31 +struct
   44.32 +
   44.33 +(* exceptions *)
   44.34 +
   44.35 +abstype exn_id = Exn_Id of string
   44.36 +with
   44.37 +
   44.38 +fun exn_id exn = Exn_Id (General.exnName exn);
   44.39 +fun print_exn_id (Exn_Id name) = name;
   44.40 +fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
   44.41 +
   44.42 +end;
   44.43 +
   44.44 +
   44.45 +(* hooks *)
   44.46 +
   44.47 +fun on_entry _ = ();
   44.48 +fun on_exit _ = ();
   44.49 +fun on_exit_exception _ = ();
   44.50 +fun on_breakpoint _ = ();
   44.51 +
   44.52 +
   44.53 +(* debugger *)
   44.54 +
   44.55 +fun fail () = raise Fail "No debugger support on this ML platform";
   44.56 +
   44.57 +type state = unit;
   44.58 +
   44.59 +fun state _ = [];
   44.60 +fun debug_function () = fail ();
   44.61 +fun debug_function_arg () = fail ();
   44.62 +fun debug_function_result () = fail ();
   44.63 +fun debug_location () = fail ();
   44.64 +fun debug_name_space () = fail ();
   44.65 +fun debug_local_name_space () = fail ();
   44.66 +
   44.67 +end;
    45.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    45.2 +++ b/src/Pure/RAW/ml_debugger_polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    45.3 @@ -0,0 +1,72 @@
    45.4 +(*  Title:      Pure/RAW/ml_debugger_polyml-5.6.ML
    45.5 +    Author:     Makarius
    45.6 +
    45.7 +ML debugger interface -- for Poly/ML 5.6, or later.
    45.8 +*)
    45.9 +
   45.10 +signature ML_DEBUGGER =
   45.11 +sig
   45.12 +  type exn_id
   45.13 +  val exn_id: exn -> exn_id
   45.14 +  val print_exn_id: exn_id -> string
   45.15 +  val eq_exn_id: exn_id * exn_id -> bool
   45.16 +  type location
   45.17 +  val on_entry: (string * location -> unit) option -> unit
   45.18 +  val on_exit: (string * location -> unit) option -> unit
   45.19 +  val on_exit_exception: (string * location -> exn -> unit) option -> unit
   45.20 +  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
   45.21 +  type state
   45.22 +  val state: Thread.thread -> state list
   45.23 +  val debug_function: state -> string
   45.24 +  val debug_function_arg: state -> ML_Name_Space.valueVal
   45.25 +  val debug_function_result: state -> ML_Name_Space.valueVal
   45.26 +  val debug_location: state -> location
   45.27 +  val debug_name_space: state -> ML_Name_Space.T
   45.28 +  val debug_local_name_space: state -> ML_Name_Space.T
   45.29 +end;
   45.30 +
   45.31 +structure ML_Debugger: ML_DEBUGGER =
   45.32 +struct
   45.33 +
   45.34 +(* exceptions *)
   45.35 +
   45.36 +abstype exn_id = Exn_Id of string * int Unsynchronized.ref
   45.37 +with
   45.38 +
   45.39 +fun exn_id exn =
   45.40 +  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
   45.41 +
   45.42 +fun print_exn_id (Exn_Id (name, _)) = name;
   45.43 +fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
   45.44 +
   45.45 +end;
   45.46 +
   45.47 +val _ =
   45.48 +  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
   45.49 +    let val s = print_exn_id exn_id
   45.50 +    in ml_pretty (ML_Pretty.String (s, size s)) end);
   45.51 +
   45.52 +
   45.53 +(* hooks *)
   45.54 +
   45.55 +type location = PolyML.location;
   45.56 +
   45.57 +val on_entry = PolyML.DebuggerInterface.setOnEntry;
   45.58 +val on_exit = PolyML.DebuggerInterface.setOnExit;
   45.59 +val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
   45.60 +val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
   45.61 +
   45.62 +
   45.63 +(* debugger operations *)
   45.64 +
   45.65 +type state = PolyML.DebuggerInterface.debugState;
   45.66 +
   45.67 +val state = PolyML.DebuggerInterface.debugState;
   45.68 +val debug_function = PolyML.DebuggerInterface.debugFunction;
   45.69 +val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
   45.70 +val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
   45.71 +val debug_location = PolyML.DebuggerInterface.debugLocation;
   45.72 +val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
   45.73 +val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
   45.74 +
   45.75 +end;
    46.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    46.2 +++ b/src/Pure/RAW/ml_name_space.ML	Wed Dec 23 23:09:13 2015 +0100
    46.3 @@ -0,0 +1,68 @@
    46.4 +(*  Title:      Pure/RAW/ml_name_space.ML
    46.5 +    Author:     Makarius
    46.6 +
    46.7 +ML name space -- dummy version of Poly/ML 5.2 facility.
    46.8 +*)
    46.9 +
   46.10 +structure ML_Name_Space =
   46.11 +struct
   46.12 +
   46.13 +type valueVal = unit;
   46.14 +type typeVal = unit;
   46.15 +type fixityVal = unit;
   46.16 +type structureVal = unit;
   46.17 +type signatureVal = unit;
   46.18 +type functorVal = unit;
   46.19 +
   46.20 +type T =
   46.21 + {lookupVal:    string -> valueVal option,
   46.22 +  lookupType:   string -> typeVal option,
   46.23 +  lookupFix:    string -> fixityVal option,
   46.24 +  lookupStruct: string -> structureVal option,
   46.25 +  lookupSig:    string -> signatureVal option,
   46.26 +  lookupFunct:  string -> functorVal option,
   46.27 +  enterVal:     string * valueVal -> unit,
   46.28 +  enterType:    string * typeVal -> unit,
   46.29 +  enterFix:     string * fixityVal -> unit,
   46.30 +  enterStruct:  string * structureVal -> unit,
   46.31 +  enterSig:     string * signatureVal -> unit,
   46.32 +  enterFunct:   string * functorVal -> unit,
   46.33 +  allVal:       unit -> (string * valueVal) list,
   46.34 +  allType:      unit -> (string * typeVal) list,
   46.35 +  allFix:       unit -> (string * fixityVal) list,
   46.36 +  allStruct:    unit -> (string * structureVal) list,
   46.37 +  allSig:       unit -> (string * signatureVal) list,
   46.38 +  allFunct:     unit -> (string * functorVal) list};
   46.39 +
   46.40 +val global: T =
   46.41 + {lookupVal = fn _ => NONE,
   46.42 +  lookupType = fn _ => NONE,
   46.43 +  lookupFix = fn _ => NONE,
   46.44 +  lookupStruct = fn _ => NONE,
   46.45 +  lookupSig = fn _ => NONE,
   46.46 +  lookupFunct = fn _ => NONE,
   46.47 +  enterVal = fn _ => (),
   46.48 +  enterType = fn _ => (),
   46.49 +  enterFix = fn _ => (),
   46.50 +  enterStruct = fn _ => (),
   46.51 +  enterSig = fn _ => (),
   46.52 +  enterFunct = fn _ => (),
   46.53 +  allVal = fn _ => [],
   46.54 +  allType = fn _ => [],
   46.55 +  allFix = fn _ => [],
   46.56 +  allStruct = fn _ => [],
   46.57 +  allSig = fn _ => [],
   46.58 +  allFunct = fn _ => []};
   46.59 +
   46.60 +val initial_val : (string * valueVal) list = [];
   46.61 +val initial_type : (string * typeVal) list = [];
   46.62 +val initial_fixity : (string * fixityVal) list = [];
   46.63 +val initial_structure : (string * structureVal) list = [];
   46.64 +val initial_signature : (string * signatureVal) list = [];
   46.65 +val initial_functor : (string * functorVal) list = [];
   46.66 +
   46.67 +fun forget_global_structure (_: string) = ();
   46.68 +
   46.69 +fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
   46.70 +
   46.71 +end;
    47.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    47.2 +++ b/src/Pure/RAW/ml_name_space_polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    47.3 @@ -0,0 +1,33 @@
    47.4 +(*  Title:      Pure/RAW/ml_name_space_polyml-5.6.ML
    47.5 +    Author:     Makarius
    47.6 +
    47.7 +Name space for Poly/ML.
    47.8 +*)
    47.9 +
   47.10 +structure ML_Name_Space =
   47.11 +struct
   47.12 +  open PolyML.NameSpace;
   47.13 +
   47.14 +  type T = PolyML.NameSpace.nameSpace;
   47.15 +  val global = PolyML.globalNameSpace;
   47.16 +  val forget_global_structure = PolyML.Compiler.forgetStructure;
   47.17 +
   47.18 +  type valueVal = Values.value;
   47.19 +  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   47.20 +  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
   47.21 +
   47.22 +  type typeVal = TypeConstrs.typeConstr;
   47.23 +  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   47.24 +
   47.25 +  type fixityVal = Infixes.fixity;
   47.26 +  fun displayFix (_: string, x) = Infixes.print x;
   47.27 +
   47.28 +  type structureVal = Structures.structureVal;
   47.29 +  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   47.30 +
   47.31 +  type signatureVal = Signatures.signatureVal;
   47.32 +  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
   47.33 +
   47.34 +  type functorVal = Functors.functorVal;
   47.35 +  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
   47.36 +end;
    48.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    48.2 +++ b/src/Pure/RAW/ml_name_space_polyml.ML	Wed Dec 23 23:09:13 2015 +0100
    48.3 @@ -0,0 +1,13 @@
    48.4 +(*  Title:      Pure/RAW/ml_name_space_polyml.ML
    48.5 +    Author:     Makarius
    48.6 +
    48.7 +Name space for Poly/ML.
    48.8 +*)
    48.9 +
   48.10 +structure ML_Name_Space =
   48.11 +struct
   48.12 +  open PolyML.NameSpace;
   48.13 +  type T = nameSpace;
   48.14 +  val global = PolyML.globalNameSpace;
   48.15 +  val forget_global_structure = PolyML.Compiler.forgetStructure;
   48.16 +end;
    49.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    49.2 +++ b/src/Pure/RAW/ml_parse_tree.ML	Wed Dec 23 23:09:13 2015 +0100
    49.3 @@ -0,0 +1,19 @@
    49.4 +(*  Title:      Pure/ML/ml_parse_tree.ML
    49.5 +    Author:     Makarius
    49.6 +
    49.7 +Additional ML parse tree components for Poly/ML.
    49.8 +*)
    49.9 +
   49.10 +signature ML_PARSE_TREE =
   49.11 +sig
   49.12 +  val completions: PolyML.ptProperties -> string list option
   49.13 +  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
   49.14 +end;
   49.15 +
   49.16 +structure ML_Parse_Tree: ML_PARSE_TREE =
   49.17 +struct
   49.18 +
   49.19 +fun completions _ = NONE;
   49.20 +fun breakpoint _ = NONE;
   49.21 +
   49.22 +end;
   49.23 \ No newline at end of file
    50.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    50.2 +++ b/src/Pure/RAW/ml_parse_tree_polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    50.3 @@ -0,0 +1,16 @@
    50.4 +(*  Title:      Pure/RAW/ml_parse_tree_polyml-5.6.ML
    50.5 +    Author:     Makarius
    50.6 +
    50.7 +Additional ML parse tree components for Poly/ML 5.6, or later.
    50.8 +*)
    50.9 +
   50.10 +structure ML_Parse_Tree: ML_PARSE_TREE =
   50.11 +struct
   50.12 +
   50.13 +fun completions (PolyML.PTcompletions x) = SOME x
   50.14 +  | completions _ = NONE;
   50.15 +
   50.16 +fun breakpoint (PolyML.PTbreakPoint x) = SOME x
   50.17 +  | breakpoint _ = NONE;
   50.18 +
   50.19 +end;
   50.20 \ No newline at end of file
    51.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    51.2 +++ b/src/Pure/RAW/ml_positions.ML	Wed Dec 23 23:09:13 2015 +0100
    51.3 @@ -0,0 +1,16 @@
    51.4 +(*  Title:      Pure/RAW/ml_positions.ML
    51.5 +    Author:     Makarius
    51.6 +
    51.7 +Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
    51.8 +*)
    51.9 +
   51.10 +fun ml_positions start_line name txt =
   51.11 +  let
   51.12 +    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
   51.13 +          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
   51.14 +          in positions line cs (s :: res) end
   51.15 +      | positions line (c :: cs) res =
   51.16 +          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
   51.17 +      | positions _ [] res = rev res;
   51.18 +  in String.concat (positions start_line (String.explode txt) []) end;
   51.19 +
    52.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    52.2 +++ b/src/Pure/RAW/ml_pretty.ML	Wed Dec 23 23:09:13 2015 +0100
    52.3 @@ -0,0 +1,30 @@
    52.4 +(*  Title:      Pure/RAW/ml_pretty.ML
    52.5 +    Author:     Makarius
    52.6 +
    52.7 +Minimal support for raw ML pretty printing -- for boot-strapping only.
    52.8 +*)
    52.9 +
   52.10 +structure ML_Pretty =
   52.11 +struct
   52.12 +
   52.13 +datatype pretty =
   52.14 +  Block of (string * string) * bool * int * pretty list |
   52.15 +  String of string * int |
   52.16 +  Break of bool * int * int;
   52.17 +
   52.18 +fun block prts = Block (("", ""), false, 2, prts);
   52.19 +fun str s = String (s, size s);
   52.20 +fun brk width = Break (false, width, 0);
   52.21 +
   52.22 +fun pair pretty1 pretty2 ((x, y), depth: int) =
   52.23 +  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
   52.24 +
   52.25 +fun enum sep lpar rpar pretty (args, depth) =
   52.26 +  let
   52.27 +    fun elems _ [] = []
   52.28 +      | elems 0 _ = [str "..."]
   52.29 +      | elems d [x] = [pretty (x, d)]
   52.30 +      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
   52.31 +  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
   52.32 +
   52.33 +end;
    53.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    53.2 +++ b/src/Pure/RAW/ml_profiling_polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    53.3 @@ -0,0 +1,19 @@
    53.4 +(*  Title:      Pure/RAW/ml_profiling_polyml-5.6.ML
    53.5 +    Author:     Makarius
    53.6 +
    53.7 +Profiling for Poly/ML 5.6.
    53.8 +*)
    53.9 +
   53.10 +structure ML_Profiling =
   53.11 +struct
   53.12 +
   53.13 +fun profile_time pr f x =
   53.14 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   53.15 +
   53.16 +fun profile_time_thread pr f x =
   53.17 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   53.18 +
   53.19 +fun profile_allocations pr f x =
   53.20 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   53.21 +
   53.22 +end;
    54.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    54.2 +++ b/src/Pure/RAW/ml_profiling_polyml.ML	Wed Dec 23 23:09:13 2015 +0100
    54.3 @@ -0,0 +1,27 @@
    54.4 +(*  Title:      Pure/RAW/ml_profiling_polyml.ML
    54.5 +    Author:     Makarius
    54.6 +
    54.7 +Profiling for Poly/ML.
    54.8 +*)
    54.9 +
   54.10 +structure ML_Profiling =
   54.11 +struct
   54.12 +
   54.13 +local
   54.14 +
   54.15 +fun profile n f x =
   54.16 +  let
   54.17 +    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   54.18 +    val res = Exn.capture f x;
   54.19 +    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   54.20 +  in Exn.release res end;
   54.21 +
   54.22 +in
   54.23 +
   54.24 +fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
   54.25 +fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
   54.26 +fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
   54.27 +
   54.28 +end;
   54.29 +
   54.30 +end;
    55.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    55.2 +++ b/src/Pure/RAW/ml_stack_dummy.ML	Wed Dec 23 23:09:13 2015 +0100
    55.3 @@ -0,0 +1,16 @@
    55.4 +(*  Title:      Pure/RAW/ml_stack_dummy.ML
    55.5 +
    55.6 +Maximum stack size (in words) for ML threads -- dummy version.
    55.7 +*)
    55.8 +
    55.9 +signature ML_STACK =
   55.10 +sig
   55.11 +  val limit: int option -> Thread.threadAttribute list
   55.12 +end;
   55.13 +
   55.14 +structure ML_Stack: ML_STACK =
   55.15 +struct
   55.16 +
   55.17 +fun limit (_: int option) : Thread.threadAttribute list = [];
   55.18 +
   55.19 +end;
    56.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    56.2 +++ b/src/Pure/RAW/ml_stack_polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    56.3 @@ -0,0 +1,16 @@
    56.4 +(*  Title:      Pure/RAW/ml_stack_polyml-5.6.ML
    56.5 +
    56.6 +Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
    56.7 +*)
    56.8 +
    56.9 +signature ML_STACK =
   56.10 +sig
   56.11 +  val limit: int option -> Thread.threadAttribute list
   56.12 +end;
   56.13 +
   56.14 +structure ML_Stack: ML_STACK =
   56.15 +struct
   56.16 +
   56.17 +fun limit m = [Thread.MaximumMLStack m];
   56.18 +
   56.19 +end;
    57.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    57.2 +++ b/src/Pure/RAW/ml_system.ML	Wed Dec 23 23:09:13 2015 +0100
    57.3 @@ -0,0 +1,32 @@
    57.4 +(*  Title:      Pure/RAW/ml_system.ML
    57.5 +    Author:     Makarius
    57.6 +
    57.7 +ML system and platform operations.
    57.8 +*)
    57.9 +
   57.10 +signature ML_SYSTEM =
   57.11 +sig
   57.12 +  val name: string
   57.13 +  val is_polyml: bool
   57.14 +  val is_smlnj: bool
   57.15 +  val platform: string
   57.16 +  val platform_is_windows: bool
   57.17 +  val share_common_data: unit -> unit
   57.18 +  val save_state: string -> unit
   57.19 +end;
   57.20 +
   57.21 +structure ML_System: ML_SYSTEM =
   57.22 +struct
   57.23 +
   57.24 +val SOME name = OS.Process.getEnv "ML_SYSTEM";
   57.25 +val is_polyml = String.isPrefix "polyml" name;
   57.26 +val is_smlnj = String.isPrefix "smlnj" name;
   57.27 +
   57.28 +val SOME platform = OS.Process.getEnv "ML_PLATFORM";
   57.29 +val platform_is_windows = String.isSuffix "windows" platform;
   57.30 +
   57.31 +fun share_common_data () = ();
   57.32 +fun save_state _ = raise Fail "Cannot save state -- undefined operation";
   57.33 +
   57.34 +end;
   57.35 +
    58.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    58.2 +++ b/src/Pure/RAW/multithreading.ML	Wed Dec 23 23:09:13 2015 +0100
    58.3 @@ -0,0 +1,75 @@
    58.4 +(*  Title:      Pure/RAW/multithreading.ML
    58.5 +    Author:     Makarius
    58.6 +
    58.7 +Dummy implementation of multithreading setup.
    58.8 +*)
    58.9 +
   58.10 +signature MULTITHREADING =
   58.11 +sig
   58.12 +  val available: bool
   58.13 +  val max_threads_value: unit -> int
   58.14 +  val max_threads_update: int -> unit
   58.15 +  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
   58.16 +  val enabled: unit -> bool
   58.17 +  val no_interrupts: Thread.threadAttribute list
   58.18 +  val public_interrupts: Thread.threadAttribute list
   58.19 +  val private_interrupts: Thread.threadAttribute list
   58.20 +  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
   58.21 +  val interrupted: unit -> unit  (*exception Interrupt*)
   58.22 +  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   58.23 +  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
   58.24 +    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   58.25 +  val trace: int ref
   58.26 +  val tracing: int -> (unit -> string) -> unit
   58.27 +  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   58.28 +  val real_time: ('a -> unit) -> 'a -> Time.time
   58.29 +  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
   58.30 +  val serial: unit -> int
   58.31 +end;
   58.32 +
   58.33 +structure Multithreading: MULTITHREADING =
   58.34 +struct
   58.35 +
   58.36 +(* options *)
   58.37 +
   58.38 +val available = false;
   58.39 +fun max_threads_value () = 1: int;
   58.40 +fun max_threads_update _ = ();
   58.41 +fun max_threads_setmp _ f x = f x;
   58.42 +fun enabled () = false;
   58.43 +
   58.44 +
   58.45 +(* attributes *)
   58.46 +
   58.47 +val no_interrupts = [];
   58.48 +val public_interrupts = [];
   58.49 +val private_interrupts = [];
   58.50 +fun sync_interrupts _ = [];
   58.51 +
   58.52 +fun interrupted () = ();
   58.53 +
   58.54 +fun with_attributes _ e = e [];
   58.55 +
   58.56 +fun sync_wait _ _ _ _ = Exn.Res true;
   58.57 +
   58.58 +
   58.59 +(* tracing *)
   58.60 +
   58.61 +val trace = ref (0: int);
   58.62 +fun tracing _ _ = ();
   58.63 +fun tracing_time _ _ _ = ();
   58.64 +fun real_time f x = (f x; Time.zeroTime);
   58.65 +
   58.66 +
   58.67 +(* synchronized evaluation *)
   58.68 +
   58.69 +fun synchronized _ _ e = e ();
   58.70 +
   58.71 +
   58.72 +(* serial numbers *)
   58.73 +
   58.74 +local val count = ref (0: int)
   58.75 +in fun serial () = (count := ! count + 1; ! count) end;
   58.76 +
   58.77 +end;
   58.78 +
    59.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    59.2 +++ b/src/Pure/RAW/multithreading_polyml.ML	Wed Dec 23 23:09:13 2015 +0100
    59.3 @@ -0,0 +1,172 @@
    59.4 +(*  Title:      Pure/RAW/multithreading_polyml.ML
    59.5 +    Author:     Makarius
    59.6 +
    59.7 +Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
    59.8 +*)
    59.9 +
   59.10 +signature MULTITHREADING =
   59.11 +sig
   59.12 +  include MULTITHREADING
   59.13 +  val interruptible: ('a -> 'b) -> 'a -> 'b
   59.14 +  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   59.15 +end;
   59.16 +
   59.17 +structure Multithreading: MULTITHREADING =
   59.18 +struct
   59.19 +
   59.20 +(* thread attributes *)
   59.21 +
   59.22 +val no_interrupts =
   59.23 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
   59.24 +
   59.25 +val test_interrupts =
   59.26 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
   59.27 +
   59.28 +val public_interrupts =
   59.29 +  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
   59.30 +
   59.31 +val private_interrupts =
   59.32 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
   59.33 +
   59.34 +val sync_interrupts = map
   59.35 +  (fn x as Thread.InterruptState Thread.InterruptDefer => x
   59.36 +    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
   59.37 +    | x => x);
   59.38 +
   59.39 +val safe_interrupts = map
   59.40 +  (fn Thread.InterruptState Thread.InterruptAsynch =>
   59.41 +      Thread.InterruptState Thread.InterruptAsynchOnce
   59.42 +    | x => x);
   59.43 +
   59.44 +fun interrupted () =
   59.45 +  let
   59.46 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
   59.47 +    val _ = Thread.setAttributes test_interrupts;
   59.48 +    val test = Exn.capture Thread.testInterrupt ();
   59.49 +    val _ = Thread.setAttributes orig_atts;
   59.50 +  in Exn.release test end;
   59.51 +
   59.52 +fun with_attributes new_atts e =
   59.53 +  let
   59.54 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
   59.55 +    val result = Exn.capture (fn () =>
   59.56 +      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
   59.57 +    val _ = Thread.setAttributes orig_atts;
   59.58 +  in Exn.release result end;
   59.59 +
   59.60 +
   59.61 +(* portable wrappers *)
   59.62 +
   59.63 +fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
   59.64 +
   59.65 +fun uninterruptible f x =
   59.66 +  with_attributes no_interrupts (fn atts =>
   59.67 +    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
   59.68 +
   59.69 +
   59.70 +(* options *)
   59.71 +
   59.72 +val available = true;
   59.73 +
   59.74 +fun max_threads_result m =
   59.75 +  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
   59.76 +
   59.77 +val max_threads = ref 1;
   59.78 +
   59.79 +fun max_threads_value () = ! max_threads;
   59.80 +
   59.81 +fun max_threads_update m = max_threads := max_threads_result m;
   59.82 +
   59.83 +fun max_threads_setmp m f x =
   59.84 +  uninterruptible (fn restore_attributes => fn () =>
   59.85 +    let
   59.86 +      val max_threads_orig = ! max_threads;
   59.87 +      val _ = max_threads_update m;
   59.88 +      val result = Exn.capture (restore_attributes f) x;
   59.89 +      val _ = max_threads := max_threads_orig;
   59.90 +    in Exn.release result end) ();
   59.91 +
   59.92 +fun enabled () = max_threads_value () > 1;
   59.93 +
   59.94 +
   59.95 +(* synchronous wait *)
   59.96 +
   59.97 +fun sync_wait opt_atts time cond lock =
   59.98 +  with_attributes
   59.99 +    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
  59.100 +    (fn _ =>
  59.101 +      (case time of
  59.102 +        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
  59.103 +      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
  59.104 +      handle exn => Exn.Exn exn);
  59.105 +
  59.106 +
  59.107 +(* tracing *)
  59.108 +
  59.109 +val trace = ref 0;
  59.110 +
  59.111 +fun tracing level msg =
  59.112 +  if level > ! trace then ()
  59.113 +  else uninterruptible (fn _ => fn () =>
  59.114 +    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
  59.115 +      handle _ (*sic*) => ()) ();
  59.116 +
  59.117 +fun tracing_time detailed time =
  59.118 +  tracing
  59.119 +   (if not detailed then 5
  59.120 +    else if Time.>= (time, seconds 1.0) then 1
  59.121 +    else if Time.>= (time, seconds 0.1) then 2
  59.122 +    else if Time.>= (time, seconds 0.01) then 3
  59.123 +    else if Time.>= (time, seconds 0.001) then 4 else 5);
  59.124 +
  59.125 +fun real_time f x =
  59.126 +  let
  59.127 +    val timer = Timer.startRealTimer ();
  59.128 +    val () = f x;
  59.129 +    val time = Timer.checkRealTimer timer;
  59.130 +  in time end;
  59.131 +
  59.132 +
  59.133 +(* synchronized evaluation *)
  59.134 +
  59.135 +fun synchronized name lock e =
  59.136 +  Exn.release (uninterruptible (fn restore_attributes => fn () =>
  59.137 +    let
  59.138 +      val immediate =
  59.139 +        if Mutex.trylock lock then true
  59.140 +        else
  59.141 +          let
  59.142 +            val _ = tracing 5 (fn () => name ^ ": locking ...");
  59.143 +            val time = real_time Mutex.lock lock;
  59.144 +            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
  59.145 +          in false end;
  59.146 +      val result = Exn.capture (restore_attributes e) ();
  59.147 +      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
  59.148 +      val _ = Mutex.unlock lock;
  59.149 +    in result end) ());
  59.150 +
  59.151 +
  59.152 +(* serial numbers *)
  59.153 +
  59.154 +local
  59.155 +
  59.156 +val serial_lock = Mutex.mutex ();
  59.157 +val serial_count = ref 0;
  59.158 +
  59.159 +in
  59.160 +
  59.161 +val serial = uninterruptible (fn _ => fn () =>
  59.162 +  let
  59.163 +    val _ = Mutex.lock serial_lock;
  59.164 +    val _ = serial_count := ! serial_count + 1;
  59.165 +    val res = ! serial_count;
  59.166 +    val _ = Mutex.unlock serial_lock;
  59.167 +  in res end);
  59.168 +
  59.169 +end;
  59.170 +
  59.171 +end;
  59.172 +
  59.173 +val interruptible = Multithreading.interruptible;
  59.174 +val uninterruptible = Multithreading.uninterruptible;
  59.175 +
    60.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    60.2 +++ b/src/Pure/RAW/overloading_smlnj.ML	Wed Dec 23 23:09:13 2015 +0100
    60.3 @@ -0,0 +1,41 @@
    60.4 +(*  Title:      Pure/RAW/overloading_smlnj.ML
    60.5 +    Author:     Makarius
    60.6 +
    60.7 +Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
    60.8 +*)
    60.9 +
   60.10 +Control.overloadKW := true;
   60.11 +
   60.12 +overload ~ : ('a -> 'a) as
   60.13 +  IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
   60.14 +  Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
   60.15 +overload + : ('a * 'a -> 'a) as
   60.16 +  IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
   60.17 +  Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
   60.18 +overload - : ('a * 'a -> 'a) as
   60.19 +  IntInf.- and Int31.- and Int32.- and Int64.- and
   60.20 +  Word.- and Word8.- and Word32.- and Word64.- and Real.-;
   60.21 +overload * : ('a * 'a -> 'a) as
   60.22 +  IntInf.* and Int31.* and Int32.* and Int64.* and
   60.23 +  Word.* and Word8.* and Word32.* and Word64.* and Real.*;
   60.24 +overload div: ('a * 'a -> 'a) as
   60.25 +  IntInf.div and Int31.div and Int32.div and Int64.div and
   60.26 +  Word.div and Word8.div and Word32.div and Word64.div;
   60.27 +overload mod: ('a * 'a -> 'a) as
   60.28 +  IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
   60.29 +  Word.mod and Word8.mod and Word32.mod and Word64.mod;
   60.30 +overload < : ('a * 'a -> bool) as
   60.31 +  IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
   60.32 +  Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
   60.33 +overload <= : ('a * 'a -> bool) as
   60.34 +  IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
   60.35 +  Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
   60.36 +overload > : ('a * 'a -> bool) as
   60.37 +  IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
   60.38 +  Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
   60.39 +overload >= : ('a * 'a -> bool) as
   60.40 +  IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
   60.41 +  Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
   60.42 +overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
   60.43 +
   60.44 +Control.overloadKW := false;
    61.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    61.2 +++ b/src/Pure/RAW/polyml-5.5.2.ML	Wed Dec 23 23:09:13 2015 +0100
    61.3 @@ -0,0 +1,23 @@
    61.4 +(*  Title:      Pure/RAW/polyml-5.5.2.ML
    61.5 +    Author:     Makarius
    61.6 +
    61.7 +Compatibility wrapper for Poly/ML 5.5.2.
    61.8 +*)
    61.9 +
   61.10 +structure Thread =
   61.11 +struct
   61.12 +  open Thread;
   61.13 +
   61.14 +  structure Thread =
   61.15 +  struct
   61.16 +    open Thread;
   61.17 +
   61.18 +    fun numProcessors () =
   61.19 +      (case Thread.numPhysicalProcessors () of
   61.20 +        SOME n => n
   61.21 +      | NONE => Thread.numProcessors ());
   61.22 +  end;
   61.23 +end;
   61.24 +
   61.25 +use "RAW/polyml.ML";
   61.26 +
    62.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    62.2 +++ b/src/Pure/RAW/polyml-5.6.ML	Wed Dec 23 23:09:13 2015 +0100
    62.3 @@ -0,0 +1,22 @@
    62.4 +(*  Title:      Pure/RAW/polyml-5.6.ML
    62.5 +    Author:     Makarius
    62.6 +
    62.7 +Compatibility wrapper for Poly/ML 5.6.
    62.8 +*)
    62.9 +
   62.10 +structure Thread =
   62.11 +struct
   62.12 +  open Thread;
   62.13 +
   62.14 +  structure Thread =
   62.15 +  struct
   62.16 +    open Thread;
   62.17 +
   62.18 +    fun numProcessors () =
   62.19 +      (case Thread.numPhysicalProcessors () of
   62.20 +        SOME n => n
   62.21 +      | NONE => Thread.numProcessors ());
   62.22 +  end;
   62.23 +end;
   62.24 +
   62.25 +use "RAW/polyml.ML";
    63.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    63.2 +++ b/src/Pure/RAW/polyml.ML	Wed Dec 23 23:09:13 2015 +0100
    63.3 @@ -0,0 +1,207 @@
    63.4 +(*  Title:      Pure/RAW/polyml.ML
    63.5 +    Author:     Makarius
    63.6 +
    63.7 +Compatibility wrapper for Poly/ML.
    63.8 +*)
    63.9 +
   63.10 +(* initial ML name space *)
   63.11 +
   63.12 +use "RAW/ml_system.ML";
   63.13 +
   63.14 +if ML_System.name = "polyml-5.6"
   63.15 +then use "RAW/ml_name_space_polyml-5.6.ML"
   63.16 +else use "RAW/ml_name_space_polyml.ML";
   63.17 +
   63.18 +structure ML_Name_Space =
   63.19 +struct
   63.20 +  open ML_Name_Space;
   63.21 +  val initial_val =
   63.22 +    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
   63.23 +      (#allVal global ());
   63.24 +  val initial_type = #allType global ();
   63.25 +  val initial_fixity = #allFix global ();
   63.26 +  val initial_structure = #allStruct global ();
   63.27 +  val initial_signature = #allSig global ();
   63.28 +  val initial_functor = #allFunct global ();
   63.29 +end;
   63.30 +
   63.31 +
   63.32 +(* ML system operations *)
   63.33 +
   63.34 +if ML_System.name = "polyml-5.3.0"
   63.35 +then use "RAW/share_common_data_polyml-5.3.0.ML"
   63.36 +else ();
   63.37 +
   63.38 +fun ml_platform_path (s: string) = s;
   63.39 +fun ml_standard_path (s: string) = s;
   63.40 +
   63.41 +if ML_System.platform_is_windows then use "RAW/windows_path.ML" else ();
   63.42 +
   63.43 +structure ML_System =
   63.44 +struct
   63.45 +  open ML_System;
   63.46 +  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   63.47 +  val save_state = PolyML.SaveState.saveState o ml_platform_path;
   63.48 +end;
   63.49 +
   63.50 +
   63.51 +(* exceptions *)
   63.52 +
   63.53 +fun reraise exn =
   63.54 +  (case PolyML.exceptionLocation exn of
   63.55 +    NONE => raise exn
   63.56 +  | SOME location => PolyML.raiseWithLocation (exn, location));
   63.57 +
   63.58 +exception Interrupt = SML90.Interrupt;
   63.59 +
   63.60 +use "RAW/exn.ML";
   63.61 +
   63.62 +fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
   63.63 +
   63.64 +if ML_System.name = "polyml-5.5.1"
   63.65 +  orelse ML_System.name = "polyml-5.5.2"
   63.66 +  orelse ML_System.name = "polyml-5.6"
   63.67 +then use "RAW/exn_trace_polyml-5.5.1.ML"
   63.68 +else ();
   63.69 +
   63.70 +
   63.71 +(* multithreading *)
   63.72 +
   63.73 +val seconds = Time.fromReal;
   63.74 +
   63.75 +if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
   63.76 +then ()
   63.77 +else use "RAW/single_assignment_polyml.ML";
   63.78 +
   63.79 +open Thread;
   63.80 +use "RAW/multithreading.ML";
   63.81 +use "RAW/multithreading_polyml.ML";
   63.82 +
   63.83 +if ML_System.name = "polyml-5.6"
   63.84 +then use "RAW/ml_stack_polyml-5.6.ML"
   63.85 +else use "RAW/ml_stack_dummy.ML";
   63.86 +
   63.87 +use "RAW/unsynchronized.ML";
   63.88 +val _ = PolyML.Compiler.forgetValue "ref";
   63.89 +val _ = PolyML.Compiler.forgetType "ref";
   63.90 +
   63.91 +
   63.92 +(* pervasive environment *)
   63.93 +
   63.94 +val _ = PolyML.Compiler.forgetValue "isSome";
   63.95 +val _ = PolyML.Compiler.forgetValue "getOpt";
   63.96 +val _ = PolyML.Compiler.forgetValue "valOf";
   63.97 +val _ = PolyML.Compiler.forgetValue "foldl";
   63.98 +val _ = PolyML.Compiler.forgetValue "foldr";
   63.99 +val _ = PolyML.Compiler.forgetValue "print";
  63.100 +val _ = PolyML.Compiler.forgetValue "explode";
  63.101 +val _ = PolyML.Compiler.forgetValue "concat";
  63.102 +
  63.103 +val ord = SML90.ord;
  63.104 +val chr = SML90.chr;
  63.105 +val raw_explode = SML90.explode;
  63.106 +val implode = SML90.implode;
  63.107 +
  63.108 +val io_buffer_size = 4096;
  63.109 +
  63.110 +fun quit () = exit 0;
  63.111 +
  63.112 +
  63.113 +(* ML runtime system *)
  63.114 +
  63.115 +if ML_System.name = "polyml-5.6"
  63.116 +then use "RAW/ml_profiling_polyml-5.6.ML"
  63.117 +else use "RAW/ml_profiling_polyml.ML";
  63.118 +
  63.119 +val pointer_eq = PolyML.pointerEq;
  63.120 +
  63.121 +
  63.122 +(* ML toplevel pretty printing *)
  63.123 +
  63.124 +use "RAW/ml_pretty.ML";
  63.125 +
  63.126 +local
  63.127 +  val depth = Unsynchronized.ref 10;
  63.128 +in
  63.129 +  fun get_default_print_depth () = ! depth;
  63.130 +  fun default_print_depth n = (depth := n; PolyML.print_depth n);
  63.131 +  val _ = default_print_depth 10;
  63.132 +end;
  63.133 +
  63.134 +val error_depth = PolyML.error_depth;
  63.135 +
  63.136 +val pretty_ml =
  63.137 +  let
  63.138 +    fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
  63.139 +      | convert _ (PolyML.PrettyBlock (_, _,
  63.140 +            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
  63.141 +          ML_Pretty.Break (true, 1, 0)
  63.142 +      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
  63.143 +          let
  63.144 +            fun property name default =
  63.145 +              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
  63.146 +                SOME (PolyML.ContextProperty (_, b)) => b
  63.147 +              | _ => default);
  63.148 +            val bg = property "begin" "";
  63.149 +            val en = property "end" "";
  63.150 +            val len' = property "length" len;
  63.151 +          in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
  63.152 +      | convert len (PolyML.PrettyString s) =
  63.153 +          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
  63.154 +  in convert "" end;
  63.155 +
  63.156 +fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
  63.157 +  | ml_pretty (ML_Pretty.Break (true, _, _)) =
  63.158 +      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
  63.159 +        [PolyML.PrettyString " "])
  63.160 +  | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
  63.161 +      let val context =
  63.162 +        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
  63.163 +        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
  63.164 +      in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
  63.165 +  | ml_pretty (ML_Pretty.String (s, len)) =
  63.166 +      if len = size s then PolyML.PrettyString s
  63.167 +      else PolyML.PrettyBlock
  63.168 +        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
  63.169 +
  63.170 +
  63.171 +(* ML compiler *)
  63.172 +
  63.173 +structure ML_Name_Space =
  63.174 +struct
  63.175 +  open ML_Name_Space;
  63.176 +  val display_val = pretty_ml o displayVal;
  63.177 +end;
  63.178 +
  63.179 +use "RAW/ml_compiler_parameters.ML";
  63.180 +if ML_System.name = "polyml-5.6"
  63.181 +then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
  63.182 +
  63.183 +use "RAW/use_context.ML";
  63.184 +use "RAW/ml_positions.ML";
  63.185 +use "RAW/compiler_polyml.ML";
  63.186 +
  63.187 +PolyML.Compiler.reportUnreferencedIds := true;
  63.188 +PolyML.Compiler.printInAlphabeticalOrder := false;
  63.189 +PolyML.Compiler.maxInlineSize := 80;
  63.190 +
  63.191 +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
  63.192 +
  63.193 +use "RAW/ml_parse_tree.ML";
  63.194 +if ML_System.name = "polyml-5.6"
  63.195 +then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
  63.196 +
  63.197 +fun toplevel_pp context (_: string list) pp =
  63.198 +  use_text context {line = 1, file = "pp", verbose = false, debug = false}
  63.199 +    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
  63.200 +
  63.201 +fun ml_make_string struct_name =
  63.202 +  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
  63.203 +    struct_name ^ ".ML_print_depth ())))))";
  63.204 +
  63.205 +
  63.206 +(* ML debugger *)
  63.207 +
  63.208 +if ML_System.name = "polyml-5.6"
  63.209 +then use "RAW/ml_debugger_polyml-5.6.ML"
  63.210 +else use "RAW/ml_debugger.ML";
    64.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    64.2 +++ b/src/Pure/RAW/pp_dummy.ML	Wed Dec 23 23:09:13 2015 +0100
    64.3 @@ -0,0 +1,16 @@
    64.4 +(*  Title:      Pure/RAW/pp_dummy.ML
    64.5 +
    64.6 +Dummy setup for toplevel pretty printing.
    64.7 +*)
    64.8 +
    64.9 +fun ml_pretty _ = raise Fail "ml_pretty dummy";
   64.10 +fun pretty_ml _ = raise Fail "pretty_ml dummy";
   64.11 +
   64.12 +structure PolyML =
   64.13 +struct
   64.14 +  fun addPrettyPrinter _ = ();
   64.15 +  fun prettyRepresentation _ =
   64.16 +    raise Fail "PolyML.prettyRepresentation dummy";
   64.17 +  open PolyML;
   64.18 +end;
   64.19 +
    65.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    65.2 +++ b/src/Pure/RAW/proper_int.ML	Wed Dec 23 23:09:13 2015 +0100
    65.3 @@ -0,0 +1,289 @@
    65.4 +(*  Title:      Pure/RAW/proper_int.ML
    65.5 +    Author:     Makarius
    65.6 +
    65.7 +SML basis with type int representing proper integers, not machine
    65.8 +words.
    65.9 +*)
   65.10 +
   65.11 +val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
   65.12 +val dest_int = IntInf.toInt: IntInf.int -> Int.int;
   65.13 +
   65.14 +
   65.15 +(* Int *)
   65.16 +
   65.17 +type int = IntInf.int;
   65.18 +
   65.19 +structure IntInf =
   65.20 +struct
   65.21 +  open IntInf;
   65.22 +  fun fromInt (a: int) = a;
   65.23 +  fun toInt (a: int) = a;
   65.24 +  val log2 = mk_int o IntInf.log2;
   65.25 +  val sign = mk_int o IntInf.sign;
   65.26 +end;
   65.27 +
   65.28 +structure Int = IntInf;
   65.29 +
   65.30 +
   65.31 +(* List *)
   65.32 +
   65.33 +structure List =
   65.34 +struct
   65.35 +  open List;
   65.36 +  fun length a = mk_int (List.length a);
   65.37 +  fun nth (a, b) = List.nth (a, dest_int b);
   65.38 +  fun take (a, b) = List.take (a, dest_int b);
   65.39 +  fun drop (a, b) = List.drop (a, dest_int b);
   65.40 +  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
   65.41 +end;
   65.42 +
   65.43 +val length = List.length;
   65.44 +
   65.45 +
   65.46 +(* Array *)
   65.47 +
   65.48 +structure Array =
   65.49 +struct
   65.50 +  open Array;
   65.51 +  val maxLen = mk_int Array.maxLen;
   65.52 +  fun array (a, b) = Array.array (dest_int a, b);
   65.53 +  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
   65.54 +  fun length a = mk_int (Array.length a);
   65.55 +  fun sub (a, b) = Array.sub (a, dest_int b);
   65.56 +  fun update (a, b, c) = Array.update (a, dest_int b, c);
   65.57 +  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
   65.58 +  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
   65.59 +  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
   65.60 +  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
   65.61 +  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   65.62 +  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   65.63 +  fun findi a b =
   65.64 +    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
   65.65 +      NONE => NONE
   65.66 +    | SOME (c, d) => SOME (mk_int c, d));
   65.67 +end;
   65.68 +
   65.69 +
   65.70 +(* Vector *)
   65.71 +
   65.72 +structure Vector =
   65.73 +struct
   65.74 +  open Vector;
   65.75 +  val maxLen = mk_int Vector.maxLen;
   65.76 +  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
   65.77 +  fun length a = mk_int (Vector.length a);
   65.78 +  fun sub (a, b) = Vector.sub (a, dest_int b);
   65.79 +  fun update (a, b, c) = Vector.update (a, dest_int b, c);
   65.80 +  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
   65.81 +  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
   65.82 +  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
   65.83 +  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
   65.84 +  fun findi a b =
   65.85 +    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
   65.86 +      NONE => NONE
   65.87 +    | SOME (c, d) => SOME (mk_int c, d));
   65.88 +end;
   65.89 +
   65.90 +
   65.91 +(* CharVector *)
   65.92 +
   65.93 +structure CharVector =
   65.94 +struct
   65.95 +  open CharVector;
   65.96 +  fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
   65.97 +end;
   65.98 +
   65.99 +
  65.100 +(* Word8VectorSlice *)
  65.101 +
  65.102 +structure Word8VectorSlice =
  65.103 +struct
  65.104 +  open Word8VectorSlice;
  65.105 +  val length = mk_int o Word8VectorSlice.length;
  65.106 +  fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
  65.107 +end;
  65.108 +
  65.109 +
  65.110 +(* Char *)
  65.111 +
  65.112 +structure Char =
  65.113 +struct
  65.114 +  open Char;
  65.115 +  val maxOrd = mk_int Char.maxOrd;
  65.116 +  val chr = Char.chr o dest_int;
  65.117 +  val ord = mk_int o Char.ord;
  65.118 +end;
  65.119 +
  65.120 +val chr = Char.chr;
  65.121 +val ord = Char.ord;
  65.122 +
  65.123 +
  65.124 +(* String *)
  65.125 +
  65.126 +structure String =
  65.127 +struct
  65.128 +  open String;
  65.129 +  val maxSize = mk_int String.maxSize;
  65.130 +  val size = mk_int o String.size;
  65.131 +  fun sub (a, b) = String.sub (a, dest_int b);
  65.132 +  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
  65.133 +  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
  65.134 +end;
  65.135 +
  65.136 +val size = String.size;
  65.137 +val substring = String.substring;
  65.138 +
  65.139 +
  65.140 +(* Substring *)
  65.141 +
  65.142 +structure Substring =
  65.143 +struct
  65.144 +  open Substring;
  65.145 +  fun sub (a, b) = Substring.sub (a, dest_int b);
  65.146 +  val size = mk_int o Substring.size;
  65.147 +  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
  65.148 +  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
  65.149 +  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
  65.150 +  fun triml a b = Substring.triml (dest_int a) b;
  65.151 +  fun trimr a b = Substring.trimr (dest_int a) b;
  65.152 +  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
  65.153 +  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
  65.154 +end;
  65.155 +
  65.156 +
  65.157 +(* StringCvt *)
  65.158 +
  65.159 +structure StringCvt =
  65.160 +struct
  65.161 +  open StringCvt;
  65.162 +  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
  65.163 +  fun realfmt fmt = Real.fmt
  65.164 +    (case fmt of
  65.165 +      EXACT => StringCvt.EXACT
  65.166 +    | FIX NONE => StringCvt.FIX NONE
  65.167 +    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
  65.168 +    | GEN NONE => StringCvt.GEN NONE
  65.169 +    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
  65.170 +    | SCI NONE => StringCvt.SCI NONE
  65.171 +    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
  65.172 +  fun padRight a b c = StringCvt.padRight a (dest_int b) c;
  65.173 +  fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
  65.174 +end;
  65.175 +
  65.176 +
  65.177 +(* Word *)
  65.178 +
  65.179 +structure Word =
  65.180 +struct
  65.181 +  open Word;
  65.182 +  val wordSize = mk_int Word.wordSize;
  65.183 +  val toInt = Word.toLargeInt;
  65.184 +  val toIntX = Word.toLargeIntX;
  65.185 +  val fromInt = Word.fromLargeInt;
  65.186 +end;
  65.187 +
  65.188 +structure Word8 =
  65.189 +struct
  65.190 +  open Word8;
  65.191 +  val wordSize = mk_int Word8.wordSize;
  65.192 +  val toInt = Word8.toLargeInt;
  65.193 +  val toIntX = Word8.toLargeIntX;
  65.194 +  val fromInt = Word8.fromLargeInt;
  65.195 +end;
  65.196 +
  65.197 +structure Word32 =
  65.198 +struct
  65.199 +  open Word32;
  65.200 +  val wordSize = mk_int Word32.wordSize;
  65.201 +  val toInt = Word32.toLargeInt;
  65.202 +  val toIntX = Word32.toLargeIntX;
  65.203 +  val fromInt = Word32.fromLargeInt;
  65.204 +end;
  65.205 +
  65.206 +structure LargeWord =
  65.207 +struct
  65.208 +  open LargeWord;
  65.209 +  val wordSize = mk_int LargeWord.wordSize;
  65.210 +  val toInt = LargeWord.toLargeInt;
  65.211 +  val toIntX = LargeWord.toLargeIntX;
  65.212 +  val fromInt = LargeWord.fromLargeInt;
  65.213 +end;
  65.214 +
  65.215 +
  65.216 +(* Real *)
  65.217 +
  65.218 +structure Real =
  65.219 +struct
  65.220 +  open Real;
  65.221 +  val radix = mk_int Real.radix;
  65.222 +  val precision = mk_int Real.precision;
  65.223 +  fun sign a = mk_int (Real.sign a);
  65.224 +  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
  65.225 +  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
  65.226 +  val ceil = mk_int o Real.ceil;
  65.227 +  val floor = mk_int o Real.floor;
  65.228 +  val real = Real.fromInt o dest_int;
  65.229 +  val round = mk_int o Real.round;
  65.230 +  val trunc = mk_int o Real.trunc;
  65.231 +  fun toInt a b = mk_int (Real.toInt a b);
  65.232 +  fun fromInt a = Real.fromInt (dest_int a);
  65.233 +  val fmt = StringCvt.realfmt;
  65.234 +end;
  65.235 +
  65.236 +val ceil = Real.ceil;
  65.237 +val floor = Real.floor;
  65.238 +val real = Real.real;
  65.239 +val round = Real.round;
  65.240 +val trunc = Real.trunc;
  65.241 +
  65.242 +
  65.243 +(* TextIO *)
  65.244 +
  65.245 +structure TextIO =
  65.246 +struct
  65.247 +  open TextIO;
  65.248 +  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
  65.249 +  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
  65.250 +end;
  65.251 +
  65.252 +
  65.253 +(* BinIO *)
  65.254 +
  65.255 +structure BinIO =
  65.256 +struct
  65.257 +  open BinIO;
  65.258 +  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
  65.259 +  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
  65.260 +end;
  65.261 +
  65.262 +
  65.263 +(* Time *)
  65.264 +
  65.265 +structure Time =
  65.266 +struct
  65.267 +  open Time;
  65.268 +  fun fmt a b = Time.fmt (dest_int a) b;
  65.269 +end;
  65.270 +
  65.271 +
  65.272 +(* Sockets *)
  65.273 +
  65.274 +structure INetSock =
  65.275 +struct
  65.276 +  open INetSock;
  65.277 +  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
  65.278 +  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
  65.279 +end;
  65.280 +
  65.281 +
  65.282 +(* OS.FileSys *)
  65.283 +
  65.284 +structure OS =
  65.285 +struct
  65.286 +  open OS;
  65.287 +  structure FileSys =
  65.288 +  struct
  65.289 +    open FileSys;
  65.290 +    fun fileSize a = mk_int (FileSys.fileSize a);
  65.291 +  end;
  65.292 +end;
    66.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    66.2 +++ b/src/Pure/RAW/share_common_data_polyml-5.3.0.ML	Wed Dec 23 23:09:13 2015 +0100
    66.3 @@ -0,0 +1,11 @@
    66.4 +(*  Title:      Pure/RAW/share_common_data_polyml-5.3.0.ML
    66.5 +
    66.6 +Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
    66.7 +anymore.
    66.8 +*)
    66.9 +
   66.10 +structure PolyML =
   66.11 +struct
   66.12 +  open PolyML;
   66.13 +  fun shareCommonData _ = ();
   66.14 +end;
    67.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    67.2 +++ b/src/Pure/RAW/single_assignment.ML	Wed Dec 23 23:09:13 2015 +0100
    67.3 @@ -0,0 +1,33 @@
    67.4 +(*  Title:      Pure/RAW/single_assignment.ML
    67.5 +    Author:     Makarius
    67.6 +
    67.7 +References with single assignment.  Unsynchronized!
    67.8 +*)
    67.9 +
   67.10 +signature SINGLE_ASSIGNMENT =
   67.11 +sig
   67.12 +  type 'a saref
   67.13 +  exception Locked
   67.14 +  val saref: unit -> 'a saref
   67.15 +  val savalue: 'a saref -> 'a option
   67.16 +  val saset: 'a saref * 'a -> unit
   67.17 +end;
   67.18 +
   67.19 +structure SingleAssignment: SINGLE_ASSIGNMENT =
   67.20 +struct
   67.21 +
   67.22 +exception Locked;
   67.23 +
   67.24 +abstype 'a saref = SARef of 'a option ref
   67.25 +with
   67.26 +
   67.27 +fun saref () = SARef (ref NONE);
   67.28 +
   67.29 +fun savalue (SARef r) = ! r;
   67.30 +
   67.31 +fun saset (SARef (r as ref NONE), x) = r := SOME x
   67.32 +  | saset _ = raise Locked;
   67.33 +
   67.34 +end;
   67.35 +
   67.36 +end;
    68.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    68.2 +++ b/src/Pure/RAW/single_assignment_polyml.ML	Wed Dec 23 23:09:13 2015 +0100
    68.3 @@ -0,0 +1,35 @@
    68.4 +(*  Title:      Pure/RAW/single_assignment_polyml.ML
    68.5 +    Author:     Makarius
    68.6 +
    68.7 +References with single assignment.  Unsynchronized!  Emulates
    68.8 +structure SingleAssignment from Poly/ML 5.4.
    68.9 +*)
   68.10 +
   68.11 +signature SINGLE_ASSIGNMENT =
   68.12 +sig
   68.13 +  type 'a saref
   68.14 +  exception Locked
   68.15 +  val saref: unit -> 'a saref
   68.16 +  val savalue: 'a saref -> 'a option
   68.17 +  val saset: 'a saref * 'a -> unit
   68.18 +end;
   68.19 +
   68.20 +structure SingleAssignment: SINGLE_ASSIGNMENT =
   68.21 +struct
   68.22 +
   68.23 +exception Locked;
   68.24 +
   68.25 +abstype 'a saref = SARef of 'a option ref
   68.26 +with
   68.27 +
   68.28 +fun saref () = SARef (ref NONE);
   68.29 +
   68.30 +fun savalue (SARef r) = ! r;
   68.31 +
   68.32 +fun saset (SARef (r as ref NONE), x) =
   68.33 +      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
   68.34 +  | saset _ = raise Locked;
   68.35 +
   68.36 +end;
   68.37 +
   68.38 +end;
    69.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    69.2 +++ b/src/Pure/RAW/smlnj.ML	Wed Dec 23 23:09:13 2015 +0100
    69.3 @@ -0,0 +1,194 @@
    69.4 +(*  Title:      Pure/RAW/smlnj.ML
    69.5 +
    69.6 +Compatibility file for Standard ML of New Jersey.
    69.7 +*)
    69.8 +
    69.9 +val io_buffer_size = 4096;
   69.10 +use "RAW/proper_int.ML";
   69.11 +
   69.12 +exception Interrupt;
   69.13 +fun reraise exn = raise exn;
   69.14 +
   69.15 +fun exit rc = Posix.Process.exit (Word8.fromInt rc);
   69.16 +fun quit () = exit 0;
   69.17 +
   69.18 +use "RAW/overloading_smlnj.ML";
   69.19 +use "RAW/exn.ML";
   69.20 +use "RAW/single_assignment.ML";
   69.21 +use "RAW/universal.ML";
   69.22 +use "RAW/thread_dummy.ML";
   69.23 +use "RAW/multithreading.ML";
   69.24 +use "RAW/ml_stack_dummy.ML";
   69.25 +use "RAW/ml_pretty.ML";
   69.26 +use "RAW/ml_name_space.ML";
   69.27 +structure PolyML = struct end;
   69.28 +use "RAW/pp_dummy.ML";
   69.29 +use "RAW/use_context.ML";
   69.30 +use "RAW/ml_positions.ML";
   69.31 +
   69.32 +
   69.33 +val seconds = Time.fromReal;
   69.34 +
   69.35 +(*low-level pointer equality*)
   69.36 +CM.autoload "$smlnj/init/init.cmi";
   69.37 +val pointer_eq = InlineT.ptreql;
   69.38 +
   69.39 +
   69.40 +(* restore old-style character / string functions *)
   69.41 +
   69.42 +val ord = mk_int o SML90.ord;
   69.43 +val chr = SML90.chr o dest_int;
   69.44 +val raw_explode = SML90.explode;
   69.45 +val implode = SML90.implode;
   69.46 +
   69.47 +
   69.48 +(* New Jersey ML parameters *)
   69.49 +
   69.50 +val _ =
   69.51 + (Control.Print.printLength := 1000;
   69.52 +  Control.Print.printDepth := 350;
   69.53 +  Control.Print.stringDepth := 250;
   69.54 +  Control.Print.signatures := 2;
   69.55 +  Control.MC.matchRedundantError := false);
   69.56 +
   69.57 +
   69.58 +(* Poly/ML emulation *)
   69.59 +
   69.60 +(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
   69.61 +local
   69.62 +  val depth = ref (10: int);
   69.63 +in
   69.64 +  fun get_default_print_depth () = ! depth;
   69.65 +  fun default_print_depth n =
   69.66 +   (depth := n;
   69.67 +    Control.Print.printDepth := dest_int n div 2;
   69.68 +    Control.Print.printLength := dest_int n);
   69.69 +  val _ = default_print_depth 10;
   69.70 +end;
   69.71 +
   69.72 +fun ml_make_string (_: string) = "(fn _ => \"?\")";
   69.73 +
   69.74 +
   69.75 +(*prompts*)
   69.76 +fun ml_prompts p1 p2 =
   69.77 +  (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
   69.78 +
   69.79 +(*dummy implementation*)
   69.80 +structure ML_Profiling =
   69.81 +struct
   69.82 +  fun profile_time (_: (int * string) list -> unit) f x = f x;
   69.83 +  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
   69.84 +  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
   69.85 +end;
   69.86 +
   69.87 +(*dummy implementation*)
   69.88 +fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
   69.89 +
   69.90 +
   69.91 +(* ML command execution *)
   69.92 +
   69.93 +fun use_text ({tune_source, print, error, ...}: use_context)
   69.94 +    {line, file, verbose, debug = _: bool} text =
   69.95 +  let
   69.96 +    val ref out_orig = Control.Print.out;
   69.97 +
   69.98 +    val out_buffer = ref ([]: string list);
   69.99 +    val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
  69.100 +    fun output () =
  69.101 +      let val str = implode (rev (! out_buffer))
  69.102 +      in String.substring (str, 0, Int.max (0, size str - 1)) end;
  69.103 +  in
  69.104 +    Control.Print.out := out;
  69.105 +    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
  69.106 +      handle exn =>
  69.107 +        (Control.Print.out := out_orig;
  69.108 +          error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
  69.109 +    Control.Print.out := out_orig;
  69.110 +    if verbose then print (output ()) else ()
  69.111 +  end;
  69.112 +
  69.113 +fun use_file context {verbose, debug} file =
  69.114 +  let
  69.115 +    val instream = TextIO.openIn file;
  69.116 +    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
  69.117 +  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
  69.118 +
  69.119 +
  69.120 +(* toplevel pretty printing *)
  69.121 +
  69.122 +fun ml_pprint pps =
  69.123 +  let
  69.124 +    fun str "" = ()
  69.125 +      | str s = PrettyPrint.string pps s;
  69.126 +    fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
  69.127 +         (str bg;
  69.128 +          (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
  69.129 +            (PrettyPrint.Rel (dest_int ind));
  69.130 +          List.app pprint prts; PrettyPrint.closeBox pps;
  69.131 +          str en)
  69.132 +      | pprint (ML_Pretty.String (s, _)) = str s
  69.133 +      | pprint (ML_Pretty.Break (false, width, offset)) =
  69.134 +          PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
  69.135 +      | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
  69.136 +  in pprint end;
  69.137 +
  69.138 +fun toplevel_pp context path pp =
  69.139 +  use_text context {line = 1, file = "pp", verbose = false, debug = false}
  69.140 +    ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
  69.141 +      "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
  69.142 +
  69.143 +
  69.144 +
  69.145 +(** interrupts **)
  69.146 +
  69.147 +local
  69.148 +
  69.149 +fun change_signal new_handler f x =
  69.150 +  let
  69.151 +    val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
  69.152 +    val result = Exn.capture (f old_handler) x;
  69.153 +    val _ = Signals.setHandler (Signals.sigINT, old_handler);
  69.154 +  in Exn.release result end;
  69.155 +
  69.156 +in
  69.157 +
  69.158 +fun interruptible (f: 'a -> 'b) x =
  69.159 +  let
  69.160 +    val result = ref (Exn.interrupt_exn: 'b Exn.result);
  69.161 +    val old_handler = Signals.inqHandler Signals.sigINT;
  69.162 +  in
  69.163 +    SMLofNJ.Cont.callcc (fn cont =>
  69.164 +      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
  69.165 +        result := Exn.capture f x));
  69.166 +    Signals.setHandler (Signals.sigINT, old_handler);
  69.167 +    Exn.release (! result)
  69.168 +  end;
  69.169 +
  69.170 +fun uninterruptible f =
  69.171 +  change_signal Signals.IGNORE
  69.172 +    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
  69.173 +
  69.174 +end;
  69.175 +
  69.176 +
  69.177 +use "RAW/unsynchronized.ML";
  69.178 +use "RAW/ml_debugger.ML";
  69.179 +
  69.180 +
  69.181 +(* ML system operations *)
  69.182 +
  69.183 +fun ml_platform_path (s: string) = s;
  69.184 +fun ml_standard_path (s: string) = s;
  69.185 +
  69.186 +use "RAW/ml_system.ML";
  69.187 +
  69.188 +structure ML_System =
  69.189 +struct
  69.190 +
  69.191 +open ML_System;
  69.192 +
  69.193 +fun save_state name =
  69.194 +  if SMLofNJ.exportML name then ()
  69.195 +  else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
  69.196 +
  69.197 +end;
    70.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    70.2 +++ b/src/Pure/RAW/thread_dummy.ML	Wed Dec 23 23:09:13 2015 +0100
    70.3 @@ -0,0 +1,82 @@
    70.4 +(*  Title:      Pure/RAW/thread_dummy.ML
    70.5 +    Author:     Makarius
    70.6 +
    70.7 +Default (mostly dummy) implementation of thread structures
    70.8 +(cf. polyml/basis/Thread.sml).
    70.9 +*)
   70.10 +
   70.11 +exception Thread of string;
   70.12 +
   70.13 +local fun fail _ = raise Thread "No multithreading support on this ML platform" in
   70.14 +
   70.15 +structure Mutex =
   70.16 +struct
   70.17 +  type mutex = unit;
   70.18 +  fun mutex _ = ();
   70.19 +  fun lock _ = fail ();
   70.20 +  fun unlock _ = fail ();
   70.21 +  fun trylock _ = fail ();
   70.22 +end;
   70.23 +
   70.24 +structure ConditionVar =
   70.25 +struct
   70.26 +  type conditionVar = unit;
   70.27 +  fun conditionVar _ = ();
   70.28 +  fun wait _ = fail ();
   70.29 +  fun waitUntil _ = fail ();
   70.30 +  fun signal _ = fail ();
   70.31 +  fun broadcast _ = fail ();
   70.32 +end;
   70.33 +
   70.34 +structure Thread =
   70.35 +struct
   70.36 +  type thread = unit;
   70.37 +
   70.38 +  datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
   70.39 +    and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
   70.40 +
   70.41 +  fun unavailable () = fail ();
   70.42 +
   70.43 +  fun fork _ = fail ();
   70.44 +  fun exit _ = fail ();
   70.45 +  fun isActive _ = fail ();
   70.46 +
   70.47 +  fun equal _ = fail ();
   70.48 +  fun self _ = fail ();
   70.49 +
   70.50 +  fun interrupt _ = fail ();
   70.51 +  fun broadcastInterrupt _ = fail ();
   70.52 +  fun testInterrupt _ = fail ();
   70.53 +
   70.54 +  fun kill _ = fail ();
   70.55 +
   70.56 +  fun setAttributes _ = fail ();
   70.57 +  fun getAttributes _ = fail ();
   70.58 +
   70.59 +  fun numProcessors _ = fail ();
   70.60 +
   70.61 +
   70.62 +(* thread data *)
   70.63 +
   70.64 +local
   70.65 +
   70.66 +val data = ref ([]: Universal.universal  ref list);
   70.67 +
   70.68 +fun find_data tag =
   70.69 +  let
   70.70 +    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
   70.71 +      | find [] = NONE;
   70.72 +  in find (! data) end;
   70.73 +
   70.74 +in
   70.75 +
   70.76 +fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
   70.77 +
   70.78 +fun setLocal (tag, x) =
   70.79 +  (case find_data tag of
   70.80 +    SOME r => r := Universal.tagInject tag x
   70.81 +  | NONE => data :=  ref (Universal.tagInject tag x) :: ! data);
   70.82 +
   70.83 +end;
   70.84 +end;
   70.85 +end;
    71.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    71.2 +++ b/src/Pure/RAW/universal.ML	Wed Dec 23 23:09:13 2015 +0100
    71.3 @@ -0,0 +1,41 @@
    71.4 +(*  Title:      Pure/RAW/universal.ML
    71.5 +    Author:     Makarius
    71.6 +
    71.7 +Universal values via tagged union.  Emulates structure Universal
    71.8 +from Poly/ML 5.1.
    71.9 +*)
   71.10 +
   71.11 +signature UNIVERSAL =
   71.12 +sig
   71.13 +  type universal
   71.14 +  type 'a tag
   71.15 +  val tag: unit -> 'a tag
   71.16 +  val tagIs: 'a tag -> universal -> bool
   71.17 +  val tagInject: 'a tag -> 'a -> universal
   71.18 +  val tagProject: 'a tag -> universal -> 'a
   71.19 +end;
   71.20 +
   71.21 +structure Universal: UNIVERSAL =
   71.22 +struct
   71.23 +
   71.24 +type universal = exn;
   71.25 +
   71.26 +datatype 'a tag = Tag of
   71.27 + {is: universal -> bool,
   71.28 +  inject: 'a -> universal,
   71.29 +  project: universal -> 'a};
   71.30 +
   71.31 +fun tag () =
   71.32 +  let exception Universal of 'a in
   71.33 +   Tag {
   71.34 +    is = fn Universal _ => true | _ => false,
   71.35 +    inject = Universal,
   71.36 +    project = fn Universal x => x}
   71.37 +  end;
   71.38 +
   71.39 +fun tagIs (Tag {is, ...}) = is;
   71.40 +fun tagInject (Tag {inject, ...}) = inject;
   71.41 +fun tagProject (Tag {project, ...}) = project;
   71.42 +
   71.43 +end;
   71.44 +
    72.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    72.2 +++ b/src/Pure/RAW/unsynchronized.ML	Wed Dec 23 23:09:13 2015 +0100
    72.3 @@ -0,0 +1,30 @@
    72.4 +(*  Title:      Pure/RAW/unsynchronized.ML
    72.5 +    Author:     Makarius
    72.6 +
    72.7 +Raw ML references as unsynchronized state variables.
    72.8 +*)
    72.9 +
   72.10 +structure Unsynchronized =
   72.11 +struct
   72.12 +
   72.13 +datatype ref = datatype ref;
   72.14 +
   72.15 +val op := = op :=;
   72.16 +val ! = !;
   72.17 +
   72.18 +fun change r f = r := f (! r);
   72.19 +fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
   72.20 +
   72.21 +fun inc i = (i := ! i + (1: int); ! i);
   72.22 +fun dec i = (i := ! i - (1: int); ! i);
   72.23 +
   72.24 +fun setmp flag value f x =
   72.25 +  uninterruptible (fn restore_attributes => fn () =>
   72.26 +    let
   72.27 +      val orig_value = ! flag;
   72.28 +      val _ = flag := value;
   72.29 +      val result = Exn.capture (restore_attributes f) x;
   72.30 +      val _ = flag := orig_value;
   72.31 +    in Exn.release result end) ();
   72.32 +
   72.33 +end;
    73.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    73.2 +++ b/src/Pure/RAW/use_context.ML	Wed Dec 23 23:09:13 2015 +0100
    73.3 @@ -0,0 +1,13 @@
    73.4 +(*  Title:      Pure/RAW/use_context.ML
    73.5 +    Author:     Makarius
    73.6 +
    73.7 +Common context for "use" operations (compiler invocation).
    73.8 +*)
    73.9 +
   73.10 +type use_context =
   73.11 + {tune_source: string -> string,
   73.12 +  name_space: ML_Name_Space.T,
   73.13 +  str_of_pos: int -> string -> string,
   73.14 +  print: string -> unit,
   73.15 +  error: string -> unit};
   73.16 +
    74.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    74.2 +++ b/src/Pure/RAW/windows_path.ML	Wed Dec 23 23:09:13 2015 +0100
    74.3 @@ -0,0 +1,34 @@
    74.4 +(*  Title:      Pure/RAW/windows_path.ML
    74.5 +    Author:     Makarius
    74.6 +
    74.7 +Windows file-system paths.
    74.8 +*)
    74.9 +
   74.10 +fun ml_platform_path path =
   74.11 +  if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
   74.12 +    (case String.tokens (fn c => c = #"/") path of
   74.13 +      "cygdrive" :: drive :: arcs =>
   74.14 +        let
   74.15 +          val vol =
   74.16 +            (case Char.fromString drive of
   74.17 +              NONE => drive ^ ":"
   74.18 +            | SOME d => String.str (Char.toUpper d) ^ ":");
   74.19 +        in String.concatWith "\\" (vol :: arcs) end
   74.20 +    | arcs =>
   74.21 +        (case OS.Process.getEnv "CYGWIN_ROOT" of
   74.22 +          SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
   74.23 +        | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
   74.24 +  else String.translate (fn #"/" => "\\" | c => String.str c) path;
   74.25 +
   74.26 +fun ml_standard_path path =
   74.27 +  let
   74.28 +    val {vol, arcs, isAbs} = OS.Path.fromString path;
   74.29 +    val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
   74.30 +  in
   74.31 +    if isAbs then
   74.32 +      (case String.explode vol of
   74.33 +        [d, #":"] =>
   74.34 +          String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
   74.35 +      | _ => path')
   74.36 +    else path'
   74.37 +  end;
    75.1 --- a/src/Pure/ROOT	Wed Dec 23 21:15:26 2015 +0100
    75.2 +++ b/src/Pure/ROOT	Wed Dec 23 23:09:13 2015 +0100
    75.3 @@ -3,83 +3,83 @@
    75.4  session RAW =
    75.5    theories
    75.6    files
    75.7 -    "General/exn.ML"
    75.8 -    "ML-Systems/compiler_polyml.ML"
    75.9 -    "ML-Systems/exn_trace_polyml-5.5.1.ML"
   75.10 -    "ML-Systems/ml_compiler_parameters.ML"
   75.11 -    "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
   75.12 -    "ML-Systems/ml_debugger.ML"
   75.13 -    "ML-Systems/ml_debugger_polyml-5.6.ML"
   75.14 -    "ML-Systems/ml_name_space.ML"
   75.15 -    "ML-Systems/ml_name_space_polyml-5.6.ML"
   75.16 -    "ML-Systems/ml_name_space_polyml.ML"
   75.17 -    "ML-Systems/ml_parse_tree.ML"
   75.18 -    "ML-Systems/ml_parse_tree_polyml-5.6.ML"
   75.19 -    "ML-Systems/ml_positions.ML"
   75.20 -    "ML-Systems/ml_pretty.ML"
   75.21 -    "ML-Systems/ml_profiling_polyml-5.6.ML"
   75.22 -    "ML-Systems/ml_profiling_polyml.ML"
   75.23 -    "ML-Systems/ml_stack_dummy.ML"
   75.24 -    "ML-Systems/ml_stack_polyml-5.6.ML"
   75.25 -    "ML-Systems/ml_system.ML"
   75.26 -    "ML-Systems/multithreading.ML"
   75.27 -    "ML-Systems/multithreading_polyml.ML"
   75.28 -    "ML-Systems/overloading_smlnj.ML"
   75.29 -    "ML-Systems/polyml-5.5.2.ML"
   75.30 -    "ML-Systems/polyml-5.6.ML"
   75.31 -    "ML-Systems/polyml-5.6.ML"
   75.32 -    "ML-Systems/polyml.ML"
   75.33 -    "ML-Systems/pp_dummy.ML"
   75.34 -    "ML-Systems/proper_int.ML"
   75.35 -    "ML-Systems/share_common_data_polyml-5.3.0.ML"
   75.36 -    "ML-Systems/single_assignment.ML"
   75.37 -    "ML-Systems/single_assignment_polyml.ML"
   75.38 -    "ML-Systems/smlnj.ML"
   75.39 -    "ML-Systems/thread_dummy.ML"
   75.40 -    "ML-Systems/universal.ML"
   75.41 -    "ML-Systems/unsynchronized.ML"
   75.42 -    "ML-Systems/use_context.ML"
   75.43 -    "ML-Systems/windows_path.ML"
   75.44 +    "RAW/compiler_polyml.ML"
   75.45 +    "RAW/exn.ML"
   75.46 +    "RAW/exn_trace_polyml-5.5.1.ML"
   75.47 +    "RAW/ml_compiler_parameters.ML"
   75.48 +    "RAW/ml_compiler_parameters_polyml-5.6.ML"
   75.49 +    "RAW/ml_debugger.ML"
   75.50 +    "RAW/ml_debugger_polyml-5.6.ML"
   75.51 +    "RAW/ml_name_space.ML"
   75.52 +    "RAW/ml_name_space_polyml-5.6.ML"
   75.53 +    "RAW/ml_name_space_polyml.ML"
   75.54 +    "RAW/ml_parse_tree.ML"
   75.55 +    "RAW/ml_parse_tree_polyml-5.6.ML"
   75.56 +    "RAW/ml_positions.ML"
   75.57 +    "RAW/ml_pretty.ML"
   75.58 +    "RAW/ml_profiling_polyml-5.6.ML"
   75.59 +    "RAW/ml_profiling_polyml.ML"
   75.60 +    "RAW/ml_stack_dummy.ML"
   75.61 +    "RAW/ml_stack_polyml-5.6.ML"
   75.62 +    "RAW/ml_system.ML"
   75.63 +    "RAW/multithreading.ML"
   75.64 +    "RAW/multithreading_polyml.ML"
   75.65 +    "RAW/overloading_smlnj.ML"
   75.66 +    "RAW/polyml-5.5.2.ML"
   75.67 +    "RAW/polyml-5.6.ML"
   75.68 +    "RAW/polyml-5.6.ML"
   75.69 +    "RAW/polyml.ML"
   75.70 +    "RAW/pp_dummy.ML"
   75.71 +    "RAW/proper_int.ML"
   75.72 +    "RAW/share_common_data_polyml-5.3.0.ML"
   75.73 +    "RAW/single_assignment.ML"
   75.74 +    "RAW/single_assignment_polyml.ML"
   75.75 +    "RAW/smlnj.ML"
   75.76 +    "RAW/thread_dummy.ML"
   75.77 +    "RAW/universal.ML"
   75.78 +    "RAW/unsynchronized.ML"
   75.79 +    "RAW/use_context.ML"
   75.80 +    "RAW/windows_path.ML"
   75.81  
   75.82  session Pure =
   75.83    global_theories Pure
   75.84    files
   75.85 -    "General/exn.ML"
   75.86 -    "ML-Systems/compiler_polyml.ML"
   75.87 -    "ML-Systems/exn_trace_polyml-5.5.1.ML"
   75.88 -    "ML-Systems/ml_compiler_parameters.ML"
   75.89 -    "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
   75.90 -    "ML-Systems/ml_debugger.ML"
   75.91 -    "ML-Systems/ml_debugger_polyml-5.6.ML"
   75.92 -    "ML-Systems/ml_name_space.ML"
   75.93 -    "ML-Systems/ml_name_space_polyml-5.6.ML"
   75.94 -    "ML-Systems/ml_name_space_polyml.ML"
   75.95 -    "ML-Systems/ml_parse_tree.ML"
   75.96 -    "ML-Systems/ml_parse_tree_polyml-5.6.ML"
   75.97 -    "ML-Systems/ml_positions.ML"
   75.98 -    "ML-Systems/ml_pretty.ML"
   75.99 -    "ML-Systems/ml_profiling_polyml-5.6.ML"
  75.100 -    "ML-Systems/ml_profiling_polyml.ML"
  75.101 -    "ML-Systems/ml_stack_dummy.ML"
  75.102 -    "ML-Systems/ml_stack_polyml-5.6.ML"
  75.103 -    "ML-Systems/ml_system.ML"
  75.104 -    "ML-Systems/multithreading.ML"
  75.105 -    "ML-Systems/multithreading_polyml.ML"
  75.106 -    "ML-Systems/overloading_smlnj.ML"
  75.107 -    "ML-Systems/polyml-5.5.2.ML"
  75.108 -    "ML-Systems/polyml-5.6.ML"
  75.109 -    "ML-Systems/polyml.ML"
  75.110 -    "ML-Systems/pp_dummy.ML"
  75.111 -    "ML-Systems/proper_int.ML"
  75.112 -    "ML-Systems/share_common_data_polyml-5.3.0.ML"
  75.113 -    "ML-Systems/single_assignment.ML"
  75.114 -    "ML-Systems/single_assignment_polyml.ML"
  75.115 -    "ML-Systems/smlnj.ML"
  75.116 -    "ML-Systems/thread_dummy.ML"
  75.117 -    "ML-Systems/universal.ML"
  75.118 -    "ML-Systems/unsynchronized.ML"
  75.119 -    "ML-Systems/use_context.ML"
  75.120 -    "ML-Systems/windows_path.ML"
  75.121 +    "RAW/compiler_polyml.ML"
  75.122 +    "RAW/exn.ML"
  75.123 +    "RAW/exn_trace_polyml-5.5.1.ML"
  75.124 +    "RAW/ml_compiler_parameters.ML"
  75.125 +    "RAW/ml_compiler_parameters_polyml-5.6.ML"
  75.126 +    "RAW/ml_debugger.ML"
  75.127 +    "RAW/ml_debugger_polyml-5.6.ML"
  75.128 +    "RAW/ml_name_space.ML"
  75.129 +    "RAW/ml_name_space_polyml-5.6.ML"
  75.130 +    "RAW/ml_name_space_polyml.ML"
  75.131 +    "RAW/ml_parse_tree.ML"
  75.132 +    "RAW/ml_parse_tree_polyml-5.6.ML"
  75.133 +    "RAW/ml_positions.ML"
  75.134 +    "RAW/ml_pretty.ML"
  75.135 +    "RAW/ml_profiling_polyml-5.6.ML"
  75.136 +    "RAW/ml_profiling_polyml.ML"
  75.137 +    "RAW/ml_stack_dummy.ML"
  75.138 +    "RAW/ml_stack_polyml-5.6.ML"
  75.139 +    "RAW/ml_system.ML"
  75.140 +    "RAW/multithreading.ML"
  75.141 +    "RAW/multithreading_polyml.ML"
  75.142 +    "RAW/overloading_smlnj.ML"
  75.143 +    "RAW/polyml-5.5.2.ML"
  75.144 +    "RAW/polyml-5.6.ML"
  75.145 +    "RAW/polyml.ML"
  75.146 +    "RAW/pp_dummy.ML"
  75.147 +    "RAW/proper_int.ML"
  75.148 +    "RAW/share_common_data_polyml-5.3.0.ML"
  75.149 +    "RAW/single_assignment.ML"
  75.150 +    "RAW/single_assignment_polyml.ML"
  75.151 +    "RAW/smlnj.ML"
  75.152 +    "RAW/thread_dummy.ML"
  75.153 +    "RAW/universal.ML"
  75.154 +    "RAW/unsynchronized.ML"
  75.155 +    "RAW/use_context.ML"
  75.156 +    "RAW/windows_path.ML"
  75.157  
  75.158      "Concurrent/bash.ML"
  75.159      "Concurrent/bash_sequential.ML"
    76.1 --- a/src/Pure/build	Wed Dec 23 21:15:26 2015 +0100
    76.2 +++ b/src/Pure/build	Wed Dec 23 23:09:13 2015 +0100
    76.3 @@ -49,8 +49,8 @@
    76.4  [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
    76.5  
    76.6  COMPAT=""
    76.7 -[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"
    76.8 -[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"
    76.9 +[ -f "RAW/${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/${ML_SYSTEM_BASE}.ML"
   76.10 +[ -f "RAW/${ML_SYSTEM}.ML" ] && COMPAT="RAW/${ML_SYSTEM}.ML"
   76.11  [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
   76.12  
   76.13  
    77.1 --- a/src/Pure/build-jars	Wed Dec 23 21:15:26 2015 +0100
    77.2 +++ b/src/Pure/build-jars	Wed Dec 23 23:09:13 2015 +0100
    77.3 @@ -28,7 +28,6 @@
    77.4    General/antiquote.scala
    77.5    General/bytes.scala
    77.6    General/completion.scala
    77.7 -  General/exn.scala
    77.8    General/file.scala
    77.9    General/graph.scala
   77.10    General/graph_display.scala
   77.11 @@ -72,9 +71,10 @@
   77.12    PIDE/text.scala
   77.13    PIDE/xml.scala
   77.14    PIDE/yxml.scala
   77.15 +  RAW/exn.scala
   77.16    ROOT.scala
   77.17 +  System/command_line.scala
   77.18    System/cygwin.scala
   77.19 -  System/command_line.scala
   77.20    System/invoke_scala.scala
   77.21    System/isabelle_charset.scala
   77.22    System/isabelle_process.scala