# HG changeset patch # User wenzelm # Date 1450908553 -3600 # Node ID ab52f183f020289ab90af78492c08cdc46c21d38 # Parent 55b3d21ab5e574ead80ba7166074a7c8057c37f8 clarified directory structure; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/General/exn.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/General/exn.scala --- 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) -} diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/compiler_polyml.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_compiler_parameters.ML --- 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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML --- 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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_debugger.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_name_space.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_name_space_polyml.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_parse_tree.ML --- 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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML --- 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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_positions.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_pretty.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_profiling_polyml.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_stack_dummy.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_stack_polyml-5.6.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/ml_system.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/multithreading.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/multithreading_polyml.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/overloading_smlnj.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/polyml-5.5.2.ML --- 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"; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/polyml-5.6.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"; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/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"; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/pp_dummy.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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/proper_int.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/share_common_data_polyml-5.3.0.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/single_assignment.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/single_assignment_polyml.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/smlnj.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/thread_dummy.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/universal.ML --- 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; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/unsynchronized.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/use_context.ML --- 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}; - diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ML-Systems/windows_path.ML --- 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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/compiler_polyml.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/exn.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/exn.scala --- /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) +} diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/exn_trace_polyml-5.5.1.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_compiler_parameters.ML --- /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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML --- /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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_debugger.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_debugger_polyml-5.6.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_name_space.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_name_space_polyml-5.6.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_name_space_polyml.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_parse_tree.ML --- /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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_parse_tree_polyml-5.6.ML --- /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 diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_positions.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_pretty.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_profiling_polyml-5.6.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_profiling_polyml.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_stack_dummy.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_stack_polyml-5.6.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/ml_system.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/multithreading.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/multithreading_polyml.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/overloading_smlnj.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/polyml-5.5.2.ML --- /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"; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/polyml-5.6.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"; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/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"; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/pp_dummy.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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/proper_int.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/share_common_data_polyml-5.3.0.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/single_assignment.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/single_assignment_polyml.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/smlnj.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/thread_dummy.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/universal.ML --- /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; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/unsynchronized.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/use_context.ML --- /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}; + diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/RAW/windows_path.ML --- /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; diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/ROOT --- 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" diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/build --- 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\"!" diff -r 55b3d21ab5e5 -r ab52f183f020 src/Pure/build-jars --- 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