--- a/Admin/Release/CHECKLIST Wed Mar 02 19:43:31 2016 +0100
+++ b/Admin/Release/CHECKLIST Thu Mar 03 11:12:02 2016 +0100
@@ -5,8 +5,6 @@
- check Admin/components;
-- test polyml-5.3.0;
-
- test 'display_drafts' command;
- test "#!/usr/bin/env isabelle_scala_script";
--- a/Admin/isatest/settings/at-poly Wed Mar 02 19:43:31 2016 +0100
+++ b/Admin/isatest/settings/at-poly Thu Mar 03 11:12:02 2016 +0100
@@ -2,11 +2,7 @@
init_components /home/isabelle/contrib "$HOME/admin/components/main"
- POLYML_HOME="/home/polyml/polyml-5.3.0"
- ML_SYSTEM="polyml-5.3.0"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
+ML_OPTIONS="-H 1000 --gcthreads 1"
ISABELLE_GHC=/usr/bin/ghc
@@ -35,4 +31,3 @@
ISABELLE_POLYML="$ML_HOME/poly"
ISABELLE_SCALA="$SCALA_HOME/bin"
ISABELLE_SMLNJ="/home/smlnj/bin/sml"
-
--- a/NEWS Wed Mar 02 19:43:31 2016 +0100
+++ b/NEWS Thu Mar 03 11:12:02 2016 +0100
@@ -205,7 +205,7 @@
discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
"YXML" in Isabelle/ML or Isabelle/Scala.
-* SML/NJ is no longer supported.
+* SML/NJ and old versions of Poly/ML are no longer supported.
New in Isabelle2016 (February 2016)
--- a/lib/scripts/run-polyml-5.3.0 Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.3.0.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## prepare databases
-
-if [ -z "$HEAP_FILE" ]; then
- INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
- check_file "$HEAP_FILE"
- INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
- { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
--- a/src/Pure/Concurrent/standard_thread.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.ML Thu Mar 03 11:12:02 2016 +0100
@@ -49,7 +49,7 @@
type params = {name: string, stack_limit: int option, interrupts: bool};
fun attributes ({stack_limit, interrupts, ...}: params) =
- ML_Stack.limit stack_limit @
+ Thread.MaximumMLStack stack_limit ::
(if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
fun fork (params: params) body =
--- a/src/Pure/ML/ml_compiler.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Thu Mar 03 11:12:02 2016 +0100
@@ -98,10 +98,8 @@
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
| reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
| reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
- | reported loc pt =
- (case ML_Parse_Tree.completions pt of
- SOME names => reported_completions loc names
- | NONE => I)
+ | reported loc (PolyML.PTcompletions names) = reported_completions loc names
+ | reported _ _ = I
and reported_tree (loc, props) = fold (reported loc) props;
val persistent_reports = reported_tree parse_tree [];
@@ -123,16 +121,14 @@
fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
| breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
- | breakpoints loc pt =
- (case ML_Parse_Tree.breakpoint pt of
- SOME b =>
- let val pos = breakpoint_position loc in
- if is_reported pos then
- let val id = serial ();
- in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
- else I
- end
- | NONE => I)
+ | breakpoints loc (PolyML.PTbreakPoint b) =
+ let val pos = breakpoint_position loc in
+ if is_reported pos then
+ let val id = serial ();
+ in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
+ else I
+ end
+ | breakpoints _ _ = I
and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
val all_breakpoints = rev (breakpoints_tree parse_tree []);
@@ -264,8 +260,8 @@
PolyML.Compiler.CPFileName location_props,
PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
PolyML.Compiler.CPCompilerResultFun result_fun,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
- ML_Compiler_Parameters.debug debug;
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+ PolyML.Compiler.CPDebug debug];
val _ =
(while not (List.null (! input_buffer)) do
--- a/src/Pure/RAW/ROOT_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* 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";
--- a/src/Pure/RAW/ROOT_polyml.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Thu Mar 03 11:12:02 2016 +0100
@@ -7,10 +7,7 @@
(* 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";
+use "RAW/ml_name_space.ML";
if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
else use "RAW/fixed_int_dummy.ML";
@@ -29,13 +26,6 @@
end;
-(* ML heap operations *)
-
-if ML_System.name = "polyml-5.3.0"
-then use "RAW/ml_heap_polyml-5.3.0.ML"
-else use "RAW/ml_heap.ML";
-
-
(* exceptions *)
fun reraise exn =
@@ -46,27 +36,16 @@
exception Interrupt = SML90.Interrupt;
use "RAW/exn.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/exn_trace.ML"
-else use "RAW/exn_trace_raw.ML";
+use "RAW/exn_trace.ML";
(* 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";
-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";
@@ -93,9 +72,8 @@
(* 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";
+use "RAW/ml_heap.ML";
+use "RAW/ml_profiling.ML";
val pointer_eq = PolyML.pointerEq;
@@ -162,10 +140,6 @@
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/ml_positions.ML";
use "RAW/ml_compiler0.ML";
@@ -175,10 +149,6 @@
PolyML.Compiler.prompt1 := "ML> ";
PolyML.Compiler.prompt2 := "ML# ";
-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 ml_make_string struct_name =
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
struct_name ^ ".ML_print_depth ()))))))";
@@ -186,6 +156,4 @@
(* ML debugger *)
-if ML_System.name = "polyml-5.6"
-then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
-else use_no_debug "RAW/ml_debugger.ML";
+use_no_debug "RAW/ml_debugger.ML";
--- a/src/Pure/RAW/exn_trace_raw.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Title: Pure/RAW/exn_trace_raw.ML
- Author: Makarius
-
-Raw exception trace for Poly/ML 5.3.0.
-*)
-
-fun print_exception_trace (_: exn -> string) (_: string -> unit) =
- PolyML.exception_trace;
--- a/src/Pure/RAW/ml_compiler0.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ml_compiler0.ML Thu Mar 03 11:12:02 2016 +0100
@@ -58,8 +58,8 @@
PolyML.Compiler.CPErrorMessageProc put_message,
PolyML.Compiler.CPLineNo (fn () => ! current_line),
PolyML.Compiler.CPFileName file,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
- ML_Compiler_Parameters.debug debug;
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+ PolyML.Compiler.CPDebug debug];
val _ =
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
--- a/src/Pure/RAW/ml_compiler_parameters.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: Pure/RAW/ml_compiler_parameters.ML
- Author: Makarius
-
-Additional ML compiler parameters for Poly/ML.
-*)
-
-signature ML_COMPILER_PARAMETERS =
-sig
- val debug: bool -> PolyML.Compiler.compilerParameters list
-end;
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug _ = [];
-
-end;
\ No newline at end of file
--- a/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(* Title: Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
- Author: Makarius
-
-Additional ML compiler parameters for Poly/ML 5.6, or later.
-*)
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug b = [PolyML.Compiler.CPDebug b];
-
-end;
\ No newline at end of file
--- a/src/Pure/RAW/ml_debugger.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ml_debugger.ML Thu Mar 03 11:12:02 2016 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/RAW/ml_debugger.ML
Author: Makarius
-ML debugger interface -- dummy version.
+ML debugger interface -- for Poly/ML 5.6, or later.
*)
signature ML_DEBUGGER =
@@ -10,16 +10,17 @@
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 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_location: state -> location
val debug_name_space: state -> ML_Name_Space.T
val debug_local_name_space: state -> ML_Name_Space.T
end;
@@ -29,36 +30,43 @@
(* exceptions *)
-abstype exn_id = Exn_Id of string
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
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*)
+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, FixedInt.fromInt (size s))) end);
+
(* hooks *)
-fun on_entry _ = ();
-fun on_exit _ = ();
-fun on_exit_exception _ = ();
-fun on_breakpoint _ = ();
+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 *)
+(* debugger operations *)
-fun fail () = raise Fail "No debugger support on this ML platform";
-
-type state = unit;
+type state = PolyML.DebuggerInterface.debugState;
-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 ();
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
end;
--- a/src/Pure/RAW/ml_debugger_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(* 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, FixedInt.fromInt (size s))) end);
-
-
-(* hooks *)
-
-type location = PolyML.location;
-
-val on_entry = PolyML.DebuggerInterface.setOnEntry;
-val on_exit = PolyML.DebuggerInterface.setOnExit;
-val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-
-
-(* debugger operations *)
-
-type state = PolyML.DebuggerInterface.debugState;
-
-val state = PolyML.DebuggerInterface.debugState;
-val debug_function = PolyML.DebuggerInterface.debugFunction;
-val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
-val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
-val debug_location = PolyML.DebuggerInterface.debugLocation;
-val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
-val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
-
-end;
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: Pure/RAW/ml_heap_polyml-5.3.0.ML
- Author: Makarius
-
-ML heap operations.
-*)
-
-signature ML_HEAP =
-sig
- val share_common_data: unit -> unit
- val save_state: string -> unit
-end;
-
-structure ML_Heap: ML_HEAP =
-struct
- fun share_common_data () = ();
- val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_name_space.ML Thu Mar 03 11:12:02 2016 +0100
@@ -0,0 +1,33 @@
+(* Title: Pure/RAW/ml_name_space.ML
+ Author: Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+ val forget_global_structure = PolyML.Compiler.forgetStructure;
+
+ type valueVal = Values.value;
+ fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
+ fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+
+ type typeVal = TypeConstrs.typeConstr;
+ fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+
+ type fixityVal = Infixes.fixity;
+ fun displayFix (_: string, x) = Infixes.print x;
+
+ type structureVal = Structures.structureVal;
+ fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+
+ type signatureVal = Signatures.signatureVal;
+ fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+
+ type functorVal = Functors.functorVal;
+ fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+end;
--- a/src/Pure/RAW/ml_name_space_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* 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;
--- a/src/Pure/RAW/ml_name_space_polyml.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* 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;
--- a/src/Pure/RAW/ml_parse_tree.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/RAW/ml_parse_tree.ML
- Author: Makarius
-
-Additional ML parse tree components for Poly/ML.
-*)
-
-signature ML_PARSE_TREE =
-sig
- val completions: PolyML.ptProperties -> string list option
- val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
-end;
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions _ = NONE;
-fun breakpoint _ = NONE;
-
-end;
\ No newline at end of file
--- a/src/Pure/RAW/ml_parse_tree_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/RAW/ml_parse_tree_polyml-5.6.ML
- Author: Makarius
-
-Additional ML parse tree components for Poly/ML 5.6, or later.
-*)
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions (PolyML.PTcompletions x) = SOME x
- | completions _ = NONE;
-
-fun breakpoint (PolyML.PTbreakPoint x) = SOME x
- | breakpoint _ = NONE;
-
-end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_profiling.ML Thu Mar 03 11:12:02 2016 +0100
@@ -0,0 +1,19 @@
+(* Title: Pure/RAW/ml_profiling.ML
+ Author: Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+ PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+ PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+ PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;
--- a/src/Pure/RAW/ml_profiling_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* 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;
--- a/src/Pure/RAW/ml_profiling_polyml.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* 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;
--- a/src/Pure/RAW/ml_stack_dummy.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* 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;
--- a/src/Pure/RAW/ml_stack_polyml-5.6.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* 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;
--- a/src/Pure/RAW/multithreading.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/multithreading.ML Thu Mar 03 11:12:02 2016 +0100
@@ -88,8 +88,13 @@
(* options *)
+fun num_processors () =
+ (case Thread.numPhysicalProcessors () of
+ SOME n => n
+ | NONE => Thread.numProcessors ());
+
fun max_threads_result m =
- if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
+ if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
val max_threads = ref 1;
--- a/src/Pure/RAW/single_assignment_polyml.ML Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* 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;
--- a/src/Pure/ROOT Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ROOT Thu Mar 03 11:12:02 2016 +0100
@@ -3,65 +3,39 @@
session RAW =
theories
files
- "RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace.ML"
- "RAW/exn_trace_raw.ML"
"RAW/fixed_int_dummy.ML"
"RAW/ml_compiler0.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_heap.ML"
- "RAW/ml_heap_polyml-5.3.0.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_name_space.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_profiling.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
"RAW/secure.ML"
- "RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
session Pure =
global_theories Pure
files
- "RAW/ROOT_polyml-5.6.ML"
"RAW/ROOT_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace.ML"
- "RAW/exn_trace_raw.ML"
"RAW/fixed_int_dummy.ML"
"RAW/ml_compiler0.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_heap.ML"
- "RAW/ml_heap_polyml-5.3.0.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_name_space.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_profiling.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
"RAW/secure.ML"
- "RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
"Concurrent/bash.ML"
--- a/src/Pure/ROOT.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ROOT.ML Thu Mar 03 11:12:02 2016 +0100
@@ -101,9 +101,7 @@
use "ML/exn_properties.ML";
-if ML_System.name = "polyml-5.6"
-then use "ML/ml_statistics.ML"
-else use "ML/ml_statistics_dummy.ML";
+use "ML/ml_statistics.ML";
use "Concurrent/standard_thread.ML";
use "Concurrent/single_assignment.ML";
--- a/src/Pure/System/system_channel.ML Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/System/system_channel.ML Thu Mar 03 11:12:02 2016 +0100
@@ -32,8 +32,7 @@
in read [] end;
fun inputN (System_Channel (in_stream, _)) n =
- if n = 0 then "" (*workaround for polyml-5.5.1 or earlier*)
- else Byte.bytesToString (BinIO.inputN (in_stream, n));
+ Byte.bytesToString (BinIO.inputN (in_stream, n));
fun output (System_Channel (_, out_stream)) s =
File.output out_stream s;