explicit markup for forked goals, as indicated by Goal.fork;
authorwenzelm
Sat May 29 19:46:29 2010 +0200 (2010-05-29 ago)
changeset 37186349e9223c685
parent 37185 64da21a2c6c7
child 37187 dc1927a0f534
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;
src/HOL/Tools/record.ML
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/Isar/proof.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/state.scala
src/Pure/System/isabelle_process.ML
src/Pure/goal.ML
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/HOL/Tools/record.ML	Sat May 29 17:26:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat May 29 19:46:29 2010 +0200
     1.3 @@ -1038,7 +1038,7 @@
     1.4    let val thm =
     1.5      if ! quick_and_dirty then Skip_Proof.make_thm thy prop
     1.6      else if Goal.future_enabled () then
     1.7 -      Goal.future_result (ProofContext.init_global thy) (Future.fork_pri ~1 prf) prop
     1.8 +      Goal.future_result (ProofContext.init_global thy) (Goal.fork prf) prop
     1.9      else prf ()
    1.10    in Drule.export_without_context thm end;
    1.11  
     2.1 --- a/src/Pure/General/markup.ML	Sat May 29 17:26:02 2010 +0200
     2.2 +++ b/src/Pure/General/markup.ML	Sat May 29 19:46:29 2010 +0200
     2.3 @@ -102,6 +102,8 @@
     2.4    val taskN: string
     2.5    val unprocessedN: string val unprocessed: T
     2.6    val runningN: string val running: string -> T
     2.7 +  val forkedN: string val forked: T
     2.8 +  val joinedN: string val joined: T
     2.9    val failedN: string val failed: T
    2.10    val finishedN: string val finished: T
    2.11    val disposedN: string val disposed: T
    2.12 @@ -299,6 +301,8 @@
    2.13  
    2.14  val (unprocessedN, unprocessed) = markup_elem "unprocessed";
    2.15  val (runningN, running) = markup_string "running" taskN;
    2.16 +val (forkedN, forked) = markup_elem "forked";
    2.17 +val (joinedN, joined) = markup_elem "joined";
    2.18  val (failedN, failed) = markup_elem "failed";
    2.19  val (finishedN, finished) = markup_elem "finished";
    2.20  val (disposedN, disposed) = markup_elem "disposed";
     3.1 --- a/src/Pure/General/markup.scala	Sat May 29 17:26:02 2010 +0200
     3.2 +++ b/src/Pure/General/markup.scala	Sat May 29 19:46:29 2010 +0200
     3.3 @@ -172,6 +172,8 @@
     3.4  
     3.5    val UNPROCESSED = "unprocessed"
     3.6    val RUNNING = "running"
     3.7 +  val FORKED = "forked"
     3.8 +  val JOINED = "joined"
     3.9    val FAILED = "failed"
    3.10    val FINISHED = "finished"
    3.11    val DISPOSED = "disposed"
     4.1 --- a/src/Pure/Isar/proof.ML	Sat May 29 17:26:02 2010 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Sat May 29 19:46:29 2010 +0200
     4.3 @@ -1070,9 +1070,10 @@
     4.4  local
     4.5  
     4.6  fun future_terminal_proof proof1 proof2 meths int state =
     4.7 -  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
     4.8 +  if not (Goal.local_future_enforced ()) andalso
     4.9 +    int orelse is_relevant state orelse not (Goal.local_future_enabled ())
    4.10    then proof1 meths state
    4.11 -  else snd (proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))) state);
    4.12 +  else snd (proof2 (fn state' => Goal.fork (fn () => ((), proof1 meths state'))) state);
    4.13  
    4.14  in
    4.15  
     5.1 --- a/src/Pure/PIDE/document.scala	Sat May 29 17:26:02 2010 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Sat May 29 19:46:29 2010 +0200
     5.3 @@ -180,7 +180,7 @@
     5.4      require(assignment.is_finished)
     5.5      (assignment.join).get(cmd) match {
     5.6        case Some(cmd_state) => cmd_state.current_state
     5.7 -      case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
     5.8 +      case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
     5.9      }
    5.10    }
    5.11  }
     6.1 --- a/src/Pure/PIDE/state.scala	Sat May 29 17:26:02 2010 +0200
     6.2 +++ b/src/Pure/PIDE/state.scala	Sat May 29 19:46:29 2010 +0200
     6.3 @@ -11,23 +11,27 @@
     6.4  class State(
     6.5    val command: Command,
     6.6    val status: Command.Status.Value,
     6.7 +  val forks: Int,
     6.8    val reverse_results: List[XML.Tree],
     6.9    val markup_root: Markup_Text)
    6.10  {
    6.11    def this(command: Command) =
    6.12 -    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
    6.13 +    this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
    6.14  
    6.15  
    6.16    /* content */
    6.17  
    6.18    private def set_status(st: Command.Status.Value): State =
    6.19 -    new State(command, st, reverse_results, markup_root)
    6.20 +    new State(command, st, forks, reverse_results, markup_root)
    6.21 +
    6.22 +  private def add_forks(i: Int): State =
    6.23 +    new State(command, status, forks + i, reverse_results, markup_root)
    6.24  
    6.25    private def add_result(res: XML.Tree): State =
    6.26 -    new State(command, status, res :: reverse_results, markup_root)
    6.27 +    new State(command, status, forks, res :: reverse_results, markup_root)
    6.28  
    6.29    private def add_markup(node: Markup_Tree): State =
    6.30 -    new State(command, status, reverse_results, markup_root + node)
    6.31 +    new State(command, status, forks, reverse_results, markup_root + node)
    6.32  
    6.33    lazy val results = reverse_results.reverse
    6.34  
    6.35 @@ -78,6 +82,8 @@
    6.36              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    6.37              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    6.38              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    6.39 +            case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1)
    6.40 +            case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1)
    6.41              case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
    6.42                atts match {
    6.43                  case Position.Range(begin, end) =>
     7.1 --- a/src/Pure/System/isabelle_process.ML	Sat May 29 17:26:02 2010 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Sat May 29 19:46:29 2010 +0200
     7.3 @@ -93,6 +93,7 @@
     7.4    setup_channels out |> init_message;
     7.5    Keyword.report ();
     7.6    Output.status (Markup.markup Markup.ready "");
     7.7 +  Goal.parallel_proofs := 3;
     7.8    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
     7.9  
    7.10  end;
     8.1 --- a/src/Pure/goal.ML	Sat May 29 17:26:02 2010 +0200
     8.2 +++ b/src/Pure/goal.ML	Sat May 29 19:46:29 2010 +0200
     8.3 @@ -23,8 +23,10 @@
     8.4    val check_finished: Proof.context -> thm -> unit
     8.5    val finish: Proof.context -> thm -> thm
     8.6    val norm_result: thm -> thm
     8.7 +  val fork: (unit -> 'a) -> 'a future
     8.8    val future_enabled: unit -> bool
     8.9    val local_future_enabled: unit -> bool
    8.10 +  val local_future_enforced: unit -> bool
    8.11    val future_result: Proof.context -> thm future -> term -> thm
    8.12    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    8.13    val prove_multi: Proof.context -> string list -> term list -> term list ->
    8.14 @@ -100,7 +102,14 @@
    8.15    #> Drule.zero_var_indexes;
    8.16  
    8.17  
    8.18 -(* future_enabled *)
    8.19 +(* parallel proofs *)
    8.20 +
    8.21 +fun fork e = Future.fork_pri ~1 (fn () =>
    8.22 +  let
    8.23 +    val _ = Output.status (Markup.markup Markup.forked "");
    8.24 +    val x = e ();  (*sic*)
    8.25 +    val _ = Output.status (Markup.markup Markup.joined "");
    8.26 +  in x end);
    8.27  
    8.28  val parallel_proofs = Unsynchronized.ref 1;
    8.29  
    8.30 @@ -108,6 +117,7 @@
    8.31    Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
    8.32  
    8.33  fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
    8.34 +fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
    8.35  
    8.36  
    8.37  (* future_result *)
    8.38 @@ -198,7 +208,7 @@
    8.39      val res =
    8.40        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
    8.41        then result ()
    8.42 -      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
    8.43 +      else future_result ctxt' (fork result) (Thm.term_of stmt);
    8.44    in
    8.45      Conjunction.elim_balanced (length props) res
    8.46      |> map (Assumption.export false ctxt' ctxt)
     9.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat May 29 17:26:02 2010 +0200
     9.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat May 29 19:46:29 2010 +0200
     9.3 @@ -25,12 +25,16 @@
     9.4  {
     9.5    def choose_color(command: Command, doc: Document): Color =
     9.6    {
     9.7 -    doc.current_state(command).status match {
     9.8 -      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
     9.9 -      case Command.Status.FINISHED => new Color(234, 248, 255)
    9.10 -      case Command.Status.FAILED => new Color(255, 193, 193)
    9.11 -      case Command.Status.UNDEFINED => Color.red
    9.12 -    }
    9.13 +    val state = doc.current_state(command)
    9.14 +    if (state.forks > 0) new Color(255, 228, 225)
    9.15 +    else if (state.forks < 0) Color.red
    9.16 +    else
    9.17 +      state.status match {
    9.18 +        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    9.19 +        case Command.Status.FINISHED => new Color(234, 248, 255)
    9.20 +        case Command.Status.FAILED => new Color(255, 193, 193)
    9.21 +        case Command.Status.UNDEFINED => Color.red
    9.22 +      }
    9.23    }
    9.24  
    9.25