# HG changeset patch # User wenzelm # Date 1449439808 -3600 # Node ID 4c232a2ddeab10bf9fab64ee9af5f6c4768398cd # Parent 4c9e1e5a240e58e83e81a6c186348fb09c84b8b7 discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6; diff -r 4c9e1e5a240e -r 4c232a2ddeab lib/scripts/run-polyml-5.5.3 --- a/lib/scripts/run-polyml-5.5.3 Sun Dec 06 17:27:42 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,106 +0,0 @@ -#!/usr/bin/env bash -# :mode=shellscript: -# -# Author: Makarius -# -# Startup script for Poly/ML 5.5.3. - -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE - - -## diagnostics - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -function fail_out() -{ - fail "Unable to create output heap file: \"$OUTFILE\"" -} - -function check_file() -{ - [ ! -f "$1" ] && fail "Unable to locate \"$1\"" -} - - -## compiler executables and libraries - -[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)" - -POLY="$ML_HOME/poly" -check_file "$POLY" - -librarypath "$ML_HOME" - - - -## prepare databases - -case "$ML_PLATFORM" in - *-windows) - PLATFORM_INFILE="$(platform_path -m "$INFILE")" - PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")" - ;; - *) - PLATFORM_INFILE="$INFILE" - PLATFORM_OUTFILE="$OUTFILE" - ;; -esac - -if [ -z "$INFILE" ]; then - INIT="" - case "$ML_PLATFORM" in - *-windows) - EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));" - ;; - *) - EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);" - ;; - esac -else - check_file "$INFILE" - INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));" - EXIT="" -fi - -if [ -z "$OUTFILE" ]; then - MLEXIT="" -else - if [ -z "$INFILE" ]; then - MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);" - else - MLEXIT="Session.save \"$OUTFILE\";" - fi - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } -fi - - -## run it! - -MLTEXT="$INIT $EXIT $MLTEXT" - -if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then - "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \ - --error-exit 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 -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; - -end; diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML Sun Dec 06 23:10:08 2015 +0100 @@ -0,0 +1,70 @@ +(* 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 +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; + +end; diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML --- a/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML Sun Dec 06 17:27:42 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* Title: Pure/ML/ml_parse_tree_polyml-5.5.3.ML - Author: Makarius - -Additional ML parse tree components for Poly/ML 5.5.3, 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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML Sun Dec 06 23:10:08 2015 +0100 @@ -0,0 +1,16 @@ +(* 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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML --- a/src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML Sun Dec 06 17:27:42 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* Title: Pure/ML-Systems/ml_stack_polyml-5.5.3.ML - -Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, 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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_stack_polyml-5.6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/ml_stack_polyml-5.6.ML Sun Dec 06 23:10:08 2015 +0100 @@ -0,0 +1,16 @@ +(* 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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/polyml-5.5.3.ML --- a/src/Pure/ML-Systems/polyml-5.5.3.ML Sun Dec 06 17:27:42 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: Pure/ML-Systems/polyml-5.5.3.ML - Author: Makarius - -Compatibility wrapper for Poly/ML 5.5.3. -*) - -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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Sun Dec 06 17:27:42 2015 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Sun Dec 06 23:10:08 2015 +0100 @@ -60,7 +60,6 @@ if ML_System.name = "polyml-5.5.1" orelse ML_System.name = "polyml-5.5.2" - orelse ML_System.name = "polyml-5.5.3" orelse ML_System.name = "polyml-5.6" then use "ML-Systems/exn_trace_polyml-5.5.1.ML" else (); @@ -78,9 +77,8 @@ use "ML-Systems/multithreading.ML"; use "ML-Systems/multithreading_polyml.ML"; -if ML_System.name = "polyml-5.5.3" - orelse ML_System.name = "polyml-5.6" -then use "ML-Systems/ml_stack_polyml-5.5.3.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"; @@ -176,9 +174,8 @@ end; use "ML-Systems/ml_compiler_parameters.ML"; -if ML_System.name = "polyml-5.5.3" - orelse ML_System.name = "polyml-5.6" -then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else (); +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"; @@ -191,9 +188,8 @@ 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.5.3" - orelse ML_System.name = "polyml-5.6" -then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else (); +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} @@ -206,7 +202,6 @@ (* ML debugger *) -if ML_System.name = "polyml-5.5.3" - orelse ML_System.name = "polyml-5.6" -then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" +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 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ROOT --- a/src/Pure/ROOT Sun Dec 06 17:27:42 2015 +0100 +++ b/src/Pure/ROOT Sun Dec 06 23:10:08 2015 +0100 @@ -7,26 +7,26 @@ "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.5.3.ML" + "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" "ML-Systems/ml_debugger.ML" - "ML-Systems/ml_debugger_polyml-5.5.3.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.5.3.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.5.3.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.5.3.ML" + "ML-Systems/polyml-5.6.ML" "ML-Systems/polyml-5.6.ML" "ML-Systems/polyml.ML" "ML-Systems/pp_dummy.ML" @@ -48,26 +48,25 @@ "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.5.3.ML" + "ML-Systems/ml_compiler_parameters_polyml-5.6.ML" "ML-Systems/ml_debugger.ML" - "ML-Systems/ml_debugger_polyml-5.5.3.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.5.3.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.5.3.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.5.3.ML" "ML-Systems/polyml-5.6.ML" "ML-Systems/polyml.ML" "ML-Systems/pp_dummy.ML" diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Dec 06 17:27:42 2015 +0100 +++ b/src/Pure/ROOT.ML Sun Dec 06 23:10:08 2015 +0100 @@ -105,7 +105,6 @@ if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1" orelse ML_System.name = "polyml-5.5.2" - orelse ML_System.name = "polyml-5.5.3" orelse ML_System.name = "polyml-5.6" then use "ML/ml_statistics_polyml-5.5.0.ML" else use "ML/ml_statistics_dummy.ML";