support for polml-5.5.2;
support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890);
clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.5.2	Wed Dec 11 18:02:22 2013 +0100
@@ -0,0 +1,90 @@
+#!/usr/bin/env bash
+# :mode=shellscript:
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.5.2.
+
+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
+
+if [ -z "$INFILE" ]; then
+  INIT=""
+  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
+else
+  check_file "$INFILE"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+  COMMIT='fun commit () = false;'
+  MLEXIT=""
+else
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  MLEXIT="commit();"
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+    --error-exit </dev/null
+  RC="$?"
+else
+  if [ -z "$TERMINATE" ]; then
+    FEEDER_OPTS=""
+  else
+    FEEDER_OPTS="-q"
+    ML_OPTIONS="$ML_OPTIONS --error-exit"
+  fi
+  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+  RC="$?"
+fi
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:

--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Dec 11 18:02:22 2013 +0100
@@ -158,7 +158,7 @@
 if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-o quick_and_dirty -e 'Unsynchronized.setmp Multithreading.max_threads 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+  "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
 if ($output_log) {
   my $outcome = ($result ? "failure" : "success");

--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 11 18:02:22 2013 +0100
@@ -17,7 +17,7 @@
 declare [[sledgehammer_instantiate_inducts = false]]
 
 ML {*
-!Multithreading.max_threads
+Multithreading.max_threads_value ()
 *}
 
 ML {*

--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Dec 11 18:02:22 2013 +0100
@@ -19,7 +19,7 @@
 hide_fact (open) HOL.ext
 
 ML {*
-!Multithreading.max_threads
+Multithreading.max_threads_value ()
 *}
 
 ML {*

--- a/src/Pure/ML-Systems/multithreading.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -14,8 +14,9 @@
 sig
   include BASIC_MULTITHREADING
   val available: bool
-  val max_threads: int ref
   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
@@ -39,8 +40,9 @@
 (* options *)
 
 val available = false;
-val max_threads = ref (1: int);
 fun max_threads_value () = 1: int;
+fun max_threads_update _ = ();
+fun max_threads_setmp _ f x = f x;
 fun enabled () = false;
 
 

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -25,21 +25,6 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* options *)
-
-val available = true;
-
-val max_threads = ref 1;
-
-fun max_threads_value () =
-  let val m = ! max_threads in
-    if m > 0 then m
-    else Int.min (Int.max (Thread.numProcessors (), 1), 8)
-  end;
-
-fun enabled () = max_threads_value () > 1;
-
-
 (* thread attributes *)
 
 val no_interrupts =
@@ -90,6 +75,37 @@
     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
+    let val n =
+      (case Thread.numPhysicalProcessors () of
+        SOME n => n
+      | NONE => Thread.numProcessors ())
+    in Int.min (Int.max (n, 1), 8) end;
+
+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 =

--- a/src/Pure/ML-Systems/polyml.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -4,6 +4,25 @@
 Compatibility wrapper for Poly/ML.
 *)
 
+(* ML system operations *)
+
+use "ML-Systems/ml_system.ML";
+
+if ML_System.name = "polyml-5.3.0"
+then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
+else ();
+
+structure ML_System =
+struct
+
+open ML_System;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+val save_state = PolyML.SaveState.saveState;
+
+end;
+
+
 (* exceptions *)
 
 fun reraise exn =
@@ -25,6 +44,9 @@
 else use "ML-Systems/single_assignment_polyml.ML";
 
 open Thread;
+if ML_System.name = "polyml-5.5.2" then ()
+else use "ML-Systems/thread_physical_processors.ML";
+
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/multithreading_polyml.ML";
 
@@ -56,25 +78,6 @@
 fun quit () = exit 0;
 
 
-(* ML system operations *)
-
-use "ML-Systems/ml_system.ML";
-
-if ML_System.name = "polyml-5.3.0"
-then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
-else ();
-
-structure ML_System =
-struct
-
-open ML_System;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-val save_state = PolyML.SaveState.saveState;
-
-end;
-
-
 (* ML runtime system *)
 
 fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/thread_physical_processors.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -0,0 +1,12 @@
+(*  Title:      Pure/ML-Systems/thread_physical_processors.ML
+    Author:     Makarius
+
+Emulation of structure Thread in Poly/ML 5.5.2 (SVN 1890).
+*)
+
+structure Thread =
+struct
+  open Thread;
+
+  fun numPhysicalProcessors () : int option = NONE;
+end;

--- a/src/Pure/PIDE/protocol.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/PIDE/protocol.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -18,7 +18,7 @@
         Options.set_default options;
         Future.ML_statistics := true;
         Multithreading.trace := Options.int options "threads_trace";
-        Multithreading.max_threads := Options.int options "threads";
+        Multithreading.max_threads_update (Options.int options "threads");
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
       end);
 

--- a/src/Pure/ROOT	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ROOT	Wed Dec 11 18:02:22 2013 +0100
@@ -19,6 +19,7 @@
     "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
+    "ML-Systems/thread_physical_processors.ML"
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
@@ -41,6 +42,7 @@
     "ML-Systems/single_assignment_polyml.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
+    "ML-Systems/thread_physical_processors.ML"
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"

--- a/src/Pure/ROOT.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ROOT.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -76,10 +76,13 @@
 else use "ML/exn_properties_dummy.ML";
 
 if ML_System.name = "polyml-5.5.1"
+  orelse ML_System.name = "polyml-5.5.2"
 then use "ML/exn_trace_polyml-5.5.1.ML"
 else ();
 
-if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1"
+if ML_System.name = "polyml-5.5.0"
+  orelse ML_System.name = "polyml-5.5.1"
+  orelse ML_System.name = "polyml-5.5.2"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
 
@@ -347,5 +350,4 @@
 val cd = File.cd o Path.explode;
 
 Proofterm.proofs := 0;
-Multithreading.max_threads := 0;
 

--- a/src/Pure/System/isar.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/System/isar.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -155,6 +155,7 @@
 
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
+  Multithreading.max_threads_update (Options.default_int "threads");
   if do_init then init () else ();
   Output.Internal.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();

--- a/src/Pure/Tools/build.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/Tools/build.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -107,7 +107,7 @@
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
-    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+    |> Multithreading.max_threads_setmp (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
@@ -167,7 +167,7 @@
           (List.app (use_theories_condition last_timing)
             |> session_timing name verbose
             |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
-            |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+            |> Multithreading.max_threads_setmp (Options.int options "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();
       val _ = Par_Exn.release_all [res1, res2];

--- a/src/Pure/Tools/proof_general_pure.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -161,9 +161,11 @@
     "Record full proof objects internally";
 
 val _ =
-  ProofGeneral.preference_int ProofGeneral.category_proof
+  ProofGeneral.preference ProofGeneral.category_proof
     NONE
-    Multithreading.max_threads
+    (Markup.print_int o Multithreading.max_threads_value)
+    (Multithreading.max_threads_update o Markup.parse_int)
+    ProofGeneral.pgipint
     "max-threads"
     "Maximum number of threads";
 
@@ -172,7 +174,7 @@
     NONE
     (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
     (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
-    ProofGeneral.pgipbool
+    ProofGeneral.pgipint
     "parallel-proofs"
     "Check proofs in parallel";