# HG changeset patch
# User wenzelm
# Date 1358537482 -3600
# Node ID 21da2a03b9d2cfd9e1ce902008643645b5c6eae4
# Parent  4a2c82644889b94b9c9b53133e45837c6571ba00# Parent  20edcc6a8def03819d4fc67b113a579f6a08e9da
merged

diff -r 4a2c82644889 -r 21da2a03b9d2 Admin/Windows/Cygwin/isabelle/postinstall
--- a/Admin/Windows/Cygwin/isabelle/postinstall	Fri Jan 18 20:01:59 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/postinstall	Fri Jan 18 20:31:22 2013 +0100
@@ -1,8 +1,12 @@
-#!/bin/dash
+#!/bin/bash
 
 PATH=/bin
 
+CONTRIB="$(cygpath -u "$(cygpath -w /)\..")"
+peflags -x8192000 -z500 "$CONTRIB/polyml-5.5.0/x86-cygwin/poly.exe"
+
 bash /etc/postinstall/base-files-mketc.sh.done
 
 mkpasswd -l >/etc/passwd
 mkgroup -l >/etc/group
+
diff -r 4a2c82644889 -r 21da2a03b9d2 Admin/Windows/Cygwin/isabelle/rebaseall
--- a/Admin/Windows/Cygwin/isabelle/rebaseall	Fri Jan 18 20:01:59 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/rebaseall	Fri Jan 18 20:31:22 2013 +0100
@@ -14,3 +14,4 @@
 dash /bin/rebaseall -T "$FILE_LIST"
 
 rm -f "$FILE_LIST"
+
diff -r 4a2c82644889 -r 21da2a03b9d2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 20:31:22 2013 +0100
@@ -5445,7 +5445,7 @@
 have *: "S Int closure T = S" using assms by auto
 have "~(rel_interior S <= rel_frontier T)"
      using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
-     closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
+     closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
      using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -52,6 +52,7 @@
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
   val ML_statistics: bool Unsynchronized.ref
+  val forked_proofs: int Unsynchronized.ref
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
@@ -187,6 +188,7 @@
 (* status *)
 
 val ML_statistics = Unsynchronized.ref false;
+val forked_proofs = Unsynchronized.ref 0;
 
 fun report_status () = (*requires SYNCHRONIZED*)
   if ! ML_statistics then
