# HG changeset patch # User wenzelm # Date 1452072033 -3600 # Node ID e8ae72c2602555f57a94a5ac452dfd5f9e06c0ff # Parent 1add21f7cabce669c166c13f46f52d4827842293 clarified ROOT files; diff -r 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/ROOT_polyml-5.5.2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/RAW/ROOT_polyml-5.5.2.ML Wed Jan 06 10:20:33 2016 +0100 @@ -0,0 +1,23 @@ +(* Title: Pure/RAW/ROOT_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/ROOT_polyml.ML"; + diff -r 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/ROOT_polyml-5.6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/RAW/ROOT_polyml-5.6.ML Wed Jan 06 10:20:33 2016 +0100 @@ -0,0 +1,22 @@ +(* Title: Pure/RAW/ROOT_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/ROOT_polyml.ML"; diff -r 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/ROOT_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/RAW/ROOT_polyml.ML Wed Jan 06 10:20:33 2016 +0100 @@ -0,0 +1,207 @@ +(* Title: Pure/RAW/ROOT_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 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/ROOT_smlnj.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/RAW/ROOT_smlnj.ML Wed Jan 06 10:20:33 2016 +0100 @@ -0,0 +1,194 @@ +(* Title: Pure/RAW/ROOT_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 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/polyml-5.5.2.ML --- a/src/Pure/RAW/polyml-5.5.2.ML Wed Jan 06 10:08:09 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* 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 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/polyml-5.6.ML --- a/src/Pure/RAW/polyml-5.6.ML Wed Jan 06 10:08:09 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* 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 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/polyml.ML --- a/src/Pure/RAW/polyml.ML Wed Jan 06 10:08:09 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,207 +0,0 @@ -(* 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 1add21f7cabc -r e8ae72c26025 src/Pure/RAW/smlnj.ML --- a/src/Pure/RAW/smlnj.ML Wed Jan 06 10:08:09 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,194 +0,0 @@ -(* 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 1add21f7cabc -r e8ae72c26025 src/Pure/ROOT --- a/src/Pure/ROOT Wed Jan 06 10:08:09 2016 +0100 +++ b/src/Pure/ROOT Wed Jan 06 10:20:33 2016 +0100 @@ -3,6 +3,10 @@ session RAW = theories files + "RAW/ROOT_polyml-5.5.2.ML" + "RAW/ROOT_polyml-5.6.ML" + "RAW/ROOT_polyml.ML" + "RAW/ROOT_smlnj.ML" "RAW/compiler_polyml.ML" "RAW/exn.ML" "RAW/exn_trace_polyml-5.5.1.ML" @@ -25,15 +29,11 @@ "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" @@ -43,6 +43,10 @@ session Pure = global_theories Pure files + "RAW/ROOT_polyml-5.5.2.ML" + "RAW/ROOT_polyml-5.6.ML" + "RAW/ROOT_polyml.ML" + "RAW/ROOT_smlnj.ML" "RAW/compiler_polyml.ML" "RAW/exn.ML" "RAW/exn_trace_polyml-5.5.1.ML" @@ -65,15 +69,11 @@ "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" diff -r 1add21f7cabc -r e8ae72c26025 src/Pure/build --- a/src/Pure/build Wed Jan 06 10:08:09 2016 +0100 +++ b/src/Pure/build Wed Jan 06 10:20:33 2016 +0100 @@ -49,8 +49,8 @@ [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" COMPAT="" -[ -f "RAW/${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/${ML_SYSTEM_BASE}.ML" -[ -f "RAW/${ML_SYSTEM}.ML" ] && COMPAT="RAW/${ML_SYSTEM}.ML" +[ -f "RAW/ROOT_${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM_BASE}.ML" +[ -f "RAW/ROOT_${ML_SYSTEM}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM}.ML" [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"