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