--- a/src/Pure/General/exn.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-(* Title: Pure/General/exn.ML
- Author: Makarius
-
-Support for exceptions.
-*)
-
-signature EXN =
-sig
- 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
-end;
-
-structure Exn: EXN =
-struct
-
-(* 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 = 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;
-
-end;
-
-datatype illegal = Interrupt;
-
--- a/src/Pure/General/exn.scala Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-/* Title: Pure/General/exn.scala
- Module: PIDE
- Author: Makarius
-
-Support for exceptions (arbitrary throwables).
-*/
-
-package isabelle
-
-
-object Exn
-{
- /* 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[Library.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/ML-Systems/compiler_polyml.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: Pure/ML-Systems/compiler_polyml.ML
-
-Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
-*)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- {line, file, verbose, debug} text =
- let
- val current_line = Unsynchronized.ref line;
- val in_buffer =
- Unsynchronized.ref (String.explode (tune_source (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" ^ str_of_pos 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] @
- ML_Compiler_Parameters.debug debug;
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); 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;
-
-end;
--- a/src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
- Author: Makarius
-
-Exception trace for Poly/ML 5.5.1 via ML output.
-*)
-
-fun print_exception_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);
-
-PolyML.Compiler.reportExhaustiveHandlers := true;
-
--- a/src/Pure/ML-Systems/ml_compiler_parameters.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: Pure/ML/ml_compiler_parameters.ML
- Author: Makarius
-
-Additional ML compiler parameters for Poly/ML.
-*)
-
-signature ML_COMPILER_PARAMETERS =
-sig
- val debug: bool -> PolyML.Compiler.compilerParameters list
-end;
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug _ = [];
-
-end;
\ No newline at end of file
--- a/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(* Title: Pure/ML/ml_compiler_parameters_polyml-5.6.ML
- Author: Makarius
-
-Additional ML compiler parameters for Poly/ML 5.6, or later.
-*)
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug b = [PolyML.Compiler.CPDebug b];
-
-end;
\ No newline at end of file
--- a/src/Pure/ML-Systems/ml_debugger.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(* Title: Pure/ML/ml_debugger.ML
- Author: Makarius
-
-ML debugger interface -- dummy version.
-*)
-
-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
- 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
-with
-
-fun exn_id exn = Exn_Id (General.exnName exn);
-fun print_exn_id (Exn_Id name) = name;
-fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2; (*over-approximation*)
-
-end;
-
-
-(* hooks *)
-
-fun on_entry _ = ();
-fun on_exit _ = ();
-fun on_exit_exception _ = ();
-fun on_breakpoint _ = ();
-
-
-(* debugger *)
-
-fun fail () = raise Fail "No debugger support on this ML platform";
-
-type state = unit;
-
-fun state _ = [];
-fun debug_function () = fail ();
-fun debug_function_arg () = fail ();
-fun debug_function_result () = fail ();
-fun debug_location () = fail ();
-fun debug_name_space () = fail ();
-fun debug_local_name_space () = fail ();
-
-end;
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(* Title: Pure/ML-Systems/ml_debugger_polyml-5.6.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 (ML_Pretty.String (s, 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/ML-Systems/ml_name_space.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(* Title: Pure/ML-Systems/ml_name_space.ML
- Author: Makarius
-
-ML name space -- dummy version of Poly/ML 5.2 facility.
-*)
-
-structure ML_Name_Space =
-struct
-
-type valueVal = unit;
-type typeVal = unit;
-type fixityVal = unit;
-type structureVal = unit;
-type signatureVal = unit;
-type functorVal = unit;
-
-type T =
- {lookupVal: string -> valueVal option,
- lookupType: string -> typeVal option,
- lookupFix: string -> fixityVal option,
- lookupStruct: string -> structureVal option,
- lookupSig: string -> signatureVal option,
- lookupFunct: string -> functorVal option,
- enterVal: string * valueVal -> unit,
- enterType: string * typeVal -> unit,
- enterFix: string * fixityVal -> unit,
- enterStruct: string * structureVal -> unit,
- enterSig: string * signatureVal -> unit,
- enterFunct: string * functorVal -> unit,
- allVal: unit -> (string * valueVal) list,
- allType: unit -> (string * typeVal) list,
- allFix: unit -> (string * fixityVal) list,
- allStruct: unit -> (string * structureVal) list,
- allSig: unit -> (string * signatureVal) list,
- allFunct: unit -> (string * functorVal) list};
-
-val global: T =
- {lookupVal = fn _ => NONE,
- lookupType = fn _ => NONE,
- lookupFix = fn _ => NONE,
- lookupStruct = fn _ => NONE,
- lookupSig = fn _ => NONE,
- lookupFunct = fn _ => NONE,
- enterVal = fn _ => (),
- enterType = fn _ => (),
- enterFix = fn _ => (),
- enterStruct = fn _ => (),
- enterSig = fn _ => (),
- enterFunct = fn _ => (),
- allVal = fn _ => [],
- allType = fn _ => [],
- allFix = fn _ => [],
- allStruct = fn _ => [],
- allSig = fn _ => [],
- allFunct = fn _ => []};
-
-val initial_val : (string * valueVal) list = [];
-val initial_type : (string * typeVal) list = [];
-val initial_fixity : (string * fixityVal) list = [];
-val initial_structure : (string * structureVal) list = [];
-val initial_signature : (string * signatureVal) list = [];
-val initial_functor : (string * functorVal) list = [];
-
-fun forget_global_structure (_: string) = ();
-
-fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
-
-end;
--- a/src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Pure/ML-Systems/ml_name_space_polyml-5.6.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);
-
- type typeVal = TypeConstrs.typeConstr;
- fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-
- type fixityVal = Infixes.fixity;
- fun displayFix (_: string, x) = Infixes.print x;
-
- type structureVal = Structures.structureVal;
- fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-
- type signatureVal = Signatures.signatureVal;
- fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-
- type functorVal = Functors.functorVal;
- fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-end;
--- a/src/Pure/ML-Systems/ml_name_space_polyml.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: Pure/ML-Systems/ml_name_space_polyml.ML
- Author: Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = nameSpace;
- val global = PolyML.globalNameSpace;
- val forget_global_structure = PolyML.Compiler.forgetStructure;
-end;
--- a/src/Pure/ML-Systems/ml_parse_tree.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/ML/ml_parse_tree.ML
- Author: Makarius
-
-Additional ML parse tree components for Poly/ML.
-*)
-
-signature ML_PARSE_TREE =
-sig
- val completions: PolyML.ptProperties -> string list option
- val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
-end;
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions _ = NONE;
-fun breakpoint _ = NONE;
-
-end;
\ No newline at end of file
--- a/src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML
- Author: Makarius
-
-Additional ML parse tree components for Poly/ML 5.6, or later.
-*)
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions (PolyML.PTcompletions x) = SOME x
- | completions _ = NONE;
-
-fun breakpoint (PolyML.PTbreakPoint x) = SOME x
- | breakpoint _ = NONE;
-
-end;
\ No newline at end of file
--- a/src/Pure/ML-Systems/ml_positions.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/ML-Systems/ml_positions.ML
- Author: Makarius
-
-Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
-*)
-
-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;
-
--- a/src/Pure/ML-Systems/ml_pretty.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: Pure/ML-Systems/ml_pretty.ML
- Author: Makarius
-
-Minimal support for raw ML pretty printing -- for boot-strapping only.
-*)
-
-structure ML_Pretty =
-struct
-
-datatype pretty =
- Block of (string * string) * bool * int * pretty list |
- String of string * int |
- Break of bool * int * int;
-
-fun block prts = Block (("", ""), false, 2, prts);
-fun str s = String (s, size s);
-fun brk width = Break (false, width, 0);
-
-fun pair pretty1 pretty2 ((x, y), depth: int) =
- block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
-
-fun enum sep lpar rpar pretty (args, depth) =
- 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 (Int.max (depth, 0)) args @ [str rpar])) end;
-
-end;
--- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/ML-Systems/ml_profiling_polyml-5.6.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/ML-Systems/ml_profiling_polyml.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: Pure/ML-Systems/ml_profiling_polyml.ML
- Author: Makarius
-
-Profiling for Poly/ML.
-*)
-
-structure ML_Profiling =
-struct
-
-local
-
-fun profile n f x =
- let
- val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
- val res = Exn.capture f x;
- val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
- in Exn.release res end;
-
-in
-
-fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
-fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
-fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
-
-end;
-
-end;
--- a/src/Pure/ML-Systems/ml_stack_dummy.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/ML-Systems/ml_stack_dummy.ML
-
-Maximum stack size (in words) for ML threads -- dummy version.
-*)
-
-signature ML_STACK =
-sig
- val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit (_: int option) : Thread.threadAttribute list = [];
-
-end;
--- a/src/Pure/ML-Systems/ml_stack_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/ML-Systems/ml_stack_polyml-5.6.ML
-
-Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
-*)
-
-signature ML_STACK =
-sig
- val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit m = [Thread.MaximumMLStack m];
-
-end;
--- a/src/Pure/ML-Systems/ml_system.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Pure/ML-Systems/ml_system.ML
- Author: Makarius
-
-ML system and platform operations.
-*)
-
-signature ML_SYSTEM =
-sig
- val name: string
- val is_polyml: bool
- val is_smlnj: bool
- val platform: string
- val platform_is_windows: bool
- val share_common_data: unit -> unit
- val save_state: string -> unit
-end;
-
-structure ML_System: ML_SYSTEM =
-struct
-
-val SOME name = OS.Process.getEnv "ML_SYSTEM";
-val is_polyml = String.isPrefix "polyml" name;
-val is_smlnj = String.isPrefix "smlnj" name;
-
-val SOME platform = OS.Process.getEnv "ML_PLATFORM";
-val platform_is_windows = String.isSuffix "windows" platform;
-
-fun share_common_data () = ();
-fun save_state _ = raise Fail "Cannot save state -- undefined operation";
-
-end;
-
--- a/src/Pure/ML-Systems/multithreading.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(* Title: Pure/ML-Systems/multithreading.ML
- Author: Makarius
-
-Dummy implementation of multithreading setup.
-*)
-
-signature MULTITHREADING =
-sig
- val available: bool
- 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 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 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
-
-(* options *)
-
-val available = false;
-fun max_threads_value () = 1: int;
-fun max_threads_update _ = ();
-fun max_threads_setmp _ f x = f x;
-fun enabled () = false;
-
-
-(* attributes *)
-
-val no_interrupts = [];
-val public_interrupts = [];
-val private_interrupts = [];
-fun sync_interrupts _ = [];
-
-fun interrupted () = ();
-
-fun with_attributes _ e = e [];
-
-fun sync_wait _ _ _ _ = Exn.Res true;
-
-
-(* tracing *)
-
-val trace = ref (0: int);
-fun tracing _ _ = ();
-fun tracing_time _ _ _ = ();
-fun real_time f x = (f x; Time.zeroTime);
-
-
-(* synchronized evaluation *)
-
-fun synchronized _ _ e = e ();
-
-
-(* serial numbers *)
-
-local val count = ref (0: int)
-in fun serial () = (count := ! count + 1; ! count) end;
-
-end;
-
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(* Title: Pure/ML-Systems/multithreading_polyml.ML
- Author: Makarius
-
-Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
-*)
-
-signature MULTITHREADING =
-sig
- include MULTITHREADING
- val interruptible: ('a -> 'b) -> 'a -> 'b
- val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-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 *)
-
-val available = true;
-
-fun max_threads_result m =
- if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 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;
-
-val interruptible = Multithreading.interruptible;
-val uninterruptible = Multithreading.uninterruptible;
-
--- a/src/Pure/ML-Systems/overloading_smlnj.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: Pure/ML-Systems/overloading_smlnj.ML
- Author: Makarius
-
-Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
-*)
-
-Control.overloadKW := true;
-
-overload ~ : ('a -> 'a) as
- IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
- Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
-overload + : ('a * 'a -> 'a) as
- IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
- Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
-overload - : ('a * 'a -> 'a) as
- IntInf.- and Int31.- and Int32.- and Int64.- and
- Word.- and Word8.- and Word32.- and Word64.- and Real.-;
-overload * : ('a * 'a -> 'a) as
- IntInf.* and Int31.* and Int32.* and Int64.* and
- Word.* and Word8.* and Word32.* and Word64.* and Real.*;
-overload div: ('a * 'a -> 'a) as
- IntInf.div and Int31.div and Int32.div and Int64.div and
- Word.div and Word8.div and Word32.div and Word64.div;
-overload mod: ('a * 'a -> 'a) as
- IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
- Word.mod and Word8.mod and Word32.mod and Word64.mod;
-overload < : ('a * 'a -> bool) as
- IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
- Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
-overload <= : ('a * 'a -> bool) as
- IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
- Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
-overload > : ('a * 'a -> bool) as
- IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
- Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
-overload >= : ('a * 'a -> bool) as
- IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
- Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
-overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
-
-Control.overloadKW := false;
--- a/src/Pure/ML-Systems/polyml-5.5.2.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.5.2.ML
- Author: Makarius
-
-Compatibility wrapper for Poly/ML 5.5.2.
-*)
-
-structure Thread =
-struct
- open Thread;
-
- structure Thread =
- struct
- open Thread;
-
- fun numProcessors () =
- (case Thread.numPhysicalProcessors () of
- SOME n => n
- | NONE => Thread.numProcessors ());
- end;
-end;
-
-use "ML-Systems/polyml.ML";
-
--- a/src/Pure/ML-Systems/polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.6.ML
- Author: Makarius
-
-Compatibility wrapper for Poly/ML 5.6.
-*)
-
-structure Thread =
-struct
- open Thread;
-
- structure Thread =
- struct
- open Thread;
-
- fun numProcessors () =
- (case Thread.numPhysicalProcessors () of
- SOME n => n
- | NONE => Thread.numProcessors ());
- end;
-end;
-
-use "ML-Systems/polyml.ML";
--- a/src/Pure/ML-Systems/polyml.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-(* Title: Pure/ML-Systems/polyml.ML
- Author: Makarius
-
-Compatibility wrapper for Poly/ML.
-*)
-
-(* initial ML name space *)
-
-use "ML-Systems/ml_system.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_name_space_polyml-5.6.ML"
-else use "ML-Systems/ml_name_space_polyml.ML";
-
-structure ML_Name_Space =
-struct
- open ML_Name_Space;
- val initial_val =
- List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
- (#allVal global ());
- val initial_type = #allType global ();
- val initial_fixity = #allFix global ();
- val initial_structure = #allStruct global ();
- val initial_signature = #allSig global ();
- val initial_functor = #allFunct global ();
-end;
-
-
-(* ML system operations *)
-
-if ML_System.name = "polyml-5.3.0"
-then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
-else ();
-
-fun ml_platform_path (s: string) = s;
-fun ml_standard_path (s: string) = s;
-
-if ML_System.platform_is_windows then use "ML-Systems/windows_path.ML" else ();
-
-structure ML_System =
-struct
- open ML_System;
- fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
- val save_state = PolyML.SaveState.saveState o ml_platform_path;
-end;
-
-
-(* exceptions *)
-
-fun reraise exn =
- (case PolyML.exceptionLocation exn of
- NONE => raise exn
- | SOME location => PolyML.raiseWithLocation (exn, location));
-
-exception Interrupt = SML90.Interrupt;
-
-use "General/exn.ML";
-
-fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
-
-if ML_System.name = "polyml-5.5.1"
- orelse ML_System.name = "polyml-5.5.2"
- orelse ML_System.name = "polyml-5.6"
-then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
-else ();
-
-
-(* multithreading *)
-
-val seconds = Time.fromReal;
-
-if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
-then ()
-else use "ML-Systems/single_assignment_polyml.ML";
-
-open Thread;
-use "ML-Systems/multithreading.ML";
-use "ML-Systems/multithreading_polyml.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_stack_polyml-5.6.ML"
-else use "ML-Systems/ml_stack_dummy.ML";
-
-use "ML-Systems/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;
-
-val io_buffer_size = 4096;
-
-fun quit () = exit 0;
-
-
-(* ML runtime system *)
-
-if ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_profiling_polyml-5.6.ML"
-else use "ML-Systems/ml_profiling_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-
-(* ML toplevel pretty printing *)
-
-use "ML-Systems/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;
-
-val pretty_ml =
- let
- fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
- | convert _ (PolyML.PrettyBlock (_, _,
- [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
- ML_Pretty.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 ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
- | convert len (PolyML.PrettyString s) =
- ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
- in convert "" end;
-
-fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
- | ml_pretty (ML_Pretty.Break (true, _, _)) =
- PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
- [PolyML.PrettyString " "])
- | ml_pretty (ML_Pretty.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 ml_pretty prts) end
- | ml_pretty (ML_Pretty.String (s, len)) =
- if len = size s then PolyML.PrettyString s
- else PolyML.PrettyBlock
- (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
-
-
-(* ML compiler *)
-
-structure ML_Name_Space =
-struct
- open ML_Name_Space;
- val display_val = pretty_ml o displayVal;
-end;
-
-use "ML-Systems/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" else ();
-
-use "ML-Systems/use_context.ML";
-use "ML-Systems/ml_positions.ML";
-use "ML-Systems/compiler_polyml.ML";
-
-PolyML.Compiler.reportUnreferencedIds := true;
-PolyML.Compiler.printInAlphabeticalOrder := false;
-PolyML.Compiler.maxInlineSize := 80;
-
-fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-
-use "ML-Systems/ml_parse_tree.ML";
-if ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_parse_tree_polyml-5.6.ML" else ();
-
-fun toplevel_pp context (_: string list) pp =
- use_text context {line = 1, file = "pp", verbose = false, debug = false}
- ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
-
-fun ml_make_string struct_name =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
- struct_name ^ ".ML_print_depth ())))))";
-
-
-(* ML debugger *)
-
-if ML_System.name = "polyml-5.6"
-then use "ML-Systems/ml_debugger_polyml-5.6.ML"
-else use "ML-Systems/ml_debugger.ML";
--- a/src/Pure/ML-Systems/pp_dummy.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/ML-Systems/pp_dummy.ML
-
-Dummy setup for toplevel pretty printing.
-*)
-
-fun ml_pretty _ = raise Fail "ml_pretty dummy";
-fun pretty_ml _ = raise Fail "pretty_ml dummy";
-
-structure PolyML =
-struct
- fun addPrettyPrinter _ = ();
- fun prettyRepresentation _ =
- raise Fail "PolyML.prettyRepresentation dummy";
- open PolyML;
-end;
-
--- a/src/Pure/ML-Systems/proper_int.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,289 +0,0 @@
-(* Title: Pure/ML-Systems/proper_int.ML
- Author: Makarius
-
-SML basis with type int representing proper integers, not machine
-words.
-*)
-
-val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
-val dest_int = IntInf.toInt: IntInf.int -> Int.int;
-
-
-(* Int *)
-
-type int = IntInf.int;
-
-structure IntInf =
-struct
- open IntInf;
- fun fromInt (a: int) = a;
- fun toInt (a: int) = a;
- val log2 = mk_int o IntInf.log2;
- val sign = mk_int o IntInf.sign;
-end;
-
-structure Int = IntInf;
-
-
-(* List *)
-
-structure List =
-struct
- open List;
- fun length a = mk_int (List.length a);
- fun nth (a, b) = List.nth (a, dest_int b);
- fun take (a, b) = List.take (a, dest_int b);
- fun drop (a, b) = List.drop (a, dest_int b);
- fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
-end;
-
-val length = List.length;
-
-
-(* Array *)
-
-structure Array =
-struct
- open Array;
- val maxLen = mk_int Array.maxLen;
- fun array (a, b) = Array.array (dest_int a, b);
- fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
- fun length a = mk_int (Array.length a);
- fun sub (a, b) = Array.sub (a, dest_int b);
- fun update (a, b, c) = Array.update (a, dest_int b, c);
- fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
- fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
- fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
- fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
- fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun findi a b =
- (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
- NONE => NONE
- | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* Vector *)
-
-structure Vector =
-struct
- open Vector;
- val maxLen = mk_int Vector.maxLen;
- fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
- fun length a = mk_int (Vector.length a);
- fun sub (a, b) = Vector.sub (a, dest_int b);
- fun update (a, b, c) = Vector.update (a, dest_int b, c);
- fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
- fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
- fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun findi a b =
- (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
- NONE => NONE
- | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* CharVector *)
-
-structure CharVector =
-struct
- open CharVector;
- fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
-end;
-
-
-(* Word8VectorSlice *)
-
-structure Word8VectorSlice =
-struct
- open Word8VectorSlice;
- val length = mk_int o Word8VectorSlice.length;
- fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
-end;
-
-
-(* Char *)
-
-structure Char =
-struct
- open Char;
- val maxOrd = mk_int Char.maxOrd;
- val chr = Char.chr o dest_int;
- val ord = mk_int o Char.ord;
-end;
-
-val chr = Char.chr;
-val ord = Char.ord;
-
-
-(* String *)
-
-structure String =
-struct
- open String;
- val maxSize = mk_int String.maxSize;
- val size = mk_int o String.size;
- fun sub (a, b) = String.sub (a, dest_int b);
- fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
- fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
-end;
-
-val size = String.size;
-val substring = String.substring;
-
-
-(* Substring *)
-
-structure Substring =
-struct
- open Substring;
- fun sub (a, b) = Substring.sub (a, dest_int b);
- val size = mk_int o Substring.size;
- fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
- fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
- fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
- fun triml a b = Substring.triml (dest_int a) b;
- fun trimr a b = Substring.trimr (dest_int a) b;
- fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
- fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
-end;
-
-
-(* StringCvt *)
-
-structure StringCvt =
-struct
- open StringCvt;
- datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
- fun realfmt fmt = Real.fmt
- (case fmt of
- EXACT => StringCvt.EXACT
- | FIX NONE => StringCvt.FIX NONE
- | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
- | GEN NONE => StringCvt.GEN NONE
- | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
- | SCI NONE => StringCvt.SCI NONE
- | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
- fun padRight a b c = StringCvt.padRight a (dest_int b) c;
- fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
-end;
-
-
-(* Word *)
-
-structure Word =
-struct
- open Word;
- val wordSize = mk_int Word.wordSize;
- val toInt = Word.toLargeInt;
- val toIntX = Word.toLargeIntX;
- val fromInt = Word.fromLargeInt;
-end;
-
-structure Word8 =
-struct
- open Word8;
- val wordSize = mk_int Word8.wordSize;
- val toInt = Word8.toLargeInt;
- val toIntX = Word8.toLargeIntX;
- val fromInt = Word8.fromLargeInt;
-end;
-
-structure Word32 =
-struct
- open Word32;
- val wordSize = mk_int Word32.wordSize;
- val toInt = Word32.toLargeInt;
- val toIntX = Word32.toLargeIntX;
- val fromInt = Word32.fromLargeInt;
-end;
-
-structure LargeWord =
-struct
- open LargeWord;
- val wordSize = mk_int LargeWord.wordSize;
- val toInt = LargeWord.toLargeInt;
- val toIntX = LargeWord.toLargeIntX;
- val fromInt = LargeWord.fromLargeInt;
-end;
-
-
-(* Real *)
-
-structure Real =
-struct
- open Real;
- val radix = mk_int Real.radix;
- val precision = mk_int Real.precision;
- fun sign a = mk_int (Real.sign a);
- fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
- fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
- val ceil = mk_int o Real.ceil;
- val floor = mk_int o Real.floor;
- val real = Real.fromInt o dest_int;
- val round = mk_int o Real.round;
- val trunc = mk_int o Real.trunc;
- fun toInt a b = mk_int (Real.toInt a b);
- fun fromInt a = Real.fromInt (dest_int a);
- val fmt = StringCvt.realfmt;
-end;
-
-val ceil = Real.ceil;
-val floor = Real.floor;
-val real = Real.real;
-val round = Real.round;
-val trunc = Real.trunc;
-
-
-(* TextIO *)
-
-structure TextIO =
-struct
- open TextIO;
- fun inputN (a, b) = TextIO.inputN (a, dest_int b);
- fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
-end;
-
-
-(* BinIO *)
-
-structure BinIO =
-struct
- open BinIO;
- fun inputN (a, b) = BinIO.inputN (a, dest_int b);
- fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
-end;
-
-
-(* Time *)
-
-structure Time =
-struct
- open Time;
- fun fmt a b = Time.fmt (dest_int a) b;
-end;
-
-
-(* Sockets *)
-
-structure INetSock =
-struct
- open INetSock;
- fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
- fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
-end;
-
-
-(* OS.FileSys *)
-
-structure OS =
-struct
- open OS;
- structure FileSys =
- struct
- open FileSys;
- fun fileSize a = mk_int (FileSys.fileSize a);
- end;
-end;
--- a/src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: Pure/ML-Systems/share_common_data_polyml-5.3.0.ML
-
-Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
-anymore.
-*)
-
-structure PolyML =
-struct
- open PolyML;
- fun shareCommonData _ = ();
-end;
--- a/src/Pure/ML-Systems/single_assignment.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Pure/ML-Systems/single_assignment.ML
- Author: Makarius
-
-References with single assignment. Unsynchronized!
-*)
-
-signature SINGLE_ASSIGNMENT =
-sig
- type 'a saref
- exception Locked
- val saref: unit -> 'a saref
- val savalue: 'a saref -> 'a option
- val saset: 'a saref * 'a -> unit
-end;
-
-structure SingleAssignment: SINGLE_ASSIGNMENT =
-struct
-
-exception Locked;
-
-abstype 'a saref = SARef of 'a option ref
-with
-
-fun saref () = SARef (ref NONE);
-
-fun savalue (SARef r) = ! r;
-
-fun saset (SARef (r as ref NONE), x) = r := SOME x
- | saset _ = raise Locked;
-
-end;
-
-end;
--- a/src/Pure/ML-Systems/single_assignment_polyml.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: Pure/ML-Systems/single_assignment_polyml.ML
- Author: Makarius
-
-References with single assignment. Unsynchronized! Emulates
-structure SingleAssignment from Poly/ML 5.4.
-*)
-
-signature SINGLE_ASSIGNMENT =
-sig
- type 'a saref
- exception Locked
- val saref: unit -> 'a saref
- val savalue: 'a saref -> 'a option
- val saset: 'a saref * 'a -> unit
-end;
-
-structure SingleAssignment: SINGLE_ASSIGNMENT =
-struct
-
-exception Locked;
-
-abstype 'a saref = SARef of 'a option ref
-with
-
-fun saref () = SARef (ref NONE);
-
-fun savalue (SARef r) = ! r;
-
-fun saset (SARef (r as ref NONE), x) =
- (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
- | saset _ = raise Locked;
-
-end;
-
-end;
--- a/src/Pure/ML-Systems/smlnj.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-(* Title: Pure/ML-Systems/smlnj.ML
-
-Compatibility file for Standard ML of New Jersey.
-*)
-
-val io_buffer_size = 4096;
-use "ML-Systems/proper_int.ML";
-
-exception Interrupt;
-fun reraise exn = raise exn;
-
-fun exit rc = Posix.Process.exit (Word8.fromInt rc);
-fun quit () = exit 0;
-
-use "ML-Systems/overloading_smlnj.ML";
-use "General/exn.ML";
-use "ML-Systems/single_assignment.ML";
-use "ML-Systems/universal.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/multithreading.ML";
-use "ML-Systems/ml_stack_dummy.ML";
-use "ML-Systems/ml_pretty.ML";
-use "ML-Systems/ml_name_space.ML";
-structure PolyML = struct end;
-use "ML-Systems/pp_dummy.ML";
-use "ML-Systems/use_context.ML";
-use "ML-Systems/ml_positions.ML";
-
-
-val seconds = Time.fromReal;
-
-(*low-level pointer equality*)
-CM.autoload "$smlnj/init/init.cmi";
-val pointer_eq = InlineT.ptreql;
-
-
-(* restore old-style character / string functions *)
-
-val ord = mk_int o SML90.ord;
-val chr = SML90.chr o dest_int;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-
-(* New Jersey ML parameters *)
-
-val _ =
- (Control.Print.printLength := 1000;
- Control.Print.printDepth := 350;
- Control.Print.stringDepth := 250;
- Control.Print.signatures := 2;
- Control.MC.matchRedundantError := false);
-
-
-(* Poly/ML emulation *)
-
-(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
-local
- val depth = ref (10: int);
-in
- fun get_default_print_depth () = ! depth;
- fun default_print_depth n =
- (depth := n;
- Control.Print.printDepth := dest_int n div 2;
- Control.Print.printLength := dest_int n);
- val _ = default_print_depth 10;
-end;
-
-fun ml_make_string (_: string) = "(fn _ => \"?\")";
-
-
-(*prompts*)
-fun ml_prompts p1 p2 =
- (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
-
-(*dummy implementation*)
-structure ML_Profiling =
-struct
- fun profile_time (_: (int * string) list -> unit) f x = f x;
- fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
- fun profile_allocations (_: (int * string) list -> unit) f x = f x;
-end;
-
-(*dummy implementation*)
-fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
-
-
-(* ML command execution *)
-
-fun use_text ({tune_source, print, error, ...}: use_context)
- {line, file, verbose, debug = _: bool} text =
- let
- val ref out_orig = Control.Print.out;
-
- val out_buffer = ref ([]: string list);
- val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
- fun output () =
- let val str = implode (rev (! out_buffer))
- in String.substring (str, 0, Int.max (0, size str - 1)) end;
- in
- Control.Print.out := out;
- Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
- handle exn =>
- (Control.Print.out := out_orig;
- error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
- Control.Print.out := out_orig;
- 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;
-
-
-(* toplevel pretty printing *)
-
-fun ml_pprint pps =
- let
- fun str "" = ()
- | str s = PrettyPrint.string pps s;
- fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
- (str bg;
- (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
- (PrettyPrint.Rel (dest_int ind));
- List.app pprint prts; PrettyPrint.closeBox pps;
- str en)
- | pprint (ML_Pretty.String (s, _)) = str s
- | pprint (ML_Pretty.Break (false, width, offset)) =
- PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
- | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
- in pprint end;
-
-fun toplevel_pp context path pp =
- use_text context {line = 1, file = "pp", verbose = false, debug = false}
- ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
- "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
-
-
-
-(** interrupts **)
-
-local
-
-fun change_signal new_handler f x =
- let
- val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
- val result = Exn.capture (f old_handler) x;
- val _ = Signals.setHandler (Signals.sigINT, old_handler);
- in Exn.release result end;
-
-in
-
-fun interruptible (f: 'a -> 'b) x =
- let
- val result = ref (Exn.interrupt_exn: 'b Exn.result);
- val old_handler = Signals.inqHandler Signals.sigINT;
- in
- SMLofNJ.Cont.callcc (fn cont =>
- (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
- result := Exn.capture f x));
- Signals.setHandler (Signals.sigINT, old_handler);
- Exn.release (! result)
- end;
-
-fun uninterruptible f =
- change_signal Signals.IGNORE
- (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/ml_debugger.ML";
-
-
-(* ML system operations *)
-
-fun ml_platform_path (s: string) = s;
-fun ml_standard_path (s: string) = s;
-
-use "ML-Systems/ml_system.ML";
-
-structure ML_System =
-struct
-
-open ML_System;
-
-fun save_state name =
- if SMLofNJ.exportML name then ()
- else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
-
-end;
--- a/src/Pure/ML-Systems/thread_dummy.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(* Title: Pure/ML-Systems/thread_dummy.ML
- Author: Makarius
-
-Default (mostly dummy) implementation of thread structures
-(cf. polyml/basis/Thread.sml).
-*)
-
-exception Thread of string;
-
-local fun fail _ = raise Thread "No multithreading support on this ML platform" in
-
-structure Mutex =
-struct
- type mutex = unit;
- fun mutex _ = ();
- fun lock _ = fail ();
- fun unlock _ = fail ();
- fun trylock _ = fail ();
-end;
-
-structure ConditionVar =
-struct
- type conditionVar = unit;
- fun conditionVar _ = ();
- fun wait _ = fail ();
- fun waitUntil _ = fail ();
- fun signal _ = fail ();
- fun broadcast _ = fail ();
-end;
-
-structure Thread =
-struct
- type thread = unit;
-
- datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
- and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
-
- fun unavailable () = fail ();
-
- fun fork _ = fail ();
- fun exit _ = fail ();
- fun isActive _ = fail ();
-
- fun equal _ = fail ();
- fun self _ = fail ();
-
- fun interrupt _ = fail ();
- fun broadcastInterrupt _ = fail ();
- fun testInterrupt _ = fail ();
-
- fun kill _ = fail ();
-
- fun setAttributes _ = fail ();
- fun getAttributes _ = fail ();
-
- fun numProcessors _ = fail ();
-
-
-(* thread data *)
-
-local
-
-val data = ref ([]: Universal.universal ref list);
-
-fun find_data tag =
- let
- fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
- | find [] = NONE;
- in find (! data) end;
-
-in
-
-fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
-
-fun setLocal (tag, x) =
- (case find_data tag of
- SOME r => r := Universal.tagInject tag x
- | NONE => data := ref (Universal.tagInject tag x) :: ! data);
-
-end;
-end;
-end;
--- a/src/Pure/ML-Systems/universal.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: Pure/ML-Systems/universal.ML
- Author: Makarius
-
-Universal values via tagged union. Emulates structure Universal
-from Poly/ML 5.1.
-*)
-
-signature UNIVERSAL =
-sig
- type universal
- type 'a tag
- val tag: unit -> 'a tag
- val tagIs: 'a tag -> universal -> bool
- val tagInject: 'a tag -> 'a -> universal
- val tagProject: 'a tag -> universal -> 'a
-end;
-
-structure Universal: UNIVERSAL =
-struct
-
-type universal = exn;
-
-datatype 'a tag = Tag of
- {is: universal -> bool,
- inject: 'a -> universal,
- project: universal -> 'a};
-
-fun tag () =
- let exception Universal of 'a in
- Tag {
- is = fn Universal _ => true | _ => false,
- inject = Universal,
- project = fn Universal x => x}
- end;
-
-fun tagIs (Tag {is, ...}) = is;
-fun tagInject (Tag {inject, ...}) = inject;
-fun tagProject (Tag {project, ...}) = project;
-
-end;
-
--- a/src/Pure/ML-Systems/unsynchronized.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: Pure/ML-Systems/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/ML-Systems/use_context.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: Pure/ML-Systems/use_context.ML
- Author: Makarius
-
-Common context for "use" operations (compiler invocation).
-*)
-
-type use_context =
- {tune_source: string -> string,
- name_space: ML_Name_Space.T,
- str_of_pos: int -> string -> string,
- print: string -> unit,
- error: string -> unit};
-
--- a/src/Pure/ML-Systems/windows_path.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Title: Pure/ML-Systems/windows_path.ML
- Author: Makarius
-
-Windows file-system paths.
-*)
-
-fun ml_platform_path 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;
-
-fun ml_standard_path 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/compiler_polyml.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,59 @@
+(* Title: Pure/RAW/compiler_polyml.ML
+
+Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
+*)
+
+local
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+in
+
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ {line, file, verbose, debug} text =
+ let
+ val current_line = Unsynchronized.ref line;
+ val in_buffer =
+ Unsynchronized.ref (String.explode (tune_source (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" ^ str_of_pos 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] @
+ ML_Compiler_Parameters.debug debug;
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); 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;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,92 @@
+(* Title: Pure/RAW/exn.ML
+ Author: Makarius
+
+Support for exceptions.
+*)
+
+signature EXN =
+sig
+ 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
+end;
+
+structure Exn: EXN =
+struct
+
+(* 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 = 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;
+
+end;
+
+datatype illegal = Interrupt;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn.scala Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,106 @@
+/* Title: Pure/RAW/exn.scala
+ Module: PIDE
+ Author: Makarius
+
+Support for exceptions (arbitrary throwables).
+*/
+
+package isabelle
+
+
+object Exn
+{
+ /* 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[Library.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/RAW/exn_trace_polyml-5.5.1.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/RAW/exn_trace_polyml-5.5.1.ML
+ Author: Makarius
+
+Exception trace for Poly/ML 5.5.1 via ML output.
+*)
+
+fun print_exception_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);
+
+PolyML.Compiler.reportExhaustiveHandlers := true;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_compiler_parameters.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,17 @@
+(* Title: Pure/ML/ml_compiler_parameters.ML
+ Author: Makarius
+
+Additional ML compiler parameters for Poly/ML.
+*)
+
+signature ML_COMPILER_PARAMETERS =
+sig
+ val debug: bool -> PolyML.Compiler.compilerParameters list
+end;
+
+structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
+struct
+
+fun debug _ = [];
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,12 @@
+(* Title: Pure/ML/ml_compiler_parameters_polyml-5.6.ML
+ Author: Makarius
+
+Additional ML compiler parameters for Poly/ML 5.6, or later.
+*)
+
+structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
+struct
+
+fun debug b = [PolyML.Compiler.CPDebug b];
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_debugger.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,64 @@
+(* Title: Pure/ML/ml_debugger.ML
+ Author: Makarius
+
+ML debugger interface -- dummy version.
+*)
+
+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
+ 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
+with
+
+fun exn_id exn = Exn_Id (General.exnName exn);
+fun print_exn_id (Exn_Id name) = name;
+fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2; (*over-approximation*)
+
+end;
+
+
+(* hooks *)
+
+fun on_entry _ = ();
+fun on_exit _ = ();
+fun on_exit_exception _ = ();
+fun on_breakpoint _ = ();
+
+
+(* debugger *)
+
+fun fail () = raise Fail "No debugger support on this ML platform";
+
+type state = unit;
+
+fun state _ = [];
+fun debug_function () = fail ();
+fun debug_function_arg () = fail ();
+fun debug_function_result () = fail ();
+fun debug_location () = fail ();
+fun debug_name_space () = fail ();
+fun debug_local_name_space () = fail ();
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_debugger_polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,72 @@
+(* Title: Pure/RAW/ml_debugger_polyml-5.6.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 (ML_Pretty.String (s, 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/RAW/ml_name_space.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,68 @@
+(* Title: Pure/RAW/ml_name_space.ML
+ Author: Makarius
+
+ML name space -- dummy version of Poly/ML 5.2 facility.
+*)
+
+structure ML_Name_Space =
+struct
+
+type valueVal = unit;
+type typeVal = unit;
+type fixityVal = unit;
+type structureVal = unit;
+type signatureVal = unit;
+type functorVal = unit;
+
+type T =
+ {lookupVal: string -> valueVal option,
+ lookupType: string -> typeVal option,
+ lookupFix: string -> fixityVal option,
+ lookupStruct: string -> structureVal option,
+ lookupSig: string -> signatureVal option,
+ lookupFunct: string -> functorVal option,
+ enterVal: string * valueVal -> unit,
+ enterType: string * typeVal -> unit,
+ enterFix: string * fixityVal -> unit,
+ enterStruct: string * structureVal -> unit,
+ enterSig: string * signatureVal -> unit,
+ enterFunct: string * functorVal -> unit,
+ allVal: unit -> (string * valueVal) list,
+ allType: unit -> (string * typeVal) list,
+ allFix: unit -> (string * fixityVal) list,
+ allStruct: unit -> (string * structureVal) list,
+ allSig: unit -> (string * signatureVal) list,
+ allFunct: unit -> (string * functorVal) list};
+
+val global: T =
+ {lookupVal = fn _ => NONE,
+ lookupType = fn _ => NONE,
+ lookupFix = fn _ => NONE,
+ lookupStruct = fn _ => NONE,
+ lookupSig = fn _ => NONE,
+ lookupFunct = fn _ => NONE,
+ enterVal = fn _ => (),
+ enterType = fn _ => (),
+ enterFix = fn _ => (),
+ enterStruct = fn _ => (),
+ enterSig = fn _ => (),
+ enterFunct = fn _ => (),
+ allVal = fn _ => [],
+ allType = fn _ => [],
+ allFix = fn _ => [],
+ allStruct = fn _ => [],
+ allSig = fn _ => [],
+ allFunct = fn _ => []};
+
+val initial_val : (string * valueVal) list = [];
+val initial_type : (string * typeVal) list = [];
+val initial_fixity : (string * fixityVal) list = [];
+val initial_structure : (string * structureVal) list = [];
+val initial_signature : (string * signatureVal) list = [];
+val initial_functor : (string * functorVal) list = [];
+
+fun forget_global_structure (_: string) = ();
+
+fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_name_space_polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,33 @@
+(* Title: Pure/RAW/ml_name_space_polyml-5.6.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);
+
+ type typeVal = TypeConstrs.typeConstr;
+ fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+
+ type fixityVal = Infixes.fixity;
+ fun displayFix (_: string, x) = Infixes.print x;
+
+ type structureVal = Structures.structureVal;
+ fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+
+ type signatureVal = Signatures.signatureVal;
+ fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+
+ type functorVal = Functors.functorVal;
+ fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_name_space_polyml.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,13 @@
+(* Title: Pure/RAW/ml_name_space_polyml.ML
+ Author: Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = nameSpace;
+ val global = PolyML.globalNameSpace;
+ val forget_global_structure = PolyML.Compiler.forgetStructure;
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_parse_tree.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,19 @@
+(* Title: Pure/ML/ml_parse_tree.ML
+ Author: Makarius
+
+Additional ML parse tree components for Poly/ML.
+*)
+
+signature ML_PARSE_TREE =
+sig
+ val completions: PolyML.ptProperties -> string list option
+ val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
+end;
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions _ = NONE;
+fun breakpoint _ = NONE;
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_parse_tree_polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/RAW/ml_parse_tree_polyml-5.6.ML
+ Author: Makarius
+
+Additional ML parse tree components for Poly/ML 5.6, or later.
+*)
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions (PolyML.PTcompletions x) = SOME x
+ | completions _ = NONE;
+
+fun breakpoint (PolyML.PTbreakPoint x) = SOME x
+ | breakpoint _ = NONE;
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_positions.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/RAW/ml_positions.ML
+ Author: Makarius
+
+Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
+*)
+
+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;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_pretty.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,30 @@
+(* Title: Pure/RAW/ml_pretty.ML
+ Author: Makarius
+
+Minimal support for raw ML pretty printing -- for boot-strapping only.
+*)
+
+structure ML_Pretty =
+struct
+
+datatype pretty =
+ Block of (string * string) * bool * int * pretty list |
+ String of string * int |
+ Break of bool * int * int;
+
+fun block prts = Block (("", ""), false, 2, prts);
+fun str s = String (s, size s);
+fun brk width = Break (false, width, 0);
+
+fun pair pretty1 pretty2 ((x, y), depth: int) =
+ block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+
+fun enum sep lpar rpar pretty (args, depth) =
+ 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 (Int.max (depth, 0)) args @ [str rpar])) end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_profiling_polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,19 @@
+(* Title: Pure/RAW/ml_profiling_polyml-5.6.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/RAW/ml_profiling_polyml.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,27 @@
+(* Title: Pure/RAW/ml_profiling_polyml.ML
+ Author: Makarius
+
+Profiling for Poly/ML.
+*)
+
+structure ML_Profiling =
+struct
+
+local
+
+fun profile n f x =
+ let
+ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+ val res = Exn.capture f x;
+ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
+ in Exn.release res end;
+
+in
+
+fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
+fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
+fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_stack_dummy.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/RAW/ml_stack_dummy.ML
+
+Maximum stack size (in words) for ML threads -- dummy version.
+*)
+
+signature ML_STACK =
+sig
+ val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit (_: int option) : Thread.threadAttribute list = [];
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_stack_polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/RAW/ml_stack_polyml-5.6.ML
+
+Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
+*)
+
+signature ML_STACK =
+sig
+ val limit: int option -> Thread.threadAttribute list
+end;
+
+structure ML_Stack: ML_STACK =
+struct
+
+fun limit m = [Thread.MaximumMLStack m];
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_system.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,32 @@
+(* Title: Pure/RAW/ml_system.ML
+ Author: Makarius
+
+ML system and platform operations.
+*)
+
+signature ML_SYSTEM =
+sig
+ val name: string
+ val is_polyml: bool
+ val is_smlnj: bool
+ val platform: string
+ val platform_is_windows: bool
+ val share_common_data: unit -> unit
+ val save_state: string -> unit
+end;
+
+structure ML_System: ML_SYSTEM =
+struct
+
+val SOME name = OS.Process.getEnv "ML_SYSTEM";
+val is_polyml = String.isPrefix "polyml" name;
+val is_smlnj = String.isPrefix "smlnj" name;
+
+val SOME platform = OS.Process.getEnv "ML_PLATFORM";
+val platform_is_windows = String.isSuffix "windows" platform;
+
+fun share_common_data () = ();
+fun save_state _ = raise Fail "Cannot save state -- undefined operation";
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/multithreading.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,75 @@
+(* Title: Pure/RAW/multithreading.ML
+ Author: Makarius
+
+Dummy implementation of multithreading setup.
+*)
+
+signature MULTITHREADING =
+sig
+ val available: bool
+ 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 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 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
+
+(* options *)
+
+val available = false;
+fun max_threads_value () = 1: int;
+fun max_threads_update _ = ();
+fun max_threads_setmp _ f x = f x;
+fun enabled () = false;
+
+
+(* attributes *)
+
+val no_interrupts = [];
+val public_interrupts = [];
+val private_interrupts = [];
+fun sync_interrupts _ = [];
+
+fun interrupted () = ();
+
+fun with_attributes _ e = e [];
+
+fun sync_wait _ _ _ _ = Exn.Res true;
+
+
+(* tracing *)
+
+val trace = ref (0: int);
+fun tracing _ _ = ();
+fun tracing_time _ _ _ = ();
+fun real_time f x = (f x; Time.zeroTime);
+
+
+(* synchronized evaluation *)
+
+fun synchronized _ _ e = e ();
+
+
+(* serial numbers *)
+
+local val count = ref (0: int)
+in fun serial () = (count := ! count + 1; ! count) end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/multithreading_polyml.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,172 @@
+(* Title: Pure/RAW/multithreading_polyml.ML
+ Author: Makarius
+
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
+*)
+
+signature MULTITHREADING =
+sig
+ include MULTITHREADING
+ val interruptible: ('a -> 'b) -> 'a -> 'b
+ val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+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 *)
+
+val available = true;
+
+fun max_threads_result m =
+ if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 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;
+
+val interruptible = Multithreading.interruptible;
+val uninterruptible = Multithreading.uninterruptible;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/overloading_smlnj.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,41 @@
+(* Title: Pure/RAW/overloading_smlnj.ML
+ Author: Makarius
+
+Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
+*)
+
+Control.overloadKW := true;
+
+overload ~ : ('a -> 'a) as
+ IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
+ Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
+overload + : ('a * 'a -> 'a) as
+ IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
+ Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
+overload - : ('a * 'a -> 'a) as
+ IntInf.- and Int31.- and Int32.- and Int64.- and
+ Word.- and Word8.- and Word32.- and Word64.- and Real.-;
+overload * : ('a * 'a -> 'a) as
+ IntInf.* and Int31.* and Int32.* and Int64.* and
+ Word.* and Word8.* and Word32.* and Word64.* and Real.*;
+overload div: ('a * 'a -> 'a) as
+ IntInf.div and Int31.div and Int32.div and Int64.div and
+ Word.div and Word8.div and Word32.div and Word64.div;
+overload mod: ('a * 'a -> 'a) as
+ IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
+ Word.mod and Word8.mod and Word32.mod and Word64.mod;
+overload < : ('a * 'a -> bool) as
+ IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
+ Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
+overload <= : ('a * 'a -> bool) as
+ IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
+ Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
+overload > : ('a * 'a -> bool) as
+ IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
+ Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
+overload >= : ('a * 'a -> bool) as
+ IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
+ Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
+overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
+
+Control.overloadKW := false;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/polyml-5.5.2.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,23 @@
+(* Title: Pure/RAW/polyml-5.5.2.ML
+ Author: Makarius
+
+Compatibility wrapper for Poly/ML 5.5.2.
+*)
+
+structure Thread =
+struct
+ open Thread;
+
+ structure Thread =
+ struct
+ open Thread;
+
+ fun numProcessors () =
+ (case Thread.numPhysicalProcessors () of
+ SOME n => n
+ | NONE => Thread.numProcessors ());
+ end;
+end;
+
+use "RAW/polyml.ML";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/polyml-5.6.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,22 @@
+(* Title: Pure/RAW/polyml-5.6.ML
+ Author: Makarius
+
+Compatibility wrapper for Poly/ML 5.6.
+*)
+
+structure Thread =
+struct
+ open Thread;
+
+ structure Thread =
+ struct
+ open Thread;
+
+ fun numProcessors () =
+ (case Thread.numPhysicalProcessors () of
+ SOME n => n
+ | NONE => Thread.numProcessors ());
+ end;
+end;
+
+use "RAW/polyml.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/polyml.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,207 @@
+(* Title: Pure/RAW/polyml.ML
+ Author: Makarius
+
+Compatibility wrapper for Poly/ML.
+*)
+
+(* initial ML name space *)
+
+use "RAW/ml_system.ML";
+
+if ML_System.name = "polyml-5.6"
+then use "RAW/ml_name_space_polyml-5.6.ML"
+else use "RAW/ml_name_space_polyml.ML";
+
+structure ML_Name_Space =
+struct
+ open ML_Name_Space;
+ val initial_val =
+ List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+ (#allVal global ());
+ val initial_type = #allType global ();
+ val initial_fixity = #allFix global ();
+ val initial_structure = #allStruct global ();
+ val initial_signature = #allSig global ();
+ val initial_functor = #allFunct global ();
+end;
+
+
+(* ML system operations *)
+
+if ML_System.name = "polyml-5.3.0"
+then use "RAW/share_common_data_polyml-5.3.0.ML"
+else ();
+
+fun ml_platform_path (s: string) = s;
+fun ml_standard_path (s: string) = s;
+
+if ML_System.platform_is_windows then use "RAW/windows_path.ML" else ();
+
+structure ML_System =
+struct
+ open ML_System;
+ fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+ val save_state = PolyML.SaveState.saveState o ml_platform_path;
+end;
+
+
+(* exceptions *)
+
+fun reraise exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => raise exn
+ | SOME location => PolyML.raiseWithLocation (exn, location));
+
+exception Interrupt = SML90.Interrupt;
+
+use "RAW/exn.ML";
+
+fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
+
+if ML_System.name = "polyml-5.5.1"
+ orelse ML_System.name = "polyml-5.5.2"
+ orelse ML_System.name = "polyml-5.6"
+then use "RAW/exn_trace_polyml-5.5.1.ML"
+else ();
+
+
+(* multithreading *)
+
+val seconds = Time.fromReal;
+
+if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
+then ()
+else use "RAW/single_assignment_polyml.ML";
+
+open Thread;
+use "RAW/multithreading.ML";
+use "RAW/multithreading_polyml.ML";
+
+if ML_System.name = "polyml-5.6"
+then use "RAW/ml_stack_polyml-5.6.ML"
+else use "RAW/ml_stack_dummy.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;
+
+val io_buffer_size = 4096;
+
+fun quit () = exit 0;
+
+
+(* ML runtime system *)
+
+if ML_System.name = "polyml-5.6"
+then use "RAW/ml_profiling_polyml-5.6.ML"
+else use "RAW/ml_profiling_polyml.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;
+
+val pretty_ml =
+ let
+ fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
+ | convert _ (PolyML.PrettyBlock (_, _,
+ [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
+ ML_Pretty.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 ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
+ | convert len (PolyML.PrettyString s) =
+ ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+ in convert "" end;
+
+fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
+ | ml_pretty (ML_Pretty.Break (true, _, _)) =
+ PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+ [PolyML.PrettyString " "])
+ | ml_pretty (ML_Pretty.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 ml_pretty prts) end
+ | ml_pretty (ML_Pretty.String (s, len)) =
+ if len = size s then PolyML.PrettyString s
+ else PolyML.PrettyBlock
+ (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
+
+
+(* ML compiler *)
+
+structure ML_Name_Space =
+struct
+ open ML_Name_Space;
+ val display_val = pretty_ml o displayVal;
+end;
+
+use "RAW/ml_compiler_parameters.ML";
+if ML_System.name = "polyml-5.6"
+then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
+
+use "RAW/use_context.ML";
+use "RAW/ml_positions.ML";
+use "RAW/compiler_polyml.ML";
+
+PolyML.Compiler.reportUnreferencedIds := true;
+PolyML.Compiler.printInAlphabeticalOrder := false;
+PolyML.Compiler.maxInlineSize := 80;
+
+fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
+
+use "RAW/ml_parse_tree.ML";
+if ML_System.name = "polyml-5.6"
+then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
+
+fun toplevel_pp context (_: string list) pp =
+ use_text context {line = 1, file = "pp", verbose = false, debug = false}
+ ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+
+fun ml_make_string struct_name =
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
+ struct_name ^ ".ML_print_depth ())))))";
+
+
+(* ML debugger *)
+
+if ML_System.name = "polyml-5.6"
+then use "RAW/ml_debugger_polyml-5.6.ML"
+else use "RAW/ml_debugger.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/pp_dummy.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/RAW/pp_dummy.ML
+
+Dummy setup for toplevel pretty printing.
+*)
+
+fun ml_pretty _ = raise Fail "ml_pretty dummy";
+fun pretty_ml _ = raise Fail "pretty_ml dummy";
+
+structure PolyML =
+struct
+ fun addPrettyPrinter _ = ();
+ fun prettyRepresentation _ =
+ raise Fail "PolyML.prettyRepresentation dummy";
+ open PolyML;
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/proper_int.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,289 @@
+(* Title: Pure/RAW/proper_int.ML
+ Author: Makarius
+
+SML basis with type int representing proper integers, not machine
+words.
+*)
+
+val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
+val dest_int = IntInf.toInt: IntInf.int -> Int.int;
+
+
+(* Int *)
+
+type int = IntInf.int;
+
+structure IntInf =
+struct
+ open IntInf;
+ fun fromInt (a: int) = a;
+ fun toInt (a: int) = a;
+ val log2 = mk_int o IntInf.log2;
+ val sign = mk_int o IntInf.sign;
+end;
+
+structure Int = IntInf;
+
+
+(* List *)
+
+structure List =
+struct
+ open List;
+ fun length a = mk_int (List.length a);
+ fun nth (a, b) = List.nth (a, dest_int b);
+ fun take (a, b) = List.take (a, dest_int b);
+ fun drop (a, b) = List.drop (a, dest_int b);
+ fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
+end;
+
+val length = List.length;
+
+
+(* Array *)
+
+structure Array =
+struct
+ open Array;
+ val maxLen = mk_int Array.maxLen;
+ fun array (a, b) = Array.array (dest_int a, b);
+ fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
+ fun length a = mk_int (Array.length a);
+ fun sub (a, b) = Array.sub (a, dest_int b);
+ fun update (a, b, c) = Array.update (a, dest_int b, c);
+ fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
+ fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
+ fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
+ fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
+ fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun findi a b =
+ (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
+ NONE => NONE
+ | SOME (c, d) => SOME (mk_int c, d));
+end;
+
+
+(* Vector *)
+
+structure Vector =
+struct
+ open Vector;
+ val maxLen = mk_int Vector.maxLen;
+ fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
+ fun length a = mk_int (Vector.length a);
+ fun sub (a, b) = Vector.sub (a, dest_int b);
+ fun update (a, b, c) = Vector.update (a, dest_int b, c);
+ fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
+ fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
+ fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun findi a b =
+ (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
+ NONE => NONE
+ | SOME (c, d) => SOME (mk_int c, d));
+end;
+
+
+(* CharVector *)
+
+structure CharVector =
+struct
+ open CharVector;
+ fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
+end;
+
+
+(* Word8VectorSlice *)
+
+structure Word8VectorSlice =
+struct
+ open Word8VectorSlice;
+ val length = mk_int o Word8VectorSlice.length;
+ fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
+end;
+
+
+(* Char *)
+
+structure Char =
+struct
+ open Char;
+ val maxOrd = mk_int Char.maxOrd;
+ val chr = Char.chr o dest_int;
+ val ord = mk_int o Char.ord;
+end;
+
+val chr = Char.chr;
+val ord = Char.ord;
+
+
+(* String *)
+
+structure String =
+struct
+ open String;
+ val maxSize = mk_int String.maxSize;
+ val size = mk_int o String.size;
+ fun sub (a, b) = String.sub (a, dest_int b);
+ fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
+ fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
+end;
+
+val size = String.size;
+val substring = String.substring;
+
+
+(* Substring *)
+
+structure Substring =
+struct
+ open Substring;
+ fun sub (a, b) = Substring.sub (a, dest_int b);
+ val size = mk_int o Substring.size;
+ fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
+ fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
+ fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
+ fun triml a b = Substring.triml (dest_int a) b;
+ fun trimr a b = Substring.trimr (dest_int a) b;
+ fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
+ fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
+end;
+
+
+(* StringCvt *)
+
+structure StringCvt =
+struct
+ open StringCvt;
+ datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
+ fun realfmt fmt = Real.fmt
+ (case fmt of
+ EXACT => StringCvt.EXACT
+ | FIX NONE => StringCvt.FIX NONE
+ | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
+ | GEN NONE => StringCvt.GEN NONE
+ | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
+ | SCI NONE => StringCvt.SCI NONE
+ | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
+ fun padRight a b c = StringCvt.padRight a (dest_int b) c;
+ fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
+end;
+
+
+(* Word *)
+
+structure Word =
+struct
+ open Word;
+ val wordSize = mk_int Word.wordSize;
+ val toInt = Word.toLargeInt;
+ val toIntX = Word.toLargeIntX;
+ val fromInt = Word.fromLargeInt;
+end;
+
+structure Word8 =
+struct
+ open Word8;
+ val wordSize = mk_int Word8.wordSize;
+ val toInt = Word8.toLargeInt;
+ val toIntX = Word8.toLargeIntX;
+ val fromInt = Word8.fromLargeInt;
+end;
+
+structure Word32 =
+struct
+ open Word32;
+ val wordSize = mk_int Word32.wordSize;
+ val toInt = Word32.toLargeInt;
+ val toIntX = Word32.toLargeIntX;
+ val fromInt = Word32.fromLargeInt;
+end;
+
+structure LargeWord =
+struct
+ open LargeWord;
+ val wordSize = mk_int LargeWord.wordSize;
+ val toInt = LargeWord.toLargeInt;
+ val toIntX = LargeWord.toLargeIntX;
+ val fromInt = LargeWord.fromLargeInt;
+end;
+
+
+(* Real *)
+
+structure Real =
+struct
+ open Real;
+ val radix = mk_int Real.radix;
+ val precision = mk_int Real.precision;
+ fun sign a = mk_int (Real.sign a);
+ fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
+ fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
+ val ceil = mk_int o Real.ceil;
+ val floor = mk_int o Real.floor;
+ val real = Real.fromInt o dest_int;
+ val round = mk_int o Real.round;
+ val trunc = mk_int o Real.trunc;
+ fun toInt a b = mk_int (Real.toInt a b);
+ fun fromInt a = Real.fromInt (dest_int a);
+ val fmt = StringCvt.realfmt;
+end;
+
+val ceil = Real.ceil;
+val floor = Real.floor;
+val real = Real.real;
+val round = Real.round;
+val trunc = Real.trunc;
+
+
+(* TextIO *)
+
+structure TextIO =
+struct
+ open TextIO;
+ fun inputN (a, b) = TextIO.inputN (a, dest_int b);
+ fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
+end;
+
+
+(* BinIO *)
+
+structure BinIO =
+struct
+ open BinIO;
+ fun inputN (a, b) = BinIO.inputN (a, dest_int b);
+ fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
+end;
+
+
+(* Time *)
+
+structure Time =
+struct
+ open Time;
+ fun fmt a b = Time.fmt (dest_int a) b;
+end;
+
+
+(* Sockets *)
+
+structure INetSock =
+struct
+ open INetSock;
+ fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
+ fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
+end;
+
+
+(* OS.FileSys *)
+
+structure OS =
+struct
+ open OS;
+ structure FileSys =
+ struct
+ open FileSys;
+ fun fileSize a = mk_int (FileSys.fileSize a);
+ end;
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/share_common_data_polyml-5.3.0.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,11 @@
+(* Title: Pure/RAW/share_common_data_polyml-5.3.0.ML
+
+Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
+anymore.
+*)
+
+structure PolyML =
+struct
+ open PolyML;
+ fun shareCommonData _ = ();
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/single_assignment.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,33 @@
+(* Title: Pure/RAW/single_assignment.ML
+ Author: Makarius
+
+References with single assignment. Unsynchronized!
+*)
+
+signature SINGLE_ASSIGNMENT =
+sig
+ type 'a saref
+ exception Locked
+ val saref: unit -> 'a saref
+ val savalue: 'a saref -> 'a option
+ val saset: 'a saref * 'a -> unit
+end;
+
+structure SingleAssignment: SINGLE_ASSIGNMENT =
+struct
+
+exception Locked;
+
+abstype 'a saref = SARef of 'a option ref
+with
+
+fun saref () = SARef (ref NONE);
+
+fun savalue (SARef r) = ! r;
+
+fun saset (SARef (r as ref NONE), x) = r := SOME x
+ | saset _ = raise Locked;
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/single_assignment_polyml.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,35 @@
+(* Title: Pure/RAW/single_assignment_polyml.ML
+ Author: Makarius
+
+References with single assignment. Unsynchronized! Emulates
+structure SingleAssignment from Poly/ML 5.4.
+*)
+
+signature SINGLE_ASSIGNMENT =
+sig
+ type 'a saref
+ exception Locked
+ val saref: unit -> 'a saref
+ val savalue: 'a saref -> 'a option
+ val saset: 'a saref * 'a -> unit
+end;
+
+structure SingleAssignment: SINGLE_ASSIGNMENT =
+struct
+
+exception Locked;
+
+abstype 'a saref = SARef of 'a option ref
+with
+
+fun saref () = SARef (ref NONE);
+
+fun savalue (SARef r) = ! r;
+
+fun saset (SARef (r as ref NONE), x) =
+ (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
+ | saset _ = raise Locked;
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/smlnj.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,194 @@
+(* Title: Pure/RAW/smlnj.ML
+
+Compatibility file for Standard ML of New Jersey.
+*)
+
+val io_buffer_size = 4096;
+use "RAW/proper_int.ML";
+
+exception Interrupt;
+fun reraise exn = raise exn;
+
+fun exit rc = Posix.Process.exit (Word8.fromInt rc);
+fun quit () = exit 0;
+
+use "RAW/overloading_smlnj.ML";
+use "RAW/exn.ML";
+use "RAW/single_assignment.ML";
+use "RAW/universal.ML";
+use "RAW/thread_dummy.ML";
+use "RAW/multithreading.ML";
+use "RAW/ml_stack_dummy.ML";
+use "RAW/ml_pretty.ML";
+use "RAW/ml_name_space.ML";
+structure PolyML = struct end;
+use "RAW/pp_dummy.ML";
+use "RAW/use_context.ML";
+use "RAW/ml_positions.ML";
+
+
+val seconds = Time.fromReal;
+
+(*low-level pointer equality*)
+CM.autoload "$smlnj/init/init.cmi";
+val pointer_eq = InlineT.ptreql;
+
+
+(* restore old-style character / string functions *)
+
+val ord = mk_int o SML90.ord;
+val chr = SML90.chr o dest_int;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+
+(* New Jersey ML parameters *)
+
+val _ =
+ (Control.Print.printLength := 1000;
+ Control.Print.printDepth := 350;
+ Control.Print.stringDepth := 250;
+ Control.Print.signatures := 2;
+ Control.MC.matchRedundantError := false);
+
+
+(* Poly/ML emulation *)
+
+(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
+local
+ val depth = ref (10: int);
+in
+ fun get_default_print_depth () = ! depth;
+ fun default_print_depth n =
+ (depth := n;
+ Control.Print.printDepth := dest_int n div 2;
+ Control.Print.printLength := dest_int n);
+ val _ = default_print_depth 10;
+end;
+
+fun ml_make_string (_: string) = "(fn _ => \"?\")";
+
+
+(*prompts*)
+fun ml_prompts p1 p2 =
+ (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
+
+(*dummy implementation*)
+structure ML_Profiling =
+struct
+ fun profile_time (_: (int * string) list -> unit) f x = f x;
+ fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
+ fun profile_allocations (_: (int * string) list -> unit) f x = f x;
+end;
+
+(*dummy implementation*)
+fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
+
+
+(* ML command execution *)
+
+fun use_text ({tune_source, print, error, ...}: use_context)
+ {line, file, verbose, debug = _: bool} text =
+ let
+ val ref out_orig = Control.Print.out;
+
+ val out_buffer = ref ([]: string list);
+ val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
+ fun output () =
+ let val str = implode (rev (! out_buffer))
+ in String.substring (str, 0, Int.max (0, size str - 1)) end;
+ in
+ Control.Print.out := out;
+ Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
+ handle exn =>
+ (Control.Print.out := out_orig;
+ error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
+ Control.Print.out := out_orig;
+ 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;
+
+
+(* toplevel pretty printing *)
+
+fun ml_pprint pps =
+ let
+ fun str "" = ()
+ | str s = PrettyPrint.string pps s;
+ fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
+ (str bg;
+ (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
+ (PrettyPrint.Rel (dest_int ind));
+ List.app pprint prts; PrettyPrint.closeBox pps;
+ str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, width, offset)) =
+ PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
+ | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
+ in pprint end;
+
+fun toplevel_pp context path pp =
+ use_text context {line = 1, file = "pp", verbose = false, debug = false}
+ ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
+ "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
+
+
+
+(** interrupts **)
+
+local
+
+fun change_signal new_handler f x =
+ let
+ val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
+ val result = Exn.capture (f old_handler) x;
+ val _ = Signals.setHandler (Signals.sigINT, old_handler);
+ in Exn.release result end;
+
+in
+
+fun interruptible (f: 'a -> 'b) x =
+ let
+ val result = ref (Exn.interrupt_exn: 'b Exn.result);
+ val old_handler = Signals.inqHandler Signals.sigINT;
+ in
+ SMLofNJ.Cont.callcc (fn cont =>
+ (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
+ result := Exn.capture f x));
+ Signals.setHandler (Signals.sigINT, old_handler);
+ Exn.release (! result)
+ end;
+
+fun uninterruptible f =
+ change_signal Signals.IGNORE
+ (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
+
+end;
+
+
+use "RAW/unsynchronized.ML";
+use "RAW/ml_debugger.ML";
+
+
+(* ML system operations *)
+
+fun ml_platform_path (s: string) = s;
+fun ml_standard_path (s: string) = s;
+
+use "RAW/ml_system.ML";
+
+structure ML_System =
+struct
+
+open ML_System;
+
+fun save_state name =
+ if SMLofNJ.exportML name then ()
+ else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/thread_dummy.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,82 @@
+(* Title: Pure/RAW/thread_dummy.ML
+ Author: Makarius
+
+Default (mostly dummy) implementation of thread structures
+(cf. polyml/basis/Thread.sml).
+*)
+
+exception Thread of string;
+
+local fun fail _ = raise Thread "No multithreading support on this ML platform" in
+
+structure Mutex =
+struct
+ type mutex = unit;
+ fun mutex _ = ();
+ fun lock _ = fail ();
+ fun unlock _ = fail ();
+ fun trylock _ = fail ();
+end;
+
+structure ConditionVar =
+struct
+ type conditionVar = unit;
+ fun conditionVar _ = ();
+ fun wait _ = fail ();
+ fun waitUntil _ = fail ();
+ fun signal _ = fail ();
+ fun broadcast _ = fail ();
+end;
+
+structure Thread =
+struct
+ type thread = unit;
+
+ datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
+ and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
+
+ fun unavailable () = fail ();
+
+ fun fork _ = fail ();
+ fun exit _ = fail ();
+ fun isActive _ = fail ();
+
+ fun equal _ = fail ();
+ fun self _ = fail ();
+
+ fun interrupt _ = fail ();
+ fun broadcastInterrupt _ = fail ();
+ fun testInterrupt _ = fail ();
+
+ fun kill _ = fail ();
+
+ fun setAttributes _ = fail ();
+ fun getAttributes _ = fail ();
+
+ fun numProcessors _ = fail ();
+
+
+(* thread data *)
+
+local
+
+val data = ref ([]: Universal.universal ref list);
+
+fun find_data tag =
+ let
+ fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
+ | find [] = NONE;
+ in find (! data) end;
+
+in
+
+fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
+
+fun setLocal (tag, x) =
+ (case find_data tag of
+ SOME r => r := Universal.tagInject tag x
+ | NONE => data := ref (Universal.tagInject tag x) :: ! data);
+
+end;
+end;
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/universal.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,41 @@
+(* Title: Pure/RAW/universal.ML
+ Author: Makarius
+
+Universal values via tagged union. Emulates structure Universal
+from Poly/ML 5.1.
+*)
+
+signature UNIVERSAL =
+sig
+ type universal
+ type 'a tag
+ val tag: unit -> 'a tag
+ val tagIs: 'a tag -> universal -> bool
+ val tagInject: 'a tag -> 'a -> universal
+ val tagProject: 'a tag -> universal -> 'a
+end;
+
+structure Universal: UNIVERSAL =
+struct
+
+type universal = exn;
+
+datatype 'a tag = Tag of
+ {is: universal -> bool,
+ inject: 'a -> universal,
+ project: universal -> 'a};
+
+fun tag () =
+ let exception Universal of 'a in
+ Tag {
+ is = fn Universal _ => true | _ => false,
+ inject = Universal,
+ project = fn Universal x => x}
+ end;
+
+fun tagIs (Tag {is, ...}) = is;
+fun tagInject (Tag {inject, ...}) = inject;
+fun tagProject (Tag {project, ...}) = project;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/unsynchronized.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,30 @@
+(* 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/use_context.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,13 @@
+(* Title: Pure/RAW/use_context.ML
+ Author: Makarius
+
+Common context for "use" operations (compiler invocation).
+*)
+
+type use_context =
+ {tune_source: string -> string,
+ name_space: ML_Name_Space.T,
+ str_of_pos: int -> string -> string,
+ print: string -> unit,
+ error: string -> unit};
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/windows_path.ML Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,34 @@
+(* Title: Pure/RAW/windows_path.ML
+ Author: Makarius
+
+Windows file-system paths.
+*)
+
+fun ml_platform_path 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;
+
+fun ml_standard_path 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;
--- a/src/Pure/ROOT Wed Dec 23 21:15:26 2015 +0100
+++ b/src/Pure/ROOT Wed Dec 23 23:09:13 2015 +0100
@@ -3,83 +3,83 @@
session RAW =
theories
files
- "General/exn.ML"
- "ML-Systems/compiler_polyml.ML"
- "ML-Systems/exn_trace_polyml-5.5.1.ML"
- "ML-Systems/ml_compiler_parameters.ML"
- "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
- "ML-Systems/ml_debugger.ML"
- "ML-Systems/ml_debugger_polyml-5.6.ML"
- "ML-Systems/ml_name_space.ML"
- "ML-Systems/ml_name_space_polyml-5.6.ML"
- "ML-Systems/ml_name_space_polyml.ML"
- "ML-Systems/ml_parse_tree.ML"
- "ML-Systems/ml_parse_tree_polyml-5.6.ML"
- "ML-Systems/ml_positions.ML"
- "ML-Systems/ml_pretty.ML"
- "ML-Systems/ml_profiling_polyml-5.6.ML"
- "ML-Systems/ml_profiling_polyml.ML"
- "ML-Systems/ml_stack_dummy.ML"
- "ML-Systems/ml_stack_polyml-5.6.ML"
- "ML-Systems/ml_system.ML"
- "ML-Systems/multithreading.ML"
- "ML-Systems/multithreading_polyml.ML"
- "ML-Systems/overloading_smlnj.ML"
- "ML-Systems/polyml-5.5.2.ML"
- "ML-Systems/polyml-5.6.ML"
- "ML-Systems/polyml-5.6.ML"
- "ML-Systems/polyml.ML"
- "ML-Systems/pp_dummy.ML"
- "ML-Systems/proper_int.ML"
- "ML-Systems/share_common_data_polyml-5.3.0.ML"
- "ML-Systems/single_assignment.ML"
- "ML-Systems/single_assignment_polyml.ML"
- "ML-Systems/smlnj.ML"
- "ML-Systems/thread_dummy.ML"
- "ML-Systems/universal.ML"
- "ML-Systems/unsynchronized.ML"
- "ML-Systems/use_context.ML"
- "ML-Systems/windows_path.ML"
+ "RAW/compiler_polyml.ML"
+ "RAW/exn.ML"
+ "RAW/exn_trace_polyml-5.5.1.ML"
+ "RAW/ml_compiler_parameters.ML"
+ "RAW/ml_compiler_parameters_polyml-5.6.ML"
+ "RAW/ml_debugger.ML"
+ "RAW/ml_debugger_polyml-5.6.ML"
+ "RAW/ml_name_space.ML"
+ "RAW/ml_name_space_polyml-5.6.ML"
+ "RAW/ml_name_space_polyml.ML"
+ "RAW/ml_parse_tree.ML"
+ "RAW/ml_parse_tree_polyml-5.6.ML"
+ "RAW/ml_positions.ML"
+ "RAW/ml_pretty.ML"
+ "RAW/ml_profiling_polyml-5.6.ML"
+ "RAW/ml_profiling_polyml.ML"
+ "RAW/ml_stack_dummy.ML"
+ "RAW/ml_stack_polyml-5.6.ML"
+ "RAW/ml_system.ML"
+ "RAW/multithreading.ML"
+ "RAW/multithreading_polyml.ML"
+ "RAW/overloading_smlnj.ML"
+ "RAW/polyml-5.5.2.ML"
+ "RAW/polyml-5.6.ML"
+ "RAW/polyml-5.6.ML"
+ "RAW/polyml.ML"
+ "RAW/pp_dummy.ML"
+ "RAW/proper_int.ML"
+ "RAW/share_common_data_polyml-5.3.0.ML"
+ "RAW/single_assignment.ML"
+ "RAW/single_assignment_polyml.ML"
+ "RAW/smlnj.ML"
+ "RAW/thread_dummy.ML"
+ "RAW/universal.ML"
+ "RAW/unsynchronized.ML"
+ "RAW/use_context.ML"
+ "RAW/windows_path.ML"
session Pure =
global_theories Pure
files
- "General/exn.ML"
- "ML-Systems/compiler_polyml.ML"
- "ML-Systems/exn_trace_polyml-5.5.1.ML"
- "ML-Systems/ml_compiler_parameters.ML"
- "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
- "ML-Systems/ml_debugger.ML"
- "ML-Systems/ml_debugger_polyml-5.6.ML"
- "ML-Systems/ml_name_space.ML"
- "ML-Systems/ml_name_space_polyml-5.6.ML"
- "ML-Systems/ml_name_space_polyml.ML"
- "ML-Systems/ml_parse_tree.ML"
- "ML-Systems/ml_parse_tree_polyml-5.6.ML"
- "ML-Systems/ml_positions.ML"
- "ML-Systems/ml_pretty.ML"
- "ML-Systems/ml_profiling_polyml-5.6.ML"
- "ML-Systems/ml_profiling_polyml.ML"
- "ML-Systems/ml_stack_dummy.ML"
- "ML-Systems/ml_stack_polyml-5.6.ML"
- "ML-Systems/ml_system.ML"
- "ML-Systems/multithreading.ML"
- "ML-Systems/multithreading_polyml.ML"
- "ML-Systems/overloading_smlnj.ML"
- "ML-Systems/polyml-5.5.2.ML"
- "ML-Systems/polyml-5.6.ML"
- "ML-Systems/polyml.ML"
- "ML-Systems/pp_dummy.ML"
- "ML-Systems/proper_int.ML"
- "ML-Systems/share_common_data_polyml-5.3.0.ML"
- "ML-Systems/single_assignment.ML"
- "ML-Systems/single_assignment_polyml.ML"
- "ML-Systems/smlnj.ML"
- "ML-Systems/thread_dummy.ML"
- "ML-Systems/universal.ML"
- "ML-Systems/unsynchronized.ML"
- "ML-Systems/use_context.ML"
- "ML-Systems/windows_path.ML"
+ "RAW/compiler_polyml.ML"
+ "RAW/exn.ML"
+ "RAW/exn_trace_polyml-5.5.1.ML"
+ "RAW/ml_compiler_parameters.ML"
+ "RAW/ml_compiler_parameters_polyml-5.6.ML"
+ "RAW/ml_debugger.ML"
+ "RAW/ml_debugger_polyml-5.6.ML"
+ "RAW/ml_name_space.ML"
+ "RAW/ml_name_space_polyml-5.6.ML"
+ "RAW/ml_name_space_polyml.ML"
+ "RAW/ml_parse_tree.ML"
+ "RAW/ml_parse_tree_polyml-5.6.ML"
+ "RAW/ml_positions.ML"
+ "RAW/ml_pretty.ML"
+ "RAW/ml_profiling_polyml-5.6.ML"
+ "RAW/ml_profiling_polyml.ML"
+ "RAW/ml_stack_dummy.ML"
+ "RAW/ml_stack_polyml-5.6.ML"
+ "RAW/ml_system.ML"
+ "RAW/multithreading.ML"
+ "RAW/multithreading_polyml.ML"
+ "RAW/overloading_smlnj.ML"
+ "RAW/polyml-5.5.2.ML"
+ "RAW/polyml-5.6.ML"
+ "RAW/polyml.ML"
+ "RAW/pp_dummy.ML"
+ "RAW/proper_int.ML"
+ "RAW/share_common_data_polyml-5.3.0.ML"
+ "RAW/single_assignment.ML"
+ "RAW/single_assignment_polyml.ML"
+ "RAW/smlnj.ML"
+ "RAW/thread_dummy.ML"
+ "RAW/universal.ML"
+ "RAW/unsynchronized.ML"
+ "RAW/use_context.ML"
+ "RAW/windows_path.ML"
"Concurrent/bash.ML"
"Concurrent/bash_sequential.ML"
--- a/src/Pure/build Wed Dec 23 21:15:26 2015 +0100
+++ b/src/Pure/build Wed Dec 23 23:09:13 2015 +0100
@@ -49,8 +49,8 @@
[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
COMPAT=""
-[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"
-[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"
+[ -f "RAW/${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/${ML_SYSTEM_BASE}.ML"
+[ -f "RAW/${ML_SYSTEM}.ML" ] && COMPAT="RAW/${ML_SYSTEM}.ML"
[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
--- a/src/Pure/build-jars Wed Dec 23 21:15:26 2015 +0100
+++ b/src/Pure/build-jars Wed Dec 23 23:09:13 2015 +0100
@@ -28,7 +28,6 @@
General/antiquote.scala
General/bytes.scala
General/completion.scala
- General/exn.scala
General/file.scala
General/graph.scala
General/graph_display.scala
@@ -72,9 +71,10 @@
PIDE/text.scala
PIDE/xml.scala
PIDE/yxml.scala
+ RAW/exn.scala
ROOT.scala
+ System/command_line.scala
System/cygwin.scala
- System/command_line.scala
System/invoke_scala.scala
System/isabelle_charset.scala
System/isabelle_process.scala