# HG changeset patch
# User wenzelm
# Date 1275155189 -7200
# Node ID 349e9223c685a37ea36bd0fd3f14eb1960fb25ca
# Parent  64da21a2c6c7a0740f1ad6a0dce49366c9615b82
explicit markup for forked goals, as indicated by Goal.fork;
accumulate pending forks within command state and hilight accordingly;
Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;

diff -r 64da21a2c6c7 -r 349e9223c685 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat May 29 17:26:02 2010 +0200
+++ b/src/HOL/Tools/record.ML	Sat May 29 19:46:29 2010 +0200
@@ -1038,7 +1038,7 @@
   let val thm =
     if ! quick_and_dirty then Skip_Proof.make_thm thy prop
     else if Goal.future_enabled () then
-      Goal.future_result (ProofContext.init_global thy) (Future.fork_pri ~1 prf) prop
+      Goal.future_result (ProofContext.init_global thy) (Goal.fork prf) prop
     else prf ()
   in Drule.export_without_context thm end;
 
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/General/markup.ML	Sat May 29 19:46:29 2010 +0200
@@ -102,6 +102,8 @@
   val taskN: string
   val unprocessedN: string val unprocessed: T
   val runningN: string val running: string -> T
+  val forkedN: string val forked: T
+  val joinedN: string val joined: T
   val failedN: string val failed: T
   val finishedN: string val finished: T
   val disposedN: string val disposed: T
@@ -299,6 +301,8 @@
 
 val (unprocessedN, unprocessed) = markup_elem "unprocessed";
 val (runningN, running) = markup_string "running" taskN;
+val (forkedN, forked) = markup_elem "forked";
+val (joinedN, joined) = markup_elem "joined";
 val (failedN, failed) = markup_elem "failed";
 val (finishedN, finished) = markup_elem "finished";
 val (disposedN, disposed) = markup_elem "disposed";
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/General/markup.scala	Sat May 29 19:46:29 2010 +0200
@@ -172,6 +172,8 @@
 
   val UNPROCESSED = "unprocessed"
   val RUNNING = "running"
+  val FORKED = "forked"
+  val JOINED = "joined"
   val FAILED = "failed"
   val FINISHED = "finished"
   val DISPOSED = "disposed"
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Sat May 29 19:46:29 2010 +0200
@@ -1070,9 +1070,10 @@
 local
 
 fun future_terminal_proof proof1 proof2 meths int state =
-  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
+  if not (Goal.local_future_enforced ()) andalso
+    int orelse is_relevant state orelse not (Goal.local_future_enabled ())
   then proof1 meths state
-  else snd (proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))) state);
+  else snd (proof2 (fn state' => Goal.fork (fn () => ((), proof1 meths state'))) state);
 
 in
 
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat May 29 19:46:29 2010 +0200
@@ -180,7 +180,7 @@
     require(assignment.is_finished)
     (assignment.join).get(cmd) match {
       case Some(cmd_state) => cmd_state.current_state
-      case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
+      case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
     }
   }
 }
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Sat May 29 19:46:29 2010 +0200
@@ -11,23 +11,27 @@
 class State(
   val command: Command,
   val status: Command.Status.Value,
+  val forks: Int,
   val reverse_results: List[XML.Tree],
   val markup_root: Markup_Text)
 {
   def this(command: Command) =
-    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
+    this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
 
 
   /* content */
 
   private def set_status(st: Command.Status.Value): State =
-    new State(command, st, reverse_results, markup_root)
+    new State(command, st, forks, reverse_results, markup_root)
+
+  private def add_forks(i: Int): State =
+    new State(command, status, forks + i, reverse_results, markup_root)
 
   private def add_result(res: XML.Tree): State =
-    new State(command, status, res :: reverse_results, markup_root)
+    new State(command, status, forks, res :: reverse_results, markup_root)
 
   private def add_markup(node: Markup_Tree): State =
-    new State(command, status, reverse_results, markup_root + node)
+    new State(command, status, forks, reverse_results, markup_root + node)
 
   lazy val results = reverse_results.reverse
 
@@ -78,6 +82,8 @@
             case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
             case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
             case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
+            case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1)
+            case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1)
             case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
               atts match {
                 case Position.Range(begin, end) =>
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sat May 29 19:46:29 2010 +0200
@@ -93,6 +93,7 @@
   setup_channels out |> init_message;
   Keyword.report ();
   Output.status (Markup.markup Markup.ready "");
+  Goal.parallel_proofs := 3;
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
 
 end;
diff -r 64da21a2c6c7 -r 349e9223c685 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat May 29 17:26:02 2010 +0200
+++ b/src/Pure/goal.ML	Sat May 29 19:46:29 2010 +0200
@@ -23,8 +23,10 @@
   val check_finished: Proof.context -> thm -> unit
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
+  val fork: (unit -> 'a) -> 'a future
   val future_enabled: unit -> bool
   val local_future_enabled: unit -> bool
+  val local_future_enforced: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -100,7 +102,14 @@
   #> Drule.zero_var_indexes;
 
 
-(* future_enabled *)
+(* parallel proofs *)
+
+fun fork e = Future.fork_pri ~1 (fn () =>
+  let
+    val _ = Output.status (Markup.markup Markup.forked "");
+    val x = e ();  (*sic*)
+    val _ = Output.status (Markup.markup Markup.joined "");
+  in x end);
 
 val parallel_proofs = Unsynchronized.ref 1;
 
@@ -108,6 +117,7 @@
   Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
 
 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
+fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
 
 
 (* future_result *)
@@ -198,7 +208,7 @@
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
-      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
+      else future_result ctxt' (fork result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
diff -r 64da21a2c6c7 -r 349e9223c685 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat May 29 17:26:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat May 29 19:46:29 2010 +0200
@@ -25,12 +25,16 @@
 {
   def choose_color(command: Command, doc: Document): Color =
   {
-    doc.current_state(command).status match {
-      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
-      case Command.Status.FINISHED => new Color(234, 248, 255)
-      case Command.Status.FAILED => new Color(255, 193, 193)
-      case Command.Status.UNDEFINED => Color.red
-    }
+    val state = doc.current_state(command)
+    if (state.forks > 0) new Color(255, 228, 225)
+    else if (state.forks < 0) Color.red
+    else
+      state.status match {
+        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+        case Command.Status.FINISHED => new Color(234, 248, 255)
+        case Command.Status.FAILED => new Color(255, 193, 193)
+        case Command.Status.UNDEFINED => Color.red
+      }
   }