# HG changeset patch
# User wenzelm
# Date 1418391757 -3600
# Node ID e7f28b330cb2b74cfe259e314cc3fe6e0a38e3b8
# Parent  a71f2e256ee24dc9c50ddfba3e84d4149427c487# Parent  e557a9ddee5f4671475d6d0b69b5245f6eb71173
merged

diff -r a71f2e256ee2 -r e7f28b330cb2 NEWS
--- a/NEWS	Fri Dec 12 10:58:40 2014 +0100
+++ b/NEWS	Fri Dec 12 14:42:37 2014 +0100
@@ -235,6 +235,9 @@
 * Renamed "pairself" to "apply2", in accordance to @{apply 2}.
 INCOMPATIBILITY.
 
+* Synchronized.value (ML) is actually synchronized (as in Scala):
+subtle change of semantics with minimal potential for INCOMPATIBILITY.
+
 
 *** System ***
 
diff -r a71f2e256ee2 -r e7f28b330cb2 etc/settings
--- a/etc/settings	Fri Dec 12 10:58:40 2014 +0100
+++ b/etc/settings	Fri Dec 12 14:42:37 2014 +0100
@@ -14,7 +14,7 @@
 
 ISABELLE_SCALA_BUILD_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130"
 
-ISABELLE_JAVA_SYSTEM_OPTIONS="-Dfile.encoding=UTF-8 -server"
+ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Doc/Implementation/ML.thy	Fri Dec 12 14:42:37 2014 +0100
@@ -2019,8 +2019,8 @@
   individual exceptions by conventional @{verbatim "handle"} of ML.
 
   \item @{ML Par_Exn.release_first} is similar to @{ML
-  Par_Exn.release_all}, but only the first exception that has occurred
-  in the original evaluation process is raised again, the others are
+  Par_Exn.release_all}, but only the first (meaningful) exception that has
+  occurred in the original evaluation process is raised again, the others are
   ignored.  That single exception may get handled by conventional
   means in ML.
 
diff -r a71f2e256ee2 -r e7f28b330cb2 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Fri Dec 12 14:42:37 2014 +0100
@@ -265,7 +265,7 @@
 
 text \<open>Input source with position information:\<close>
 ML \<open>
-  val s: Input.source = \<open>abc\<close>;
+  val s: Input.source = \<open>abc123def456\<close>;
   writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
 
   \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
@@ -282,6 +282,4 @@
   val thms = [a, b, c];
 \<close>
 
-ML \<open>\<close>
-
 end
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Fri Dec 12 14:42:37 2014 +0100
@@ -56,21 +56,19 @@
 
 fun get_some f xs =
   let
-    exception FOUND of 'b option;
-    fun found (Exn.Exn (FOUND some)) = some
-      | found _ = NONE;
+    exception FOUND of 'b;
     val results =
       managed_results "Par_List.get_some"
-        (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
+        (fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs;
   in
-    (case get_first found results of
-      SOME y => SOME y
-    | NONE => (Par_Exn.release_first results; NONE))
+    (case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of
+      NONE => (Par_Exn.release_first results; NONE)
+    | some => some)
   end;
 
 fun find_some P = get_some (fn x => if P x then SOME x else NONE);
 
-fun exists P = is_some o get_some (fn x => if P x then SOME () else NONE);
+fun exists P = is_some o find_some P;
 fun forall P = not o exists (not o P);
 
 end;
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/Concurrent/par_list.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_list.scala	Fri Dec 12 14:42:37 2014 +0100
@@ -0,0 +1,68 @@
+/*  Title:      Pure/Concurrent/par_list.scala
+    Author:     Makarius
+
+Parallel list combinators.
+*/
+
+
+package isabelle
+
+
+import java.util.concurrent.{Future => JFuture, CancellationException}
+
+
+object Par_List
+{
+  def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
+    if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
+    else {
+      val state = Synchronized((List.empty[JFuture[Exn.Result[B]]], false))
+
+      def cancel_other(self: Int = -1): Unit =
+        state.change { case (tasks, canceled) =>
+          if (!canceled) {
+            for ((task, i) <- tasks.iterator.zipWithIndex if i != self)
+              task.cancel(true)
+          }
+          (tasks, true)
+        }
+
+      try {
+        state.change(_ =>
+          (xs.iterator.zipWithIndex.map({ case (x, self) =>
+            Simple_Thread.submit_task {
+              val result = Exn.capture { f(x) }
+              result match { case Exn.Exn(_) => cancel_other(self) case _ => }
+              result
+            }
+          }).toList, false))
+
+        state.value._1.map(future =>
+          try { future.get }
+          catch { case _: CancellationException => Exn.Exn(Exn.Interrupt()): Exn.Result[B] })
+      }
+      finally { cancel_other() }
+    }
+
+  def map[A, B](f: A => B, xs: List[A]): List[B] =
+    Exn.release_first(managed_results(f, xs))
+
+  def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] =
+  {
+    class Found(val res: B) extends Exception
+    val results =
+      managed_results(
+        (x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs)
+    results.collectFirst({ case Exn.Exn(found: Found) => found.res }) match {
+      case None => Exn.release_first(results); None
+      case some => some
+    }
+  }
+
+  def find_some[A](P: A => Boolean, xs: List[A]): Option[A] =
+    get_some((x: A) => if (P(x)) Some(x) else None, xs)
+
+  def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
+  def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
+}
+
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Concurrent/simple_thread.scala	Fri Dec 12 14:42:37 2014 +0100
@@ -9,9 +9,8 @@
 
 
 import java.lang.Thread
-import java.util.concurrent.{Callable, Future => JFuture}
-
-import scala.collection.parallel.ForkJoinTasks
+import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
+  TimeUnit, LinkedBlockingQueue}
 
 
 object Simple_Thread
@@ -41,7 +40,12 @@
 
   /* thread pool */
 
-  lazy val default_pool = ForkJoinTasks.defaultForkJoinPool
+  lazy val default_pool =
+    {
+      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+      val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+    }
 
   def submit_task[A](body: => A): JFuture[A] =
     default_pool.submit(new Callable[A] { def call = body })
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Dec 12 14:42:37 2014 +0100
@@ -33,7 +33,8 @@
   cond = ConditionVar.conditionVar (),
   var = Unsynchronized.ref x};
 
-fun value (Var {var, ...}) = ! var;
+fun value (Var {name, lock, var, ...}) =
+  Multithreading.synchronized name lock (fn () => ! var);
 
 
 (* synchronized access *)
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/General/exn.scala	Fri Dec 12 14:42:37 2014 +0100
@@ -26,6 +26,12 @@
       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 */
 
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Dec 12 14:42:37 2014 +0100
@@ -80,8 +80,7 @@
 val available = true;
 
 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 (Thread.numProcessors (), 1), 8);
 
 val max_threads = ref 1;
 
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Dec 12 14:42:37 2014 +0100
@@ -85,13 +85,11 @@
     def loaded_files: List[Path] =
     {
       val dep_files =
-        rev_deps.par.map(dep =>
-          Exn.capture {
-            dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
-          }).toList
-      ((Nil: List[Path]) /: dep_files) {
-        case (acc_files, files) => Exn.release(files) ::: acc_files
-      }
+        Par_List.map(
+          (dep: Dep) =>
+            dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)),
+          rev_deps)
+      ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }
   }
 
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Tools/build.scala	Fri Dec 12 14:42:37 2014 +0100
@@ -345,9 +345,7 @@
       val graph = tree.graph
       val sessions = graph.keys
 
-      val timings =
-        sessions.par.map((name: String) =>
-          Exn.capture { (name, load_timings(name)) }).toList.map(Exn.release(_))
+      val timings = Par_List.map((name: String) => (name, load_timings(name)), sessions)
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =
diff -r a71f2e256ee2 -r e7f28b330cb2 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/build-jars	Fri Dec 12 14:42:37 2014 +0100
@@ -14,6 +14,7 @@
   Concurrent/event_timer.scala
   Concurrent/future.scala
   Concurrent/mailbox.scala
+  Concurrent/par_list.scala
   Concurrent/simple_thread.scala
   Concurrent/synchronized.scala
   GUI/color_value.scala