discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
authorwenzelm
Thu Mar 03 21:59:21 2016 +0100 (2016-03-03)
changeset 62508d0b68218ea55
parent 62507 15c36c181130
child 62509 13d6948e4b12
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
src/Pure/Concurrent/multithreading.ML
src/Pure/Concurrent/unsynchronized.ML
src/Pure/General/exn.ML
src/Pure/General/exn.scala
src/Pure/General/secure.ML
src/Pure/ML/fixed_int_dummy.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_debugger.ML
src/Pure/ML/ml_heap.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ML/ml_pretty.ML
src/Pure/ML/ml_profiling.ML
src/Pure/ML/ml_system.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/exn.ML
src/Pure/RAW/exn.scala
src/Pure/RAW/fixed_int_dummy.ML
src/Pure/RAW/ml_compiler0.ML
src/Pure/RAW/ml_debugger.ML
src/Pure/RAW/ml_heap.ML
src/Pure/RAW/ml_name_space.ML
src/Pure/RAW/ml_pretty.ML
src/Pure/RAW/ml_profiling.ML
src/Pure/RAW/ml_system.ML
src/Pure/RAW/multithreading.ML
src/Pure/RAW/secure.ML
src/Pure/RAW/unsynchronized.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/build.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/multithreading.ML	Thu Mar 03 21:59:21 2016 +0100
     1.3 @@ -0,0 +1,196 @@
     1.4 +(*  Title:      Pure/Concurrent/multithreading.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
     1.8 +*)
     1.9 +
    1.10 +signature BASIC_MULTITHREADING =
    1.11 +sig
    1.12 +  val interruptible: ('a -> 'b) -> 'a -> 'b
    1.13 +  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    1.14 +end;
    1.15 +
    1.16 +signature MULTITHREADING =
    1.17 +sig
    1.18 +  include BASIC_MULTITHREADING
    1.19 +  val no_interrupts: Thread.threadAttribute list
    1.20 +  val public_interrupts: Thread.threadAttribute list
    1.21 +  val private_interrupts: Thread.threadAttribute list
    1.22 +  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
    1.23 +  val interrupted: unit -> unit  (*exception Interrupt*)
    1.24 +  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    1.25 +  val max_threads_value: unit -> int
    1.26 +  val max_threads_update: int -> unit
    1.27 +  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
    1.28 +  val enabled: unit -> bool
    1.29 +  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
    1.30 +    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
    1.31 +  val trace: int ref
    1.32 +  val tracing: int -> (unit -> string) -> unit
    1.33 +  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
    1.34 +  val real_time: ('a -> unit) -> 'a -> Time.time
    1.35 +  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
    1.36 +  val serial: unit -> int
    1.37 +end;
    1.38 +
    1.39 +structure Multithreading: MULTITHREADING =
    1.40 +struct
    1.41 +
    1.42 +(* thread attributes *)
    1.43 +
    1.44 +val no_interrupts =
    1.45 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    1.46 +
    1.47 +val test_interrupts =
    1.48 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
    1.49 +
    1.50 +val public_interrupts =
    1.51 +  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    1.52 +
    1.53 +val private_interrupts =
    1.54 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
    1.55 +
    1.56 +val sync_interrupts = map
    1.57 +  (fn x as Thread.InterruptState Thread.InterruptDefer => x
    1.58 +    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
    1.59 +    | x => x);
    1.60 +
    1.61 +val safe_interrupts = map
    1.62 +  (fn Thread.InterruptState Thread.InterruptAsynch =>
    1.63 +      Thread.InterruptState Thread.InterruptAsynchOnce
    1.64 +    | x => x);
    1.65 +
    1.66 +fun interrupted () =
    1.67 +  let
    1.68 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
    1.69 +    val _ = Thread.setAttributes test_interrupts;
    1.70 +    val test = Exn.capture Thread.testInterrupt ();
    1.71 +    val _ = Thread.setAttributes orig_atts;
    1.72 +  in Exn.release test end;
    1.73 +
    1.74 +fun with_attributes new_atts e =
    1.75 +  let
    1.76 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
    1.77 +    val result = Exn.capture (fn () =>
    1.78 +      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
    1.79 +    val _ = Thread.setAttributes orig_atts;
    1.80 +  in Exn.release result end;
    1.81 +
    1.82 +
    1.83 +(* portable wrappers *)
    1.84 +
    1.85 +fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
    1.86 +
    1.87 +fun uninterruptible f x =
    1.88 +  with_attributes no_interrupts (fn atts =>
    1.89 +    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
    1.90 +
    1.91 +
    1.92 +(* options *)
    1.93 +
    1.94 +fun num_processors () =
    1.95 +  (case Thread.numPhysicalProcessors () of
    1.96 +    SOME n => n
    1.97 +  | NONE => Thread.numProcessors ());
    1.98 +
    1.99 +fun max_threads_result m =
   1.100 +  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
   1.101 +
   1.102 +val max_threads = ref 1;
   1.103 +
   1.104 +fun max_threads_value () = ! max_threads;
   1.105 +
   1.106 +fun max_threads_update m = max_threads := max_threads_result m;
   1.107 +
   1.108 +fun max_threads_setmp m f x =
   1.109 +  uninterruptible (fn restore_attributes => fn () =>
   1.110 +    let
   1.111 +      val max_threads_orig = ! max_threads;
   1.112 +      val _ = max_threads_update m;
   1.113 +      val result = Exn.capture (restore_attributes f) x;
   1.114 +      val _ = max_threads := max_threads_orig;
   1.115 +    in Exn.release result end) ();
   1.116 +
   1.117 +fun enabled () = max_threads_value () > 1;
   1.118 +
   1.119 +
   1.120 +(* synchronous wait *)
   1.121 +
   1.122 +fun sync_wait opt_atts time cond lock =
   1.123 +  with_attributes
   1.124 +    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
   1.125 +    (fn _ =>
   1.126 +      (case time of
   1.127 +        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
   1.128 +      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
   1.129 +      handle exn => Exn.Exn exn);
   1.130 +
   1.131 +
   1.132 +(* tracing *)
   1.133 +
   1.134 +val trace = ref 0;
   1.135 +
   1.136 +fun tracing level msg =
   1.137 +  if level > ! trace then ()
   1.138 +  else uninterruptible (fn _ => fn () =>
   1.139 +    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
   1.140 +      handle _ (*sic*) => ()) ();
   1.141 +
   1.142 +fun tracing_time detailed time =
   1.143 +  tracing
   1.144 +   (if not detailed then 5
   1.145 +    else if Time.>= (time, seconds 1.0) then 1
   1.146 +    else if Time.>= (time, seconds 0.1) then 2
   1.147 +    else if Time.>= (time, seconds 0.01) then 3
   1.148 +    else if Time.>= (time, seconds 0.001) then 4 else 5);
   1.149 +
   1.150 +fun real_time f x =
   1.151 +  let
   1.152 +    val timer = Timer.startRealTimer ();
   1.153 +    val () = f x;
   1.154 +    val time = Timer.checkRealTimer timer;
   1.155 +  in time end;
   1.156 +
   1.157 +
   1.158 +(* synchronized evaluation *)
   1.159 +
   1.160 +fun synchronized name lock e =
   1.161 +  Exn.release (uninterruptible (fn restore_attributes => fn () =>
   1.162 +    let
   1.163 +      val immediate =
   1.164 +        if Mutex.trylock lock then true
   1.165 +        else
   1.166 +          let
   1.167 +            val _ = tracing 5 (fn () => name ^ ": locking ...");
   1.168 +            val time = real_time Mutex.lock lock;
   1.169 +            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
   1.170 +          in false end;
   1.171 +      val result = Exn.capture (restore_attributes e) ();
   1.172 +      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
   1.173 +      val _ = Mutex.unlock lock;
   1.174 +    in result end) ());
   1.175 +
   1.176 +
   1.177 +(* serial numbers *)
   1.178 +
   1.179 +local
   1.180 +
   1.181 +val serial_lock = Mutex.mutex ();
   1.182 +val serial_count = ref 0;
   1.183 +
   1.184 +in
   1.185 +
   1.186 +val serial = uninterruptible (fn _ => fn () =>
   1.187 +  let
   1.188 +    val _ = Mutex.lock serial_lock;
   1.189 +    val _ = serial_count := ! serial_count + 1;
   1.190 +    val res = ! serial_count;
   1.191 +    val _ = Mutex.unlock serial_lock;
   1.192 +  in res end);
   1.193 +
   1.194 +end;
   1.195 +
   1.196 +end;
   1.197 +
   1.198 +structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
   1.199 +open Basic_Multithreading;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Concurrent/unsynchronized.ML	Thu Mar 03 21:59:21 2016 +0100
     2.3 @@ -0,0 +1,30 @@
     2.4 +(*  Title:      Pure/Concurrent/unsynchronized.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Raw ML references as unsynchronized state variables.
     2.8 +*)
     2.9 +
    2.10 +structure Unsynchronized =
    2.11 +struct
    2.12 +
    2.13 +datatype ref = datatype ref;
    2.14 +
    2.15 +val op := = op :=;
    2.16 +val ! = !;
    2.17 +
    2.18 +fun change r f = r := f (! r);
    2.19 +fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
    2.20 +
    2.21 +fun inc i = (i := ! i + (1: int); ! i);
    2.22 +fun dec i = (i := ! i - (1: int); ! i);
    2.23 +
    2.24 +fun setmp flag value f x =
    2.25 +  uninterruptible (fn restore_attributes => fn () =>
    2.26 +    let
    2.27 +      val orig_value = ! flag;
    2.28 +      val _ = flag := value;
    2.29 +      val result = Exn.capture (restore_attributes f) x;
    2.30 +      val _ = flag := orig_value;
    2.31 +    in Exn.release result end) ();
    2.32 +
    2.33 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/exn.ML	Thu Mar 03 21:59:21 2016 +0100
     3.3 @@ -0,0 +1,134 @@
     3.4 +(*  Title:      Pure/General/exn.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Support for exceptions.
     3.8 +*)
     3.9 +
    3.10 +signature BASIC_EXN =
    3.11 +sig
    3.12 +  exception ERROR of string
    3.13 +  val error: string -> 'a
    3.14 +  val cat_error: string -> string -> 'a
    3.15 +end;
    3.16 +
    3.17 +signature EXN =
    3.18 +sig
    3.19 +  include BASIC_EXN
    3.20 +  val reraise: exn -> 'a
    3.21 +  datatype 'a result = Res of 'a | Exn of exn
    3.22 +  val get_res: 'a result -> 'a option
    3.23 +  val get_exn: 'a result -> exn option
    3.24 +  val capture: ('a -> 'b) -> 'a -> 'b result
    3.25 +  val release: 'a result -> 'a
    3.26 +  val map_res: ('a -> 'b) -> 'a result -> 'b result
    3.27 +  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
    3.28 +  val map_exn: (exn -> exn) -> 'a result -> 'a result
    3.29 +  exception Interrupt
    3.30 +  val interrupt: unit -> 'a
    3.31 +  val is_interrupt: exn -> bool
    3.32 +  val interrupt_exn: 'a result
    3.33 +  val is_interrupt_exn: 'a result -> bool
    3.34 +  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
    3.35 +  val return_code: exn -> int -> int
    3.36 +  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
    3.37 +  exception EXCEPTIONS of exn list
    3.38 +  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
    3.39 +end;
    3.40 +
    3.41 +structure Exn: EXN =
    3.42 +struct
    3.43 +
    3.44 +(* reraise *)
    3.45 +
    3.46 +fun reraise exn =
    3.47 +  (case PolyML.exceptionLocation exn of
    3.48 +    NONE => raise exn
    3.49 +  | SOME location => PolyML.raiseWithLocation (exn, location));
    3.50 +
    3.51 +
    3.52 +(* user errors *)
    3.53 +
    3.54 +exception ERROR of string;
    3.55 +
    3.56 +fun error msg = raise ERROR msg;
    3.57 +
    3.58 +fun cat_error "" msg = error msg
    3.59 +  | cat_error msg "" = error msg
    3.60 +  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
    3.61 +
    3.62 +
    3.63 +(* exceptions as values *)
    3.64 +
    3.65 +datatype 'a result =
    3.66 +  Res of 'a |
    3.67 +  Exn of exn;
    3.68 +
    3.69 +fun get_res (Res x) = SOME x
    3.70 +  | get_res _ = NONE;
    3.71 +
    3.72 +fun get_exn (Exn exn) = SOME exn
    3.73 +  | get_exn _ = NONE;
    3.74 +
    3.75 +fun capture f x = Res (f x) handle e => Exn e;
    3.76 +
    3.77 +fun release (Res y) = y
    3.78 +  | release (Exn e) = reraise e;
    3.79 +
    3.80 +fun map_res f (Res x) = Res (f x)
    3.81 +  | map_res f (Exn e) = Exn e;
    3.82 +
    3.83 +fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
    3.84 +
    3.85 +fun map_exn f (Res x) = Res x
    3.86 +  | map_exn f (Exn e) = Exn (f e);
    3.87 +
    3.88 +
    3.89 +(* interrupts *)
    3.90 +
    3.91 +exception Interrupt = SML90.Interrupt;
    3.92 +
    3.93 +fun interrupt () = raise Interrupt;
    3.94 +
    3.95 +fun is_interrupt Interrupt = true
    3.96 +  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
    3.97 +  | is_interrupt _ = false;
    3.98 +
    3.99 +val interrupt_exn = Exn Interrupt;
   3.100 +
   3.101 +fun is_interrupt_exn (Exn exn) = is_interrupt exn
   3.102 +  | is_interrupt_exn _ = false;
   3.103 +
   3.104 +fun interruptible_capture f x =
   3.105 +  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
   3.106 +
   3.107 +
   3.108 +(* POSIX return code *)
   3.109 +
   3.110 +fun return_code exn rc =
   3.111 +  if is_interrupt exn then (130: int) else rc;
   3.112 +
   3.113 +fun capture_exit rc f x =
   3.114 +  f x handle exn => exit (return_code exn rc);
   3.115 +
   3.116 +
   3.117 +(* concatenated exceptions *)
   3.118 +
   3.119 +exception EXCEPTIONS of exn list;
   3.120 +
   3.121 +
   3.122 +(* low-level trace *)
   3.123 +
   3.124 +fun trace exn_message output e =
   3.125 +  PolyML.Exception.traceException
   3.126 +    (e, fn (trace, exn) =>
   3.127 +      let
   3.128 +        val title = "Exception trace - " ^ exn_message exn;
   3.129 +        val () = output (String.concatWith "\n" (title :: trace));
   3.130 +      in reraise exn end);
   3.131 +
   3.132 +end;
   3.133 +
   3.134 +datatype illegal = Interrupt;
   3.135 +
   3.136 +structure Basic_Exn: BASIC_EXN = Exn;
   3.137 +open Basic_Exn;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/General/exn.scala	Thu Mar 03 21:59:21 2016 +0100
     4.3 @@ -0,0 +1,137 @@
     4.4 +/*  Title:      Pure/General/exn.scala
     4.5 +    Module:     PIDE
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +Support for exceptions (arbitrary throwables).
     4.9 +*/
    4.10 +
    4.11 +package isabelle
    4.12 +
    4.13 +
    4.14 +object Exn
    4.15 +{
    4.16 +  /* user errors */
    4.17 +
    4.18 +  class User_Error(message: String) extends RuntimeException(message)
    4.19 +  {
    4.20 +    override def equals(that: Any): Boolean =
    4.21 +      that match {
    4.22 +        case other: User_Error => message == other.getMessage
    4.23 +        case _ => false
    4.24 +      }
    4.25 +    override def hashCode: Int = message.hashCode
    4.26 +
    4.27 +    override def toString: String = "ERROR(" + message + ")"
    4.28 +  }
    4.29 +
    4.30 +  object ERROR
    4.31 +  {
    4.32 +    def apply(message: String): User_Error = new User_Error(message)
    4.33 +    def unapply(exn: Throwable): Option[String] = user_message(exn)
    4.34 +  }
    4.35 +
    4.36 +  def error(message: String): Nothing = throw ERROR(message)
    4.37 +
    4.38 +  def cat_message(msg1: String, msg2: String): String =
    4.39 +    if (msg1 == "") msg2
    4.40 +    else if (msg2 == "") msg1
    4.41 +    else msg1 + "\n" + msg2
    4.42 +
    4.43 +  def cat_error(msg1: String, msg2: String): Nothing =
    4.44 +    error(cat_message(msg1, msg2))
    4.45 +
    4.46 +
    4.47 +  /* exceptions as values */
    4.48 +
    4.49 +  sealed abstract class Result[A]
    4.50 +  {
    4.51 +    def user_error: Result[A] =
    4.52 +      this match {
    4.53 +        case Exn(ERROR(msg)) => Exn(ERROR(msg))
    4.54 +        case _ => this
    4.55 +      }
    4.56 +  }
    4.57 +  case class Res[A](res: A) extends Result[A]
    4.58 +  case class Exn[A](exn: Throwable) extends Result[A]
    4.59 +
    4.60 +  def capture[A](e: => A): Result[A] =
    4.61 +    try { Res(e) }
    4.62 +    catch { case exn: Throwable => Exn[A](exn) }
    4.63 +
    4.64 +  def release[A](result: Result[A]): A =
    4.65 +    result match {
    4.66 +      case Res(x) => x
    4.67 +      case Exn(exn) => throw exn
    4.68 +    }
    4.69 +
    4.70 +  def release_first[A](results: List[Result[A]]): List[A] =
    4.71 +    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
    4.72 +      case Some(Exn(exn)) => throw exn
    4.73 +      case _ => results.map(release(_))
    4.74 +    }
    4.75 +
    4.76 +
    4.77 +  /* interrupts */
    4.78 +
    4.79 +  def is_interrupt(exn: Throwable): Boolean =
    4.80 +  {
    4.81 +    var found_interrupt = false
    4.82 +    var e = exn
    4.83 +    while (!found_interrupt && e != null) {
    4.84 +      found_interrupt |= e.isInstanceOf[InterruptedException]
    4.85 +      e = e.getCause
    4.86 +    }
    4.87 +    found_interrupt
    4.88 +  }
    4.89 +
    4.90 +  object Interrupt
    4.91 +  {
    4.92 +    def apply(): Throwable = new InterruptedException
    4.93 +    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
    4.94 +
    4.95 +    def expose() { if (Thread.interrupted) throw apply() }
    4.96 +    def impose() { Thread.currentThread.interrupt }
    4.97 +
    4.98 +    def postpone[A](body: => A): Option[A] =
    4.99 +    {
   4.100 +      val interrupted = Thread.interrupted
   4.101 +      val result = capture { body }
   4.102 +      if (interrupted) impose()
   4.103 +      result match {
   4.104 +        case Res(x) => Some(x)
   4.105 +        case Exn(e) =>
   4.106 +          if (is_interrupt(e)) { impose(); None }
   4.107 +          else throw e
   4.108 +      }
   4.109 +    }
   4.110 +
   4.111 +    val return_code = 130
   4.112 +  }
   4.113 +
   4.114 +
   4.115 +  /* POSIX return code */
   4.116 +
   4.117 +  def return_code(exn: Throwable, rc: Int): Int =
   4.118 +    if (is_interrupt(exn)) Interrupt.return_code else rc
   4.119 +
   4.120 +
   4.121 +  /* message */
   4.122 +
   4.123 +  def user_message(exn: Throwable): Option[String] =
   4.124 +    if (exn.getClass == classOf[RuntimeException] ||
   4.125 +        exn.getClass == classOf[User_Error])
   4.126 +    {
   4.127 +      val msg = exn.getMessage
   4.128 +      Some(if (msg == null || msg == "") "Error" else msg)
   4.129 +    }
   4.130 +    else if (exn.isInstanceOf[java.io.IOException])
   4.131 +    {
   4.132 +      val msg = exn.getMessage
   4.133 +      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
   4.134 +    }
   4.135 +    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
   4.136 +    else None
   4.137 +
   4.138 +  def message(exn: Throwable): String =
   4.139 +    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
   4.140 +}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/General/secure.ML	Thu Mar 03 21:59:21 2016 +0100
     5.3 @@ -0,0 +1,27 @@
     5.4 +(*  Title:      Pure/General/secure.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Secure critical operations.
     5.8 +*)
     5.9 +
    5.10 +signature SECURE =
    5.11 +sig
    5.12 +  val set_secure: unit -> unit
    5.13 +  val is_secure: unit -> bool
    5.14 +  val deny: string -> unit
    5.15 +  val deny_ml: unit -> unit
    5.16 +end;
    5.17 +
    5.18 +structure Secure: SECURE =
    5.19 +struct
    5.20 +
    5.21 +val secure = Unsynchronized.ref false;
    5.22 +
    5.23 +fun set_secure () = secure := true;
    5.24 +fun is_secure () = ! secure;
    5.25 +
    5.26 +fun deny msg = if is_secure () then error msg else ();
    5.27 +
    5.28 +fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
    5.29 +
    5.30 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/ML/fixed_int_dummy.ML	Thu Mar 03 21:59:21 2016 +0100
     6.3 @@ -0,0 +1,6 @@
     6.4 +(*  Title:      Pure/ML/fixed_int_dummy.ML
     6.5 +
     6.6 +FixedInt dummy that is not fixed (up to Poly/ML 5.6).
     6.7 +*)
     6.8 +
     6.9 +structure FixedInt = IntInf;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML/ml_compiler0.ML	Thu Mar 03 21:59:21 2016 +0100
     7.3 @@ -0,0 +1,110 @@
     7.4 +(*  Title:      Pure/ML/ml_compiler0.ML
     7.5 +
     7.6 +Runtime compilation and evaluation (bootstrap version of
     7.7 +Pure/ML/ml_compiler.ML).
     7.8 +*)
     7.9 +
    7.10 +signature ML_COMPILER0 =
    7.11 +sig
    7.12 +  type context =
    7.13 +   {name_space: ML_Name_Space.T,
    7.14 +    here: int -> string -> string,
    7.15 +    print: string -> unit,
    7.16 +    error: string -> unit}
    7.17 +  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
    7.18 +  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
    7.19 +  val debug_option: bool option -> bool
    7.20 +  val use_operations: (bool option -> string -> unit) ->
    7.21 +    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
    7.22 +end;
    7.23 +
    7.24 +structure ML_Compiler0: ML_COMPILER0 =
    7.25 +struct
    7.26 +
    7.27 +type context =
    7.28 + {name_space: ML_Name_Space.T,
    7.29 +  here: int -> string -> string,
    7.30 +  print: string -> unit,
    7.31 +  error: string -> unit};
    7.32 +
    7.33 +fun drop_newline s =
    7.34 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    7.35 +  else s;
    7.36 +
    7.37 +fun ml_positions start_line name txt =
    7.38 +  let
    7.39 +    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
    7.40 +          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
    7.41 +          in positions line cs (s :: res) end
    7.42 +      | positions line (c :: cs) res =
    7.43 +          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
    7.44 +      | positions _ [] res = rev res;
    7.45 +  in String.concat (positions start_line (String.explode txt) []) end;
    7.46 +
    7.47 +fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
    7.48 +  let
    7.49 +    val _ = Secure.deny_ml ();
    7.50 +
    7.51 +    val current_line = Unsynchronized.ref line;
    7.52 +    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
    7.53 +    val out_buffer = Unsynchronized.ref ([]: string list);
    7.54 +    fun output () = drop_newline (implode (rev (! out_buffer)));
    7.55 +
    7.56 +    fun get () =
    7.57 +      (case ! in_buffer of
    7.58 +        [] => NONE
    7.59 +      | c :: cs =>
    7.60 +          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    7.61 +    fun put s = out_buffer := s :: ! out_buffer;
    7.62 +    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
    7.63 +     (put (if hard then "Error: " else "Warning: ");
    7.64 +      PolyML.prettyPrint (put, 76) msg1;
    7.65 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    7.66 +      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
    7.67 +
    7.68 +    val parameters =
    7.69 +     [PolyML.Compiler.CPOutStream put,
    7.70 +      PolyML.Compiler.CPNameSpace name_space,
    7.71 +      PolyML.Compiler.CPErrorMessageProc put_message,
    7.72 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    7.73 +      PolyML.Compiler.CPFileName file,
    7.74 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
    7.75 +      PolyML.Compiler.CPDebug debug];
    7.76 +    val _ =
    7.77 +      (while not (List.null (! in_buffer)) do
    7.78 +        PolyML.compiler (get, parameters) ())
    7.79 +      handle exn =>
    7.80 +        if Exn.is_interrupt exn then Exn.reraise exn
    7.81 +        else
    7.82 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    7.83 +          error (output ()); Exn.reraise exn);
    7.84 +  in if verbose then print (output ()) else () end;
    7.85 +
    7.86 +fun use_file context {verbose, debug} file =
    7.87 +  let
    7.88 +    val instream = TextIO.openIn file;
    7.89 +    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    7.90 +  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    7.91 +
    7.92 +
    7.93 +fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
    7.94 +  | debug_option (SOME debug) = debug;
    7.95 +
    7.96 +fun use_operations (use_ : bool option -> string -> unit) =
    7.97 +  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
    7.98 +
    7.99 +end;
   7.100 +
   7.101 +val {use, use_debug, use_no_debug} =
   7.102 +  let
   7.103 +    val context: ML_Compiler0.context =
   7.104 +     {name_space = ML_Name_Space.global,
   7.105 +      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
   7.106 +      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
   7.107 +      error = fn s => error s};
   7.108 +  in
   7.109 +    ML_Compiler0.use_operations (fn opt_debug => fn file =>
   7.110 +      ML_Compiler0.use_file context
   7.111 +        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
   7.112 +      handle ERROR msg => (#print context msg; raise error "ML error"))
   7.113 +  end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/ML/ml_debugger.ML	Thu Mar 03 21:59:21 2016 +0100
     8.3 @@ -0,0 +1,72 @@
     8.4 +(*  Title:      Pure/ML/ml_debugger.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.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/ML/ml_heap.ML	Thu Mar 03 21:59:21 2016 +0100
     9.3 @@ -0,0 +1,17 @@
     9.4 +(*  Title:      Pure/ML/ml_heap.ML
     9.5 +    Author:     Makarius
     9.6 +
     9.7 +ML heap operations.
     9.8 +*)
     9.9 +
    9.10 +signature ML_HEAP =
    9.11 +sig
    9.12 +  val share_common_data: unit -> unit
    9.13 +  val save_state: string -> unit
    9.14 +end;
    9.15 +
    9.16 +structure ML_Heap: ML_HEAP =
    9.17 +struct
    9.18 +  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    9.19 +  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
    9.20 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 03 21:59:21 2016 +0100
    10.3 @@ -0,0 +1,41 @@
    10.4 +(*  Title:      Pure/ML/ml_name_space.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 +  val initial_val =
   10.22 +    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
   10.23 +      (#allVal global ());
   10.24 +
   10.25 +  type typeVal = TypeConstrs.typeConstr;
   10.26 +  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   10.27 +  val initial_type = #allType global ();
   10.28 +
   10.29 +  type fixityVal = Infixes.fixity;
   10.30 +  fun displayFix (_: string, x) = Infixes.print x;
   10.31 +  val initial_fixity = #allFix global ();
   10.32 +
   10.33 +  type structureVal = Structures.structureVal;
   10.34 +  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   10.35 +  val initial_structure = #allStruct global ();
   10.36 +
   10.37 +  type signatureVal = Signatures.signatureVal;
   10.38 +  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
   10.39 +  val initial_signature = #allSig global ();
   10.40 +
   10.41 +  type functorVal = Functors.functorVal;
   10.42 +  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
   10.43 +  val initial_functor = #allFunct global ();
   10.44 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 03 21:59:21 2016 +0100
    11.3 @@ -0,0 +1,84 @@
    11.4 +(*  Title:      Pure/ML/ml_pretty.ML
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Minimal support for raw ML pretty printing, notably for toplevel pp.
    11.8 +*)
    11.9 +
   11.10 +signature ML_PRETTY =
   11.11 +sig
   11.12 +  datatype pretty =
   11.13 +    Block of (string * string) * bool * FixedInt.int * pretty list |
   11.14 +    String of string * FixedInt.int |
   11.15 +    Break of bool * FixedInt.int * FixedInt.int
   11.16 +  val block: pretty list -> pretty
   11.17 +  val str: string -> pretty
   11.18 +  val brk: FixedInt.int -> pretty
   11.19 +  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
   11.20 +  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
   11.21 +  val to_polyml: pretty -> PolyML.pretty
   11.22 +  val from_polyml: PolyML.pretty -> pretty
   11.23 +end;
   11.24 +
   11.25 +structure ML_Pretty: ML_PRETTY =
   11.26 +struct
   11.27 +
   11.28 +datatype pretty =
   11.29 +  Block of (string * string) * bool * FixedInt.int * pretty list |
   11.30 +  String of string * FixedInt.int |
   11.31 +  Break of bool * FixedInt.int * FixedInt.int;
   11.32 +
   11.33 +fun block prts = Block (("", ""), false, 2, prts);
   11.34 +fun str s = String (s, FixedInt.fromInt (size s));
   11.35 +fun brk width = Break (false, width, 0);
   11.36 +
   11.37 +fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
   11.38 +  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
   11.39 +
   11.40 +fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
   11.41 +  let
   11.42 +    fun elems _ [] = []
   11.43 +      | elems 0 _ = [str "..."]
   11.44 +      | elems d [x] = [pretty (x, d)]
   11.45 +      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
   11.46 +  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
   11.47 +
   11.48 +
   11.49 +(* convert *)
   11.50 +
   11.51 +fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
   11.52 +  | to_polyml (Break (true, _, _)) =
   11.53 +      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
   11.54 +        [PolyML.PrettyString " "])
   11.55 +  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
   11.56 +      let val context =
   11.57 +        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
   11.58 +        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
   11.59 +      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
   11.60 +  | to_polyml (String (s, len)) =
   11.61 +      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
   11.62 +      else
   11.63 +        PolyML.PrettyBlock
   11.64 +          (0, false,
   11.65 +            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
   11.66 +
   11.67 +val from_polyml =
   11.68 +  let
   11.69 +    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
   11.70 +      | convert _ (PolyML.PrettyBlock (_, _,
   11.71 +            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
   11.72 +          Break (true, 1, 0)
   11.73 +      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
   11.74 +          let
   11.75 +            fun property name default =
   11.76 +              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
   11.77 +                SOME (PolyML.ContextProperty (_, b)) => b
   11.78 +              | _ => default);
   11.79 +            val bg = property "begin" "";
   11.80 +            val en = property "end" "";
   11.81 +            val len' = property "length" len;
   11.82 +          in Block ((bg, en), consistent, ind, map (convert len') prts) end
   11.83 +      | convert len (PolyML.PrettyString s) =
   11.84 +          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   11.85 +  in convert "" end;
   11.86 +
   11.87 +end;
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/ML/ml_profiling.ML	Thu Mar 03 21:59:21 2016 +0100
    12.3 @@ -0,0 +1,19 @@
    12.4 +(*  Title:      Pure/ML/ml_profiling.ML
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Profiling for Poly/ML 5.6.
    12.8 +*)
    12.9 +
   12.10 +structure ML_Profiling =
   12.11 +struct
   12.12 +
   12.13 +fun profile_time pr f x =
   12.14 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   12.15 +
   12.16 +fun profile_time_thread pr f x =
   12.17 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   12.18 +
   12.19 +fun profile_allocations pr f x =
   12.20 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   12.21 +
   12.22 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Pure/ML/ml_system.ML	Thu Mar 03 21:59:21 2016 +0100
    13.3 @@ -0,0 +1,58 @@
    13.4 +(*  Title:      Pure/ML/ml_system.ML
    13.5 +    Author:     Makarius
    13.6 +
    13.7 +ML system and platform operations.
    13.8 +*)
    13.9 +
   13.10 +signature ML_SYSTEM =
   13.11 +sig
   13.12 +  val name: string
   13.13 +  val platform: string
   13.14 +  val platform_is_windows: bool
   13.15 +  val platform_path: string -> string
   13.16 +  val standard_path: string -> string
   13.17 +end;
   13.18 +
   13.19 +structure ML_System: ML_SYSTEM =
   13.20 +struct
   13.21 +
   13.22 +val SOME name = OS.Process.getEnv "ML_SYSTEM";
   13.23 +val SOME platform = OS.Process.getEnv "ML_PLATFORM";
   13.24 +val platform_is_windows = String.isSuffix "windows" platform;
   13.25 +
   13.26 +val platform_path =
   13.27 +  if platform_is_windows then
   13.28 +    fn path =>
   13.29 +      if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
   13.30 +        (case String.tokens (fn c => c = #"/") path of
   13.31 +          "cygdrive" :: drive :: arcs =>
   13.32 +            let
   13.33 +              val vol =
   13.34 +                (case Char.fromString drive of
   13.35 +                  NONE => drive ^ ":"
   13.36 +                | SOME d => String.str (Char.toUpper d) ^ ":");
   13.37 +            in String.concatWith "\\" (vol :: arcs) end
   13.38 +        | arcs =>
   13.39 +            (case OS.Process.getEnv "CYGWIN_ROOT" of
   13.40 +              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
   13.41 +            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
   13.42 +      else String.translate (fn #"/" => "\\" | c => String.str c) path
   13.43 +  else fn path => path;
   13.44 +
   13.45 +val standard_path =
   13.46 +  if platform_is_windows then
   13.47 +    fn path =>
   13.48 +      let
   13.49 +        val {vol, arcs, isAbs} = OS.Path.fromString path;
   13.50 +        val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
   13.51 +      in
   13.52 +        if isAbs then
   13.53 +          (case String.explode vol of
   13.54 +            [d, #":"] =>
   13.55 +              String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
   13.56 +          | _ => path')
   13.57 +        else path'
   13.58 +      end
   13.59 +  else fn path => path;
   13.60 +
   13.61 +end;
    14.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 21:35:16 2016 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,94 +0,0 @@
    14.4 -(*  Title:      Pure/RAW/ROOT_polyml.ML
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -Compatibility wrapper for Poly/ML.
    14.8 -*)
    14.9 -
   14.10 -(* initial ML name space *)
   14.11 -
   14.12 -use "RAW/ml_system.ML";
   14.13 -use "RAW/ml_name_space.ML";
   14.14 -
   14.15 -if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
   14.16 -else use "RAW/fixed_int_dummy.ML";
   14.17 -
   14.18 -
   14.19 -(* exceptions *)
   14.20 -
   14.21 -use "RAW/exn.ML";
   14.22 -
   14.23 -
   14.24 -(* multithreading *)
   14.25 -
   14.26 -val seconds = Time.fromReal;
   14.27 -
   14.28 -open Thread;
   14.29 -use "RAW/multithreading.ML";
   14.30 -
   14.31 -use "RAW/unsynchronized.ML";
   14.32 -val _ = PolyML.Compiler.forgetValue "ref";
   14.33 -val _ = PolyML.Compiler.forgetType "ref";
   14.34 -
   14.35 -
   14.36 -(* pervasive environment *)
   14.37 -
   14.38 -val _ = PolyML.Compiler.forgetValue "isSome";
   14.39 -val _ = PolyML.Compiler.forgetValue "getOpt";
   14.40 -val _ = PolyML.Compiler.forgetValue "valOf";
   14.41 -val _ = PolyML.Compiler.forgetValue "foldl";
   14.42 -val _ = PolyML.Compiler.forgetValue "foldr";
   14.43 -val _ = PolyML.Compiler.forgetValue "print";
   14.44 -val _ = PolyML.Compiler.forgetValue "explode";
   14.45 -val _ = PolyML.Compiler.forgetValue "concat";
   14.46 -
   14.47 -val ord = SML90.ord;
   14.48 -val chr = SML90.chr;
   14.49 -val raw_explode = SML90.explode;
   14.50 -val implode = SML90.implode;
   14.51 -
   14.52 -fun quit () = exit 0;
   14.53 -
   14.54 -
   14.55 -(* ML runtime system *)
   14.56 -
   14.57 -use "RAW/ml_heap.ML";
   14.58 -use "RAW/ml_profiling.ML";
   14.59 -
   14.60 -val pointer_eq = PolyML.pointerEq;
   14.61 -
   14.62 -
   14.63 -(* ML toplevel pretty printing *)
   14.64 -
   14.65 -use "RAW/ml_pretty.ML";
   14.66 -
   14.67 -local
   14.68 -  val depth = Unsynchronized.ref 10;
   14.69 -in
   14.70 -  fun get_default_print_depth () = ! depth;
   14.71 -  fun default_print_depth n = (depth := n; PolyML.print_depth n);
   14.72 -  val _ = default_print_depth 10;
   14.73 -end;
   14.74 -
   14.75 -val error_depth = PolyML.error_depth;
   14.76 -
   14.77 -
   14.78 -(* ML compiler *)
   14.79 -
   14.80 -use "RAW/secure.ML";
   14.81 -use "RAW/ml_compiler0.ML";
   14.82 -
   14.83 -PolyML.Compiler.reportUnreferencedIds := true;
   14.84 -PolyML.Compiler.reportExhaustiveHandlers := true;
   14.85 -PolyML.Compiler.printInAlphabeticalOrder := false;
   14.86 -PolyML.Compiler.maxInlineSize := 80;
   14.87 -PolyML.Compiler.prompt1 := "ML> ";
   14.88 -PolyML.Compiler.prompt2 := "ML# ";
   14.89 -
   14.90 -fun ml_make_string struct_name =
   14.91 -  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
   14.92 -    struct_name ^ ".ML_print_depth ()))))))";
   14.93 -
   14.94 -
   14.95 -(* ML debugger *)
   14.96 -
   14.97 -use_no_debug "RAW/ml_debugger.ML";
    15.1 --- a/src/Pure/RAW/exn.ML	Thu Mar 03 21:35:16 2016 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,134 +0,0 @@
    15.4 -(*  Title:      Pure/RAW/exn.ML
    15.5 -    Author:     Makarius
    15.6 -
    15.7 -Support for exceptions.
    15.8 -*)
    15.9 -
   15.10 -signature BASIC_EXN =
   15.11 -sig
   15.12 -  exception ERROR of string
   15.13 -  val error: string -> 'a
   15.14 -  val cat_error: string -> string -> 'a
   15.15 -end;
   15.16 -
   15.17 -signature EXN =
   15.18 -sig
   15.19 -  include BASIC_EXN
   15.20 -  val reraise: exn -> 'a
   15.21 -  datatype 'a result = Res of 'a | Exn of exn
   15.22 -  val get_res: 'a result -> 'a option
   15.23 -  val get_exn: 'a result -> exn option
   15.24 -  val capture: ('a -> 'b) -> 'a -> 'b result
   15.25 -  val release: 'a result -> 'a
   15.26 -  val map_res: ('a -> 'b) -> 'a result -> 'b result
   15.27 -  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
   15.28 -  val map_exn: (exn -> exn) -> 'a result -> 'a result
   15.29 -  exception Interrupt
   15.30 -  val interrupt: unit -> 'a
   15.31 -  val is_interrupt: exn -> bool
   15.32 -  val interrupt_exn: 'a result
   15.33 -  val is_interrupt_exn: 'a result -> bool
   15.34 -  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
   15.35 -  val return_code: exn -> int -> int
   15.36 -  val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   15.37 -  exception EXCEPTIONS of exn list
   15.38 -  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
   15.39 -end;
   15.40 -
   15.41 -structure Exn: EXN =
   15.42 -struct
   15.43 -
   15.44 -(* reraise *)
   15.45 -
   15.46 -fun reraise exn =
   15.47 -  (case PolyML.exceptionLocation exn of
   15.48 -    NONE => raise exn
   15.49 -  | SOME location => PolyML.raiseWithLocation (exn, location));
   15.50 -
   15.51 -
   15.52 -(* user errors *)
   15.53 -
   15.54 -exception ERROR of string;
   15.55 -
   15.56 -fun error msg = raise ERROR msg;
   15.57 -
   15.58 -fun cat_error "" msg = error msg
   15.59 -  | cat_error msg "" = error msg
   15.60 -  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
   15.61 -
   15.62 -
   15.63 -(* exceptions as values *)
   15.64 -
   15.65 -datatype 'a result =
   15.66 -  Res of 'a |
   15.67 -  Exn of exn;
   15.68 -
   15.69 -fun get_res (Res x) = SOME x
   15.70 -  | get_res _ = NONE;
   15.71 -
   15.72 -fun get_exn (Exn exn) = SOME exn
   15.73 -  | get_exn _ = NONE;
   15.74 -
   15.75 -fun capture f x = Res (f x) handle e => Exn e;
   15.76 -
   15.77 -fun release (Res y) = y
   15.78 -  | release (Exn e) = reraise e;
   15.79 -
   15.80 -fun map_res f (Res x) = Res (f x)
   15.81 -  | map_res f (Exn e) = Exn e;
   15.82 -
   15.83 -fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
   15.84 -
   15.85 -fun map_exn f (Res x) = Res x
   15.86 -  | map_exn f (Exn e) = Exn (f e);
   15.87 -
   15.88 -
   15.89 -(* interrupts *)
   15.90 -
   15.91 -exception Interrupt = SML90.Interrupt;
   15.92 -
   15.93 -fun interrupt () = raise Interrupt;
   15.94 -
   15.95 -fun is_interrupt Interrupt = true
   15.96 -  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
   15.97 -  | is_interrupt _ = false;
   15.98 -
   15.99 -val interrupt_exn = Exn Interrupt;
  15.100 -
  15.101 -fun is_interrupt_exn (Exn exn) = is_interrupt exn
  15.102 -  | is_interrupt_exn _ = false;
  15.103 -
  15.104 -fun interruptible_capture f x =
  15.105 -  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
  15.106 -
  15.107 -
  15.108 -(* POSIX return code *)
  15.109 -
  15.110 -fun return_code exn rc =
  15.111 -  if is_interrupt exn then (130: int) else rc;
  15.112 -
  15.113 -fun capture_exit rc f x =
  15.114 -  f x handle exn => exit (return_code exn rc);
  15.115 -
  15.116 -
  15.117 -(* concatenated exceptions *)
  15.118 -
  15.119 -exception EXCEPTIONS of exn list;
  15.120 -
  15.121 -
  15.122 -(* low-level trace *)
  15.123 -
  15.124 -fun trace exn_message output e =
  15.125 -  PolyML.Exception.traceException
  15.126 -    (e, fn (trace, exn) =>
  15.127 -      let
  15.128 -        val title = "Exception trace - " ^ exn_message exn;
  15.129 -        val () = output (String.concatWith "\n" (title :: trace));
  15.130 -      in reraise exn end);
  15.131 -
  15.132 -end;
  15.133 -
  15.134 -datatype illegal = Interrupt;
  15.135 -
  15.136 -structure Basic_Exn: BASIC_EXN = Exn;
  15.137 -open Basic_Exn;
    16.1 --- a/src/Pure/RAW/exn.scala	Thu Mar 03 21:35:16 2016 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,137 +0,0 @@
    16.4 -/*  Title:      Pure/RAW/exn.scala
    16.5 -    Module:     PIDE
    16.6 -    Author:     Makarius
    16.7 -
    16.8 -Support for exceptions (arbitrary throwables).
    16.9 -*/
   16.10 -
   16.11 -package isabelle
   16.12 -
   16.13 -
   16.14 -object Exn
   16.15 -{
   16.16 -  /* user errors */
   16.17 -
   16.18 -  class User_Error(message: String) extends RuntimeException(message)
   16.19 -  {
   16.20 -    override def equals(that: Any): Boolean =
   16.21 -      that match {
   16.22 -        case other: User_Error => message == other.getMessage
   16.23 -        case _ => false
   16.24 -      }
   16.25 -    override def hashCode: Int = message.hashCode
   16.26 -
   16.27 -    override def toString: String = "ERROR(" + message + ")"
   16.28 -  }
   16.29 -
   16.30 -  object ERROR
   16.31 -  {
   16.32 -    def apply(message: String): User_Error = new User_Error(message)
   16.33 -    def unapply(exn: Throwable): Option[String] = user_message(exn)
   16.34 -  }
   16.35 -
   16.36 -  def error(message: String): Nothing = throw ERROR(message)
   16.37 -
   16.38 -  def cat_message(msg1: String, msg2: String): String =
   16.39 -    if (msg1 == "") msg2
   16.40 -    else if (msg2 == "") msg1
   16.41 -    else msg1 + "\n" + msg2
   16.42 -
   16.43 -  def cat_error(msg1: String, msg2: String): Nothing =
   16.44 -    error(cat_message(msg1, msg2))
   16.45 -
   16.46 -
   16.47 -  /* exceptions as values */
   16.48 -
   16.49 -  sealed abstract class Result[A]
   16.50 -  {
   16.51 -    def user_error: Result[A] =
   16.52 -      this match {
   16.53 -        case Exn(ERROR(msg)) => Exn(ERROR(msg))
   16.54 -        case _ => this
   16.55 -      }
   16.56 -  }
   16.57 -  case class Res[A](res: A) extends Result[A]
   16.58 -  case class Exn[A](exn: Throwable) extends Result[A]
   16.59 -
   16.60 -  def capture[A](e: => A): Result[A] =
   16.61 -    try { Res(e) }
   16.62 -    catch { case exn: Throwable => Exn[A](exn) }
   16.63 -
   16.64 -  def release[A](result: Result[A]): A =
   16.65 -    result match {
   16.66 -      case Res(x) => x
   16.67 -      case Exn(exn) => throw exn
   16.68 -    }
   16.69 -
   16.70 -  def release_first[A](results: List[Result[A]]): List[A] =
   16.71 -    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
   16.72 -      case Some(Exn(exn)) => throw exn
   16.73 -      case _ => results.map(release(_))
   16.74 -    }
   16.75 -
   16.76 -
   16.77 -  /* interrupts */
   16.78 -
   16.79 -  def is_interrupt(exn: Throwable): Boolean =
   16.80 -  {
   16.81 -    var found_interrupt = false
   16.82 -    var e = exn
   16.83 -    while (!found_interrupt && e != null) {
   16.84 -      found_interrupt |= e.isInstanceOf[InterruptedException]
   16.85 -      e = e.getCause
   16.86 -    }
   16.87 -    found_interrupt
   16.88 -  }
   16.89 -
   16.90 -  object Interrupt
   16.91 -  {
   16.92 -    def apply(): Throwable = new InterruptedException
   16.93 -    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
   16.94 -
   16.95 -    def expose() { if (Thread.interrupted) throw apply() }
   16.96 -    def impose() { Thread.currentThread.interrupt }
   16.97 -
   16.98 -    def postpone[A](body: => A): Option[A] =
   16.99 -    {
  16.100 -      val interrupted = Thread.interrupted
  16.101 -      val result = capture { body }
  16.102 -      if (interrupted) impose()
  16.103 -      result match {
  16.104 -        case Res(x) => Some(x)
  16.105 -        case Exn(e) =>
  16.106 -          if (is_interrupt(e)) { impose(); None }
  16.107 -          else throw e
  16.108 -      }
  16.109 -    }
  16.110 -
  16.111 -    val return_code = 130
  16.112 -  }
  16.113 -
  16.114 -
  16.115 -  /* POSIX return code */
  16.116 -
  16.117 -  def return_code(exn: Throwable, rc: Int): Int =
  16.118 -    if (is_interrupt(exn)) Interrupt.return_code else rc
  16.119 -
  16.120 -
  16.121 -  /* message */
  16.122 -
  16.123 -  def user_message(exn: Throwable): Option[String] =
  16.124 -    if (exn.getClass == classOf[RuntimeException] ||
  16.125 -        exn.getClass == classOf[User_Error])
  16.126 -    {
  16.127 -      val msg = exn.getMessage
  16.128 -      Some(if (msg == null || msg == "") "Error" else msg)
  16.129 -    }
  16.130 -    else if (exn.isInstanceOf[java.io.IOException])
  16.131 -    {
  16.132 -      val msg = exn.getMessage
  16.133 -      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
  16.134 -    }
  16.135 -    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
  16.136 -    else None
  16.137 -
  16.138 -  def message(exn: Throwable): String =
  16.139 -    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
  16.140 -}
    17.1 --- a/src/Pure/RAW/fixed_int_dummy.ML	Thu Mar 03 21:35:16 2016 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,6 +0,0 @@
    17.4 -(*  Title:      Pure/RAW/fixed_int_dummy.ML
    17.5 -
    17.6 -FixedInt dummy that is not fixed (up to Poly/ML 5.6).
    17.7 -*)
    17.8 -
    17.9 -structure FixedInt = IntInf;
    18.1 --- a/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 21:35:16 2016 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,110 +0,0 @@
    18.4 -(*  Title:      Pure/RAW/ml_compiler0.ML
    18.5 -
    18.6 -Runtime compilation and evaluation (bootstrap version of
    18.7 -Pure/ML/ml_compiler.ML).
    18.8 -*)
    18.9 -
   18.10 -signature ML_COMPILER0 =
   18.11 -sig
   18.12 -  type context =
   18.13 -   {name_space: ML_Name_Space.T,
   18.14 -    here: int -> string -> string,
   18.15 -    print: string -> unit,
   18.16 -    error: string -> unit}
   18.17 -  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
   18.18 -  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
   18.19 -  val debug_option: bool option -> bool
   18.20 -  val use_operations: (bool option -> string -> unit) ->
   18.21 -    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
   18.22 -end;
   18.23 -
   18.24 -structure ML_Compiler0: ML_COMPILER0 =
   18.25 -struct
   18.26 -
   18.27 -type context =
   18.28 - {name_space: ML_Name_Space.T,
   18.29 -  here: int -> string -> string,
   18.30 -  print: string -> unit,
   18.31 -  error: string -> unit};
   18.32 -
   18.33 -fun drop_newline s =
   18.34 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   18.35 -  else s;
   18.36 -
   18.37 -fun ml_positions start_line name txt =
   18.38 -  let
   18.39 -    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
   18.40 -          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
   18.41 -          in positions line cs (s :: res) end
   18.42 -      | positions line (c :: cs) res =
   18.43 -          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
   18.44 -      | positions _ [] res = rev res;
   18.45 -  in String.concat (positions start_line (String.explode txt) []) end;
   18.46 -
   18.47 -fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
   18.48 -  let
   18.49 -    val _ = Secure.deny_ml ();
   18.50 -
   18.51 -    val current_line = Unsynchronized.ref line;
   18.52 -    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
   18.53 -    val out_buffer = Unsynchronized.ref ([]: string list);
   18.54 -    fun output () = drop_newline (implode (rev (! out_buffer)));
   18.55 -
   18.56 -    fun get () =
   18.57 -      (case ! in_buffer of
   18.58 -        [] => NONE
   18.59 -      | c :: cs =>
   18.60 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
   18.61 -    fun put s = out_buffer := s :: ! out_buffer;
   18.62 -    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
   18.63 -     (put (if hard then "Error: " else "Warning: ");
   18.64 -      PolyML.prettyPrint (put, 76) msg1;
   18.65 -      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
   18.66 -      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
   18.67 -
   18.68 -    val parameters =
   18.69 -     [PolyML.Compiler.CPOutStream put,
   18.70 -      PolyML.Compiler.CPNameSpace name_space,
   18.71 -      PolyML.Compiler.CPErrorMessageProc put_message,
   18.72 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
   18.73 -      PolyML.Compiler.CPFileName file,
   18.74 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
   18.75 -      PolyML.Compiler.CPDebug debug];
   18.76 -    val _ =
   18.77 -      (while not (List.null (! in_buffer)) do
   18.78 -        PolyML.compiler (get, parameters) ())
   18.79 -      handle exn =>
   18.80 -        if Exn.is_interrupt exn then Exn.reraise exn
   18.81 -        else
   18.82 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   18.83 -          error (output ()); Exn.reraise exn);
   18.84 -  in if verbose then print (output ()) else () end;
   18.85 -
   18.86 -fun use_file context {verbose, debug} file =
   18.87 -  let
   18.88 -    val instream = TextIO.openIn file;
   18.89 -    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   18.90 -  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
   18.91 -
   18.92 -
   18.93 -fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
   18.94 -  | debug_option (SOME debug) = debug;
   18.95 -
   18.96 -fun use_operations (use_ : bool option -> string -> unit) =
   18.97 -  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
   18.98 -
   18.99 -end;
  18.100 -
  18.101 -val {use, use_debug, use_no_debug} =
  18.102 -  let
  18.103 -    val context: ML_Compiler0.context =
  18.104 -     {name_space = ML_Name_Space.global,
  18.105 -      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
  18.106 -      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
  18.107 -      error = fn s => error s};
  18.108 -  in
  18.109 -    ML_Compiler0.use_operations (fn opt_debug => fn file =>
  18.110 -      ML_Compiler0.use_file context
  18.111 -        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
  18.112 -      handle ERROR msg => (#print context msg; raise error "ML error"))
  18.113 -  end;
    19.1 --- a/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 21:35:16 2016 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,72 +0,0 @@
    19.4 -(*  Title:      Pure/RAW/ml_debugger.ML
    19.5 -    Author:     Makarius
    19.6 -
    19.7 -ML debugger interface -- for Poly/ML 5.6, or later.
    19.8 -*)
    19.9 -
   19.10 -signature ML_DEBUGGER =
   19.11 -sig
   19.12 -  type exn_id
   19.13 -  val exn_id: exn -> exn_id
   19.14 -  val print_exn_id: exn_id -> string
   19.15 -  val eq_exn_id: exn_id * exn_id -> bool
   19.16 -  type location
   19.17 -  val on_entry: (string * location -> unit) option -> unit
   19.18 -  val on_exit: (string * location -> unit) option -> unit
   19.19 -  val on_exit_exception: (string * location -> exn -> unit) option -> unit
   19.20 -  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
   19.21 -  type state
   19.22 -  val state: Thread.thread -> state list
   19.23 -  val debug_function: state -> string
   19.24 -  val debug_function_arg: state -> ML_Name_Space.valueVal
   19.25 -  val debug_function_result: state -> ML_Name_Space.valueVal
   19.26 -  val debug_location: state -> location
   19.27 -  val debug_name_space: state -> ML_Name_Space.T
   19.28 -  val debug_local_name_space: state -> ML_Name_Space.T
   19.29 -end;
   19.30 -
   19.31 -structure ML_Debugger: ML_DEBUGGER =
   19.32 -struct
   19.33 -
   19.34 -(* exceptions *)
   19.35 -
   19.36 -abstype exn_id = Exn_Id of string * int Unsynchronized.ref
   19.37 -with
   19.38 -
   19.39 -fun exn_id exn =
   19.40 -  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
   19.41 -
   19.42 -fun print_exn_id (Exn_Id (name, _)) = name;
   19.43 -fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
   19.44 -
   19.45 -end;
   19.46 -
   19.47 -val _ =
   19.48 -  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
   19.49 -    let val s = print_exn_id exn_id
   19.50 -    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
   19.51 -
   19.52 -
   19.53 -(* hooks *)
   19.54 -
   19.55 -type location = PolyML.location;
   19.56 -
   19.57 -val on_entry = PolyML.DebuggerInterface.setOnEntry;
   19.58 -val on_exit = PolyML.DebuggerInterface.setOnExit;
   19.59 -val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
   19.60 -val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
   19.61 -
   19.62 -
   19.63 -(* debugger operations *)
   19.64 -
   19.65 -type state = PolyML.DebuggerInterface.debugState;
   19.66 -
   19.67 -val state = PolyML.DebuggerInterface.debugState;
   19.68 -val debug_function = PolyML.DebuggerInterface.debugFunction;
   19.69 -val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
   19.70 -val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
   19.71 -val debug_location = PolyML.DebuggerInterface.debugLocation;
   19.72 -val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
   19.73 -val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
   19.74 -
   19.75 -end;
    20.1 --- a/src/Pure/RAW/ml_heap.ML	Thu Mar 03 21:35:16 2016 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,17 +0,0 @@
    20.4 -(*  Title:      Pure/RAW/ml_heap.ML
    20.5 -    Author:     Makarius
    20.6 -
    20.7 -ML heap operations.
    20.8 -*)
    20.9 -
   20.10 -signature ML_HEAP =
   20.11 -sig
   20.12 -  val share_common_data: unit -> unit
   20.13 -  val save_state: string -> unit
   20.14 -end;
   20.15 -
   20.16 -structure ML_Heap: ML_HEAP =
   20.17 -struct
   20.18 -  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   20.19 -  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
   20.20 -end;
    21.1 --- a/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 21:35:16 2016 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,41 +0,0 @@
    21.4 -(*  Title:      Pure/RAW/ml_name_space.ML
    21.5 -    Author:     Makarius
    21.6 -
    21.7 -Name space for Poly/ML.
    21.8 -*)
    21.9 -
   21.10 -structure ML_Name_Space =
   21.11 -struct
   21.12 -  open PolyML.NameSpace;
   21.13 -
   21.14 -  type T = PolyML.NameSpace.nameSpace;
   21.15 -  val global = PolyML.globalNameSpace;
   21.16 -  val forget_global_structure = PolyML.Compiler.forgetStructure;
   21.17 -
   21.18 -  type valueVal = Values.value;
   21.19 -  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   21.20 -  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
   21.21 -  val initial_val =
   21.22 -    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
   21.23 -      (#allVal global ());
   21.24 -
   21.25 -  type typeVal = TypeConstrs.typeConstr;
   21.26 -  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
   21.27 -  val initial_type = #allType global ();
   21.28 -
   21.29 -  type fixityVal = Infixes.fixity;
   21.30 -  fun displayFix (_: string, x) = Infixes.print x;
   21.31 -  val initial_fixity = #allFix global ();
   21.32 -
   21.33 -  type structureVal = Structures.structureVal;
   21.34 -  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
   21.35 -  val initial_structure = #allStruct global ();
   21.36 -
   21.37 -  type signatureVal = Signatures.signatureVal;
   21.38 -  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
   21.39 -  val initial_signature = #allSig global ();
   21.40 -
   21.41 -  type functorVal = Functors.functorVal;
   21.42 -  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
   21.43 -  val initial_functor = #allFunct global ();
   21.44 -end;
    22.1 --- a/src/Pure/RAW/ml_pretty.ML	Thu Mar 03 21:35:16 2016 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,84 +0,0 @@
    22.4 -(*  Title:      Pure/RAW/ml_pretty.ML
    22.5 -    Author:     Makarius
    22.6 -
    22.7 -Minimal support for raw ML pretty printing, notably for toplevel pp.
    22.8 -*)
    22.9 -
   22.10 -signature ML_PRETTY =
   22.11 -sig
   22.12 -  datatype pretty =
   22.13 -    Block of (string * string) * bool * FixedInt.int * pretty list |
   22.14 -    String of string * FixedInt.int |
   22.15 -    Break of bool * FixedInt.int * FixedInt.int
   22.16 -  val block: pretty list -> pretty
   22.17 -  val str: string -> pretty
   22.18 -  val brk: FixedInt.int -> pretty
   22.19 -  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
   22.20 -  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
   22.21 -  val to_polyml: pretty -> PolyML.pretty
   22.22 -  val from_polyml: PolyML.pretty -> pretty
   22.23 -end;
   22.24 -
   22.25 -structure ML_Pretty: ML_PRETTY =
   22.26 -struct
   22.27 -
   22.28 -datatype pretty =
   22.29 -  Block of (string * string) * bool * FixedInt.int * pretty list |
   22.30 -  String of string * FixedInt.int |
   22.31 -  Break of bool * FixedInt.int * FixedInt.int;
   22.32 -
   22.33 -fun block prts = Block (("", ""), false, 2, prts);
   22.34 -fun str s = String (s, FixedInt.fromInt (size s));
   22.35 -fun brk width = Break (false, width, 0);
   22.36 -
   22.37 -fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
   22.38 -  block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
   22.39 -
   22.40 -fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
   22.41 -  let
   22.42 -    fun elems _ [] = []
   22.43 -      | elems 0 _ = [str "..."]
   22.44 -      | elems d [x] = [pretty (x, d)]
   22.45 -      | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
   22.46 -  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
   22.47 -
   22.48 -
   22.49 -(* convert *)
   22.50 -
   22.51 -fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
   22.52 -  | to_polyml (Break (true, _, _)) =
   22.53 -      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
   22.54 -        [PolyML.PrettyString " "])
   22.55 -  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
   22.56 -      let val context =
   22.57 -        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
   22.58 -        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
   22.59 -      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
   22.60 -  | to_polyml (String (s, len)) =
   22.61 -      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
   22.62 -      else
   22.63 -        PolyML.PrettyBlock
   22.64 -          (0, false,
   22.65 -            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
   22.66 -
   22.67 -val from_polyml =
   22.68 -  let
   22.69 -    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
   22.70 -      | convert _ (PolyML.PrettyBlock (_, _,
   22.71 -            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
   22.72 -          Break (true, 1, 0)
   22.73 -      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
   22.74 -          let
   22.75 -            fun property name default =
   22.76 -              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
   22.77 -                SOME (PolyML.ContextProperty (_, b)) => b
   22.78 -              | _ => default);
   22.79 -            val bg = property "begin" "";
   22.80 -            val en = property "end" "";
   22.81 -            val len' = property "length" len;
   22.82 -          in Block ((bg, en), consistent, ind, map (convert len') prts) end
   22.83 -      | convert len (PolyML.PrettyString s) =
   22.84 -          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   22.85 -  in convert "" end;
   22.86 -
   22.87 -end;
    23.1 --- a/src/Pure/RAW/ml_profiling.ML	Thu Mar 03 21:35:16 2016 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,19 +0,0 @@
    23.4 -(*  Title:      Pure/RAW/ml_profiling.ML
    23.5 -    Author:     Makarius
    23.6 -
    23.7 -Profiling for Poly/ML 5.6.
    23.8 -*)
    23.9 -
   23.10 -structure ML_Profiling =
   23.11 -struct
   23.12 -
   23.13 -fun profile_time pr f x =
   23.14 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   23.15 -
   23.16 -fun profile_time_thread pr f x =
   23.17 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   23.18 -
   23.19 -fun profile_allocations pr f x =
   23.20 -  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   23.21 -
   23.22 -end;
    24.1 --- a/src/Pure/RAW/ml_system.ML	Thu Mar 03 21:35:16 2016 +0100
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,58 +0,0 @@
    24.4 -(*  Title:      Pure/RAW/ml_system.ML
    24.5 -    Author:     Makarius
    24.6 -
    24.7 -ML system and platform operations.
    24.8 -*)
    24.9 -
   24.10 -signature ML_SYSTEM =
   24.11 -sig
   24.12 -  val name: string
   24.13 -  val platform: string
   24.14 -  val platform_is_windows: bool
   24.15 -  val platform_path: string -> string
   24.16 -  val standard_path: string -> string
   24.17 -end;
   24.18 -
   24.19 -structure ML_System: ML_SYSTEM =
   24.20 -struct
   24.21 -
   24.22 -val SOME name = OS.Process.getEnv "ML_SYSTEM";
   24.23 -val SOME platform = OS.Process.getEnv "ML_PLATFORM";
   24.24 -val platform_is_windows = String.isSuffix "windows" platform;
   24.25 -
   24.26 -val platform_path =
   24.27 -  if platform_is_windows then
   24.28 -    fn path =>
   24.29 -      if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then
   24.30 -        (case String.tokens (fn c => c = #"/") path of
   24.31 -          "cygdrive" :: drive :: arcs =>
   24.32 -            let
   24.33 -              val vol =
   24.34 -                (case Char.fromString drive of
   24.35 -                  NONE => drive ^ ":"
   24.36 -                | SOME d => String.str (Char.toUpper d) ^ ":");
   24.37 -            in String.concatWith "\\" (vol :: arcs) end
   24.38 -        | arcs =>
   24.39 -            (case OS.Process.getEnv "CYGWIN_ROOT" of
   24.40 -              SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
   24.41 -            | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
   24.42 -      else String.translate (fn #"/" => "\\" | c => String.str c) path
   24.43 -  else fn path => path;
   24.44 -
   24.45 -val standard_path =
   24.46 -  if platform_is_windows then
   24.47 -    fn path =>
   24.48 -      let
   24.49 -        val {vol, arcs, isAbs} = OS.Path.fromString path;
   24.50 -        val path' = String.translate (fn #"\\" => "/" | c => String.str c) path;
   24.51 -      in
   24.52 -        if isAbs then
   24.53 -          (case String.explode vol of
   24.54 -            [d, #":"] =>
   24.55 -              String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs)
   24.56 -          | _ => path')
   24.57 -        else path'
   24.58 -      end
   24.59 -  else fn path => path;
   24.60 -
   24.61 -end;
    25.1 --- a/src/Pure/RAW/multithreading.ML	Thu Mar 03 21:35:16 2016 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,196 +0,0 @@
    25.4 -(*  Title:      Pure/RAW/multithreading.ML
    25.5 -    Author:     Makarius
    25.6 -
    25.7 -Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
    25.8 -*)
    25.9 -
   25.10 -signature BASIC_MULTITHREADING =
   25.11 -sig
   25.12 -  val interruptible: ('a -> 'b) -> 'a -> 'b
   25.13 -  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   25.14 -end;
   25.15 -
   25.16 -signature MULTITHREADING =
   25.17 -sig
   25.18 -  include BASIC_MULTITHREADING
   25.19 -  val no_interrupts: Thread.threadAttribute list
   25.20 -  val public_interrupts: Thread.threadAttribute list
   25.21 -  val private_interrupts: Thread.threadAttribute list
   25.22 -  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
   25.23 -  val interrupted: unit -> unit  (*exception Interrupt*)
   25.24 -  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   25.25 -  val max_threads_value: unit -> int
   25.26 -  val max_threads_update: int -> unit
   25.27 -  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
   25.28 -  val enabled: unit -> bool
   25.29 -  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
   25.30 -    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   25.31 -  val trace: int ref
   25.32 -  val tracing: int -> (unit -> string) -> unit
   25.33 -  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   25.34 -  val real_time: ('a -> unit) -> 'a -> Time.time
   25.35 -  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
   25.36 -  val serial: unit -> int
   25.37 -end;
   25.38 -
   25.39 -structure Multithreading: MULTITHREADING =
   25.40 -struct
   25.41 -
   25.42 -(* thread attributes *)
   25.43 -
   25.44 -val no_interrupts =
   25.45 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
   25.46 -
   25.47 -val test_interrupts =
   25.48 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
   25.49 -
   25.50 -val public_interrupts =
   25.51 -  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
   25.52 -
   25.53 -val private_interrupts =
   25.54 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
   25.55 -
   25.56 -val sync_interrupts = map
   25.57 -  (fn x as Thread.InterruptState Thread.InterruptDefer => x
   25.58 -    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
   25.59 -    | x => x);
   25.60 -
   25.61 -val safe_interrupts = map
   25.62 -  (fn Thread.InterruptState Thread.InterruptAsynch =>
   25.63 -      Thread.InterruptState Thread.InterruptAsynchOnce
   25.64 -    | x => x);
   25.65 -
   25.66 -fun interrupted () =
   25.67 -  let
   25.68 -    val orig_atts = safe_interrupts (Thread.getAttributes ());
   25.69 -    val _ = Thread.setAttributes test_interrupts;
   25.70 -    val test = Exn.capture Thread.testInterrupt ();
   25.71 -    val _ = Thread.setAttributes orig_atts;
   25.72 -  in Exn.release test end;
   25.73 -
   25.74 -fun with_attributes new_atts e =
   25.75 -  let
   25.76 -    val orig_atts = safe_interrupts (Thread.getAttributes ());
   25.77 -    val result = Exn.capture (fn () =>
   25.78 -      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
   25.79 -    val _ = Thread.setAttributes orig_atts;
   25.80 -  in Exn.release result end;
   25.81 -
   25.82 -
   25.83 -(* portable wrappers *)
   25.84 -
   25.85 -fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
   25.86 -
   25.87 -fun uninterruptible f x =
   25.88 -  with_attributes no_interrupts (fn atts =>
   25.89 -    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
   25.90 -
   25.91 -
   25.92 -(* options *)
   25.93 -
   25.94 -fun num_processors () =
   25.95 -  (case Thread.numPhysicalProcessors () of
   25.96 -    SOME n => n
   25.97 -  | NONE => Thread.numProcessors ());
   25.98 -
   25.99 -fun max_threads_result m =
  25.100 -  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
  25.101 -
  25.102 -val max_threads = ref 1;
  25.103 -
  25.104 -fun max_threads_value () = ! max_threads;
  25.105 -
  25.106 -fun max_threads_update m = max_threads := max_threads_result m;
  25.107 -
  25.108 -fun max_threads_setmp m f x =
  25.109 -  uninterruptible (fn restore_attributes => fn () =>
  25.110 -    let
  25.111 -      val max_threads_orig = ! max_threads;
  25.112 -      val _ = max_threads_update m;
  25.113 -      val result = Exn.capture (restore_attributes f) x;
  25.114 -      val _ = max_threads := max_threads_orig;
  25.115 -    in Exn.release result end) ();
  25.116 -
  25.117 -fun enabled () = max_threads_value () > 1;
  25.118 -
  25.119 -
  25.120 -(* synchronous wait *)
  25.121 -
  25.122 -fun sync_wait opt_atts time cond lock =
  25.123 -  with_attributes
  25.124 -    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
  25.125 -    (fn _ =>
  25.126 -      (case time of
  25.127 -        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
  25.128 -      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
  25.129 -      handle exn => Exn.Exn exn);
  25.130 -
  25.131 -
  25.132 -(* tracing *)
  25.133 -
  25.134 -val trace = ref 0;
  25.135 -
  25.136 -fun tracing level msg =
  25.137 -  if level > ! trace then ()
  25.138 -  else uninterruptible (fn _ => fn () =>
  25.139 -    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
  25.140 -      handle _ (*sic*) => ()) ();
  25.141 -
  25.142 -fun tracing_time detailed time =
  25.143 -  tracing
  25.144 -   (if not detailed then 5
  25.145 -    else if Time.>= (time, seconds 1.0) then 1
  25.146 -    else if Time.>= (time, seconds 0.1) then 2
  25.147 -    else if Time.>= (time, seconds 0.01) then 3
  25.148 -    else if Time.>= (time, seconds 0.001) then 4 else 5);
  25.149 -
  25.150 -fun real_time f x =
  25.151 -  let
  25.152 -    val timer = Timer.startRealTimer ();
  25.153 -    val () = f x;
  25.154 -    val time = Timer.checkRealTimer timer;
  25.155 -  in time end;
  25.156 -
  25.157 -
  25.158 -(* synchronized evaluation *)
  25.159 -
  25.160 -fun synchronized name lock e =
  25.161 -  Exn.release (uninterruptible (fn restore_attributes => fn () =>
  25.162 -    let
  25.163 -      val immediate =
  25.164 -        if Mutex.trylock lock then true
  25.165 -        else
  25.166 -          let
  25.167 -            val _ = tracing 5 (fn () => name ^ ": locking ...");
  25.168 -            val time = real_time Mutex.lock lock;
  25.169 -            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
  25.170 -          in false end;
  25.171 -      val result = Exn.capture (restore_attributes e) ();
  25.172 -      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
  25.173 -      val _ = Mutex.unlock lock;
  25.174 -    in result end) ());
  25.175 -
  25.176 -
  25.177 -(* serial numbers *)
  25.178 -
  25.179 -local
  25.180 -
  25.181 -val serial_lock = Mutex.mutex ();
  25.182 -val serial_count = ref 0;
  25.183 -
  25.184 -in
  25.185 -
  25.186 -val serial = uninterruptible (fn _ => fn () =>
  25.187 -  let
  25.188 -    val _ = Mutex.lock serial_lock;
  25.189 -    val _ = serial_count := ! serial_count + 1;
  25.190 -    val res = ! serial_count;
  25.191 -    val _ = Mutex.unlock serial_lock;
  25.192 -  in res end);
  25.193 -
  25.194 -end;
  25.195 -
  25.196 -end;
  25.197 -
  25.198 -structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
  25.199 -open Basic_Multithreading;
    26.1 --- a/src/Pure/RAW/secure.ML	Thu Mar 03 21:35:16 2016 +0100
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,27 +0,0 @@
    26.4 -(*  Title:      Pure/RAW/secure.ML
    26.5 -    Author:     Makarius
    26.6 -
    26.7 -Secure critical operations.
    26.8 -*)
    26.9 -
   26.10 -signature SECURE =
   26.11 -sig
   26.12 -  val set_secure: unit -> unit
   26.13 -  val is_secure: unit -> bool
   26.14 -  val deny: string -> unit
   26.15 -  val deny_ml: unit -> unit
   26.16 -end;
   26.17 -
   26.18 -structure Secure: SECURE =
   26.19 -struct
   26.20 -
   26.21 -val secure = Unsynchronized.ref false;
   26.22 -
   26.23 -fun set_secure () = secure := true;
   26.24 -fun is_secure () = ! secure;
   26.25 -
   26.26 -fun deny msg = if is_secure () then error msg else ();
   26.27 -
   26.28 -fun deny_ml () = deny "Cannot evaluate ML source in secure mode";
   26.29 -
   26.30 -end;
    27.1 --- a/src/Pure/RAW/unsynchronized.ML	Thu Mar 03 21:35:16 2016 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,30 +0,0 @@
    27.4 -(*  Title:      Pure/RAW/unsynchronized.ML
    27.5 -    Author:     Makarius
    27.6 -
    27.7 -Raw ML references as unsynchronized state variables.
    27.8 -*)
    27.9 -
   27.10 -structure Unsynchronized =
   27.11 -struct
   27.12 -
   27.13 -datatype ref = datatype ref;
   27.14 -
   27.15 -val op := = op :=;
   27.16 -val ! = !;
   27.17 -
   27.18 -fun change r f = r := f (! r);
   27.19 -fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
   27.20 -
   27.21 -fun inc i = (i := ! i + (1: int); ! i);
   27.22 -fun dec i = (i := ! i - (1: int); ! i);
   27.23 -
   27.24 -fun setmp flag value f x =
   27.25 -  uninterruptible (fn restore_attributes => fn () =>
   27.26 -    let
   27.27 -      val orig_value = ! flag;
   27.28 -      val _ = flag := value;
   27.29 -      val result = Exn.capture (restore_attributes f) x;
   27.30 -      val _ = flag := orig_value;
   27.31 -    in Exn.release result end) ();
   27.32 -
   27.33 -end;
    28.1 --- a/src/Pure/ROOT	Thu Mar 03 21:35:16 2016 +0100
    28.2 +++ b/src/Pure/ROOT	Thu Mar 03 21:59:21 2016 +0100
    28.3 @@ -1,39 +1,8 @@
    28.4  chapter Pure
    28.5  
    28.6 -session RAW =
    28.7 -  theories
    28.8 -  files
    28.9 -    "RAW/ROOT_polyml.ML"
   28.10 -    "RAW/exn.ML"
   28.11 -    "RAW/fixed_int_dummy.ML"
   28.12 -    "RAW/ml_compiler0.ML"
   28.13 -    "RAW/ml_debugger.ML"
   28.14 -    "RAW/ml_heap.ML"
   28.15 -    "RAW/ml_name_space.ML"
   28.16 -    "RAW/ml_pretty.ML"
   28.17 -    "RAW/ml_profiling.ML"
   28.18 -    "RAW/ml_system.ML"
   28.19 -    "RAW/multithreading.ML"
   28.20 -    "RAW/secure.ML"
   28.21 -    "RAW/unsynchronized.ML"
   28.22 -
   28.23  session Pure =
   28.24    global_theories Pure
   28.25    files
   28.26 -    "RAW/ROOT_polyml.ML"
   28.27 -    "RAW/exn.ML"
   28.28 -    "RAW/fixed_int_dummy.ML"
   28.29 -    "RAW/ml_compiler0.ML"
   28.30 -    "RAW/ml_debugger.ML"
   28.31 -    "RAW/ml_heap.ML"
   28.32 -    "RAW/ml_name_space.ML"
   28.33 -    "RAW/ml_pretty.ML"
   28.34 -    "RAW/ml_profiling.ML"
   28.35 -    "RAW/ml_system.ML"
   28.36 -    "RAW/multithreading.ML"
   28.37 -    "RAW/secure.ML"
   28.38 -    "RAW/unsynchronized.ML"
   28.39 -
   28.40      "Concurrent/bash.ML"
   28.41      "Concurrent/bash_windows.ML"
   28.42      "Concurrent/cache.ML"
   28.43 @@ -42,6 +11,7 @@
   28.44      "Concurrent/future.ML"
   28.45      "Concurrent/lazy.ML"
   28.46      "Concurrent/mailbox.ML"
   28.47 +    "Concurrent/multithreading.ML"
   28.48      "Concurrent/par_exn.ML"
   28.49      "Concurrent/par_list.ML"
   28.50      "Concurrent/random.ML"
   28.51 @@ -50,6 +20,7 @@
   28.52      "Concurrent/synchronized.ML"
   28.53      "Concurrent/task_queue.ML"
   28.54      "Concurrent/time_limit.ML"
   28.55 +    "Concurrent/unsynchronized.ML"
   28.56      "General/alist.ML"
   28.57      "General/antiquote.ML"
   28.58      "General/balanced_tree.ML"
   28.59 @@ -58,6 +29,7 @@
   28.60      "General/buffer.ML"
   28.61      "General/change_table.ML"
   28.62      "General/completion.ML"
   28.63 +    "General/exn.ML"
   28.64      "General/file.ML"
   28.65      "General/graph.ML"
   28.66      "General/graph_display.ML"
   28.67 @@ -77,6 +49,7 @@
   28.68      "General/queue.ML"
   28.69      "General/same.ML"
   28.70      "General/scan.ML"
   28.71 +    "General/secure.ML"
   28.72      "General/seq.ML"
   28.73      "General/sha1.ML"
   28.74      "General/sha1_polyml.ML"
   28.75 @@ -130,17 +103,25 @@
   28.76      "ML/exn_debugger.ML"
   28.77      "ML/exn_output.ML"
   28.78      "ML/exn_properties.ML"
   28.79 +    "ML/fixed_int_dummy.ML"
   28.80      "ML/install_pp_polyml.ML"
   28.81      "ML/ml_antiquotation.ML"
   28.82      "ML/ml_compiler.ML"
   28.83 +    "ML/ml_compiler0.ML"
   28.84      "ML/ml_context.ML"
   28.85 +    "ML/ml_debugger.ML"
   28.86      "ML/ml_env.ML"
   28.87      "ML/ml_file.ML"
   28.88 +    "ML/ml_heap.ML"
   28.89      "ML/ml_lex.ML"
   28.90 +    "ML/ml_name_space.ML"
   28.91      "ML/ml_options.ML"
   28.92 +    "ML/ml_pretty.ML"
   28.93 +    "ML/ml_profiling.ML"
   28.94      "ML/ml_statistics.ML"
   28.95      "ML/ml_statistics_dummy.ML"
   28.96      "ML/ml_syntax.ML"
   28.97 +    "ML/ml_system.ML"
   28.98      "PIDE/active.ML"
   28.99      "PIDE/command.ML"
  28.100      "PIDE/command_span.ML"
    29.1 --- a/src/Pure/ROOT.ML	Thu Mar 03 21:35:16 2016 +0100
    29.2 +++ b/src/Pure/ROOT.ML	Thu Mar 03 21:59:21 2016 +0100
    29.3 @@ -1,6 +1,14 @@
    29.4 -(*** Isabelle/Pure bootstrap from "RAW" environment ***)
    29.5 +(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
    29.6 +
    29.7 +(** bootstrap phase 0: Poly/ML setup **)
    29.8 +
    29.9 +(* initial ML name space *)
   29.10  
   29.11 -(** bootstrap phase 0: towards ML within position context *)
   29.12 +use "ML/ml_system.ML";
   29.13 +use "ML/ml_name_space.ML";
   29.14 +
   29.15 +if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
   29.16 +else use "ML/fixed_int_dummy.ML";
   29.17  
   29.18  structure Distribution =     (*filled-in by makedist*)
   29.19  struct
   29.20 @@ -10,6 +18,87 @@
   29.21  end;
   29.22  
   29.23  
   29.24 +(* multithreading *)
   29.25 +
   29.26 +use "General/exn.ML";
   29.27 +
   29.28 +val seconds = Time.fromReal;
   29.29 +
   29.30 +open Thread;
   29.31 +use "Concurrent/multithreading.ML";
   29.32 +
   29.33 +use "Concurrent/unsynchronized.ML";
   29.34 +val _ = PolyML.Compiler.forgetValue "ref";
   29.35 +val _ = PolyML.Compiler.forgetType "ref";
   29.36 +
   29.37 +
   29.38 +(* pervasive environment *)
   29.39 +
   29.40 +val _ = PolyML.Compiler.forgetValue "isSome";
   29.41 +val _ = PolyML.Compiler.forgetValue "getOpt";
   29.42 +val _ = PolyML.Compiler.forgetValue "valOf";
   29.43 +val _ = PolyML.Compiler.forgetValue "foldl";
   29.44 +val _ = PolyML.Compiler.forgetValue "foldr";
   29.45 +val _ = PolyML.Compiler.forgetValue "print";
   29.46 +val _ = PolyML.Compiler.forgetValue "explode";
   29.47 +val _ = PolyML.Compiler.forgetValue "concat";
   29.48 +
   29.49 +val ord = SML90.ord;
   29.50 +val chr = SML90.chr;
   29.51 +val raw_explode = SML90.explode;
   29.52 +val implode = SML90.implode;
   29.53 +
   29.54 +fun quit () = exit 0;
   29.55 +
   29.56 +
   29.57 +(* ML runtime system *)
   29.58 +
   29.59 +use "ML/ml_heap.ML";
   29.60 +use "ML/ml_profiling.ML";
   29.61 +
   29.62 +val pointer_eq = PolyML.pointerEq;
   29.63 +
   29.64 +
   29.65 +(* ML toplevel pretty printing *)
   29.66 +
   29.67 +use "ML/ml_pretty.ML";
   29.68 +
   29.69 +local
   29.70 +  val depth = Unsynchronized.ref 10;
   29.71 +in
   29.72 +  fun get_default_print_depth () = ! depth;
   29.73 +  fun default_print_depth n = (depth := n; PolyML.print_depth n);
   29.74 +  val _ = default_print_depth 10;
   29.75 +end;
   29.76 +
   29.77 +val error_depth = PolyML.error_depth;
   29.78 +
   29.79 +
   29.80 +(* ML compiler *)
   29.81 +
   29.82 +use "General/secure.ML";
   29.83 +use "ML/ml_compiler0.ML";
   29.84 +
   29.85 +PolyML.Compiler.reportUnreferencedIds := true;
   29.86 +PolyML.Compiler.reportExhaustiveHandlers := true;
   29.87 +PolyML.Compiler.printInAlphabeticalOrder := false;
   29.88 +PolyML.Compiler.maxInlineSize := 80;
   29.89 +PolyML.Compiler.prompt1 := "ML> ";
   29.90 +PolyML.Compiler.prompt2 := "ML# ";
   29.91 +
   29.92 +fun ml_make_string struct_name =
   29.93 +  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
   29.94 +    struct_name ^ ".ML_print_depth ()))))))";
   29.95 +
   29.96 +
   29.97 +(* ML debugger *)
   29.98 +
   29.99 +use_no_debug "ML/ml_debugger.ML";
  29.100 +
  29.101 +
  29.102 +
  29.103 +(** bootstrap phase 1: towards ML within position context *)
  29.104 +
  29.105  (* library of general tools *)
  29.106  
  29.107  use "General/basics.ML";
  29.108 @@ -52,7 +141,7 @@
  29.109  
  29.110  
  29.111  
  29.112 -(** bootstrap phase 1: towards ML within Isar context *)
  29.113 +(** bootstrap phase 2: towards ML within Isar context *)
  29.114  
  29.115  (* library of general tools *)
  29.116  
  29.117 @@ -236,7 +325,7 @@
  29.118  
  29.119  
  29.120  
  29.121 -(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
  29.122 +(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
  29.123  
  29.124  (*basic proof engine*)
  29.125  use "par_tactical.ML";
    30.1 --- a/src/Pure/Tools/build.scala	Thu Mar 03 21:35:16 2016 +0100
    30.2 +++ b/src/Pure/Tools/build.scala	Thu Mar 03 21:59:21 2016 +0100
    30.3 @@ -54,7 +54,7 @@
    30.4      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    30.5    }
    30.6  
    30.7 -  def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    30.8 +  def is_pure(name: String): Boolean = name == "Pure"
    30.9  
   30.10    def session_info(options: Options, select: Boolean, dir: Path,
   30.11        chapter: String, entry: Session_Entry): (String, Session_Info) =
   30.12 @@ -581,33 +581,13 @@
   30.13        """
   30.14        . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   30.15        """ +
   30.16 -      (if (is_pure(name)) {
   30.17 -        val ml_system = Isabelle_System.getenv("ML_SYSTEM")
   30.18 -        val ml_system_base = Library.space_explode('-', ml_system).headOption getOrElse ml_system
   30.19 -        val ml_root =
   30.20 -          List(ml_system, ml_system_base).map(a => "RAW/ROOT_" + a + ".ML").
   30.21 -            find(b => Path.explode("~~/src/Pure/" + b).file.isFile) getOrElse
   30.22 -            error("Missing compatibility file for ML system " + quote(ml_system))
   30.23 -
   30.24 -        if (name == "RAW") {
   30.25 -          """
   30.26 -            rm -f "$OUTPUT"
   30.27 -            "$ISABELLE_PROCESS" \
   30.28 -              -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
   30.29 -              -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
   30.30 -              -q RAW_ML_SYSTEM
   30.31 -          """
   30.32 -        }
   30.33 -        else {
   30.34 -          """
   30.35 -            rm -f "$OUTPUT"
   30.36 -            "$ISABELLE_PROCESS" \
   30.37 -              -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
   30.38 -              -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
   30.39 -              -q RAW_ML_SYSTEM
   30.40 -          """
   30.41 -        }
   30.42 -      }
   30.43 +      (if (is_pure(name))
   30.44 +        """
   30.45 +          rm -f "$OUTPUT"
   30.46 +          "$ISABELLE_PROCESS" -f "ROOT.ML" \
   30.47 +            -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
   30.48 +            -q RAW_ML_SYSTEM
   30.49 +        """
   30.50        else
   30.51          """
   30.52          rm -f "$OUTPUT"
    31.1 --- a/src/Pure/build-jars	Thu Mar 03 21:35:16 2016 +0100
    31.2 +++ b/src/Pure/build-jars	Thu Mar 03 21:59:21 2016 +0100
    31.3 @@ -28,6 +28,7 @@
    31.4    General/antiquote.scala
    31.5    General/bytes.scala
    31.6    General/completion.scala
    31.7 +  General/exn.scala
    31.8    General/file.scala
    31.9    General/graph.scala
   31.10    General/graph_display.scala
   31.11 @@ -71,7 +72,6 @@
   31.12    PIDE/text.scala
   31.13    PIDE/xml.scala
   31.14    PIDE/yxml.scala
   31.15 -  RAW/exn.scala
   31.16    ROOT.scala
   31.17    System/command_line.scala
   31.18    System/cygwin.scala