@@ -197,6 +199,7 @@
       val waiting = count_workers Waiting;
       val stats =
        [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+        ("tasks_proof", Markup.print_int (! forked_proofs)),
         ("tasks_ready", Markup.print_int ready),
         ("tasks_pending", Markup.print_int pending),
         ("tasks_running", Markup.print_int running),
@@ -253,12 +256,11 @@
       Task_Queue.running task (fn () =>
         setmp_worker_task task (fn () =>
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
-    val _ = Multithreading.tracing 2 (fn () =>
-      let
-        val s = Task_Queue.str_of_task_groups task;
-        fun micros time = string_of_int (Time.toNanoseconds time div 1000);
-        val (run, wait, deps) = Task_Queue.timing_of_task task;
-      in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
+    val _ =
+      if ! Multithreading.trace >= 2 then
+        Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
+          handle Fail msg => warning msg
+      else ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -22,7 +22,7 @@
   val pri_of_task: task -> int
   val str_of_task: task -> string
   val str_of_task_groups: task -> string
-  val timing_of_task: task -> Time.time * Time.time * string list
+  val task_statistics: task -> Properties.T
   val running: task -> (unit -> 'a) -> 'a
   val joining: task -> (unit -> 'a) -> 'a
   val waiting: task -> task list -> (unit -> 'a) -> 'a
@@ -114,14 +114,17 @@
   name: string,
   id: int,
   pri: int option,
-  timing: timing Synchronized.var option}
+  timing: timing Synchronized.var option,
+  pos: Position.T}
 with
 
 val dummy_task =
-  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
+  Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
+    pos = Position.none};
 
 fun new_task group name pri =
-  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
+  Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
+    pos = Position.thread_data ()};
 
 fun group_of_task (Task {group, ...}) = group;
 fun name_of_task (Task {name, ...}) = name;
@@ -132,9 +135,6 @@
 
 fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
 
-fun timing_of_task (Task {timing, ...}) =
-  (case timing of NONE => timing_start | SOME var => Synchronized.value var);
-
 fun update_timing update (Task {timing, ...}) e =
   uninterruptible (fn restore_attributes => fn () =>
     let
@@ -147,6 +147,18 @@
 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
   prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
 
+fun task_statistics (Task {name, id, timing, pos, ...}) =
+  let
+    val (run, wait, wait_deps) =
+      (case timing of NONE => timing_start | SOME var => Synchronized.value var);
+    fun micros time = string_of_int (Time.toNanoseconds time div 1000);
+  in
+    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+     ("task_name", name), ("task_id", Markup.print_int id),
+     ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
+    Position.properties_of pos
+  end;
+
 end;
 
 structure Tasks = Table(type key = task val ord = task_ord);
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Jan 18 20:31:22 2013 +0100
@@ -43,7 +43,8 @@
     ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
 
   val tasks_fields =
-    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+    ("Future tasks",
+      List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
 
   val workers_fields =
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -134,6 +134,7 @@
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
+  val task_statistics: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val no_output: Output.output * Output.output
@@ -412,6 +413,8 @@
 
 val ML_statistics = (functionN, "ML_statistics");
 
+val task_statistics = (functionN, "task_statistics");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 18 20:31:22 2013 +0100
@@ -330,6 +330,15 @@
         case _ => None
       }
   }
+
+  object Task_Statistics
+  {
+    def unapply(props: Properties.T): Option[Properties.T] =
+      props match {
+        case (FUNCTION, "task_statistics") :: stats => Some(stats)
+        case _ => None
+      }
+  }
 }
 
 
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/System/session.scala	Fri Jan 18 20:31:22 2013 +0100
@@ -364,6 +364,9 @@
         case Markup.ML_Statistics(props) if output.is_protocol =>
           statistics.event(Session.Statistics(props))
 
+        case Markup.Task_Statistics(props) if output.is_protocol =>
+          // FIXME
+
         case _ if output.is_init =>
           phase = Session.Ready
 
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Tools/build.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -19,13 +19,21 @@
       else NONE
   | ML_statistics _ _ = NONE;
 
+fun task_statistics (function :: stats) "" =
+      if function = Markup.task_statistics then SOME stats
+      else NONE
+  | task_statistics _ _ = NONE;
+
 fun protocol_message props output =
   (case ML_statistics props output of
     SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
   | NONE =>
-      (case Markup.dest_loading_theory props of
-        SOME name => writeln ("\floading_theory = " ^ name)
-      | NONE => raise Fail "Undefined Output.protocol_message"));
+      (case task_statistics props output of
+        SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
+      | NONE =>
+          (case Markup.dest_loading_theory props of
+            SOME name => writeln ("\floading_theory = " ^ name)
+          | NONE => raise Fail "Undefined Output.protocol_message")));
 
 
 (* build *)
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Tools/build.scala	Fri Jan 18 20:31:22 2013 +0100
@@ -561,14 +561,16 @@
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
 
-  sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
+  sealed case class Log_Info(
+    stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
 
   def parse_log(text: String): Log_Info =
   {
     val lines = split_lines(text)
     val stats = Props.parse_lines("\fML_statistics = ", lines)
+    val tasks = Props.parse_lines("\ftask_statistics = ", lines)
     val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
-    Log_Info(stats, timing)
+    Log_Info(stats, tasks, timing)
   }
 
 
diff -r 4a2c82644889 -r 21da2a03b9d2 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/goal.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -116,9 +116,7 @@
   Synchronized.change forked_proofs (fn (m, groups, tab) =>
     let
       val n = m + i;
-      val _ =
-        Multithreading.tracing 2 (fn () =>
-          ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
+      val _ = Future.forked_proofs := n;
     in (n, groups, tab) end);
 
 fun register_forked id future =
@@ -176,7 +174,7 @@
 
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
-    (groups, (0, [], Inttab.empty)));
+    (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
 
 end;