# HG changeset patch # User wenzelm # Date 1346412205 -7200 # Node ID 4680c4046814d6a9420134d15e71b6ffcc1b178f # Parent 8e124393c281488312e617bb9da820a59aac6b30 further refinement of command status, to accomodate forked proofs; diff -r 8e124393c281 -r 4680c4046814 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Aug 30 22:38:12 2012 +0200 +++ b/src/Pure/PIDE/command.ML Fri Aug 31 13:23:25 2012 +0200 @@ -105,13 +105,13 @@ val is_proof = Keyword.is_proof (Toplevel.name_of tr); val _ = Multithreading.interrupted (); - val _ = Toplevel.status tr Isabelle_Markup.forked; + val _ = Toplevel.status tr Isabelle_Markup.running; val start = Timing.start (); val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st'); val errs = errs1 @ errs2; val _ = timing tr (Timing.result start); - val _ = Toplevel.status tr Isabelle_Markup.joined; + val _ = Toplevel.status tr Isabelle_Markup.finished; val _ = List.app (Toplevel.error_msg tr) errs; in (case result of @@ -122,7 +122,6 @@ in ((st, malformed'), no_print) end | SOME st' => let - val _ = Toplevel.status tr Isabelle_Markup.finished; val _ = proof_status tr st'; val do_print = not is_init andalso diff -r 8e124393c281 -r 4680c4046814 src/Pure/PIDE/isabelle_markup.ML --- a/src/Pure/PIDE/isabelle_markup.ML Thu Aug 30 22:38:12 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.ML Fri Aug 31 13:23:25 2012 +0200 @@ -89,9 +89,9 @@ val acceptedN: string val accepted: Markup.T val forkedN: string val forked: Markup.T val joinedN: string val joined: Markup.T - val cancelledN: string val cancelled: Markup.T + val runningN: string val running: Markup.T + val finishedN: string val finished: Markup.T val failedN: string val failed: Markup.T - val finishedN: string val finished: Markup.T val serialN: string val legacyN: string val legacy: Markup.T val promptN: string val prompt: Markup.T @@ -274,9 +274,9 @@ val (acceptedN, accepted) = markup_elem "accepted"; val (forkedN, forked) = markup_elem "forked"; val (joinedN, joined) = markup_elem "joined"; -val (cancelledN, cancelled) = markup_elem "cancelled"; +val (runningN, running) = markup_elem "running"; +val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; -val (finishedN, finished) = markup_elem "finished"; (* messages *) diff -r 8e124393c281 -r 4680c4046814 src/Pure/PIDE/isabelle_markup.scala --- a/src/Pure/PIDE/isabelle_markup.scala Thu Aug 30 22:38:12 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.scala Fri Aug 31 13:23:25 2012 +0200 @@ -195,9 +195,9 @@ val ACCEPTED = "accepted" val FORKED = "forked" val JOINED = "joined" - val CANCELLED = "cancelled" + val RUNNING = "running" + val FINISHED = "finished" val FAILED = "failed" - val FINISHED = "finished" /* interactive documents */ diff -r 8e124393c281 -r 4680c4046814 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Aug 30 22:38:12 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Aug 31 13:23:25 2012 +0200 @@ -49,32 +49,34 @@ } sealed case class Status( + private val touched: Boolean = false, private val accepted: Boolean = false, - private val finished: Boolean = false, private val failed: Boolean = false, - forks: Int = 0) + forks: Int = 0, + runs: Int = 0) { - def is_unprocessed: Boolean = accepted && !finished && !failed && forks == 0 - def is_running: Boolean = forks != 0 - def is_finished: Boolean = finished && forks == 0 - def is_failed: Boolean = failed && forks == 0 def + (that: Status): Status = - Status(accepted || that.accepted, finished || that.finished, - failed || that.failed, forks + that.forks) + Status(touched || that.touched, accepted || that.accepted, failed || that.failed, + forks + that.forks, runs + that.runs) + + def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0)) + def is_running: Boolean = runs != 0 + def is_finished: Boolean = !failed && forks == 0 && runs == 0 + def is_failed: Boolean = failed } val command_status_markup: Set[String] = - Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED, - Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED) + Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, + Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED) def command_status(status: Status, markup: Markup): Status = markup match { case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true) - case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true) + case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1) + case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) + case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1) + case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1) case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true) - case Markup(Isabelle_Markup.CANCELLED, _) => status.copy(failed = true) - case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1) - case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1) case _ => status } diff -r 8e124393c281 -r 4680c4046814 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Aug 30 22:38:12 2012 +0200 +++ b/src/Pure/goal.ML Fri Aug 31 13:23:25 2012 +0200 @@ -120,23 +120,9 @@ ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n)); in n end); -fun capture_status e = - let - val task_props = - (case Future.worker_task () of - NONE => I - | SOME task => Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]); - fun status m = Output.status (Markup.markup_only (task_props m)); - - val _ = status Isabelle_Markup.forked; - val result = Exn.capture (Future.interruptible_task e) (); - val _ = - (case result of - Exn.Res _ => status Isabelle_Markup.joined - | Exn.Exn exn => - if Exn.is_interrupt exn then status Isabelle_Markup.cancelled - else status Isabelle_Markup.failed); - in result end; +fun status task markups = + let val props = Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)] + in Output.status (implode (map (Markup.markup_only o props) markups)) end; fun fork_name name e = uninterruptible (fn _ => fn () => @@ -145,7 +131,17 @@ val future = (singleton o Future.forks) {name = name, group = NONE, deps = [], pri = ~1, interrupts = false} - (fn () => Exn.release (capture_status e before forked ~1)); + (fn () => + let + val task = the (Future.worker_task ()); + val _ = status task [Isabelle_Markup.running]; + val result = Exn.capture (Future.interruptible_task e) (); + val _ = + status task + ([Isabelle_Markup.finished, Isabelle_Markup.joined] @ + (if is_some (Exn.get_res result) then [] else [Isabelle_Markup.failed])); + in Exn.release result end); + val _ = status (Future.task_of future) [Isabelle_Markup.forked]; in future end) (); fun fork e = fork_name "Goal.fork" e; diff -r 8e124393c281 -r 4680c4046814 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Aug 30 22:38:12 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 31 13:23:25 2012 +0200 @@ -293,8 +293,8 @@ color <- (result match { case (Some(status), _) => - if (status.is_running) Some(running1_color) - else if (status.is_unprocessed) Some(unprocessed1_color) + if (status.is_unprocessed) Some(unprocessed1_color) + else if (status.is_running) Some(running1_color) else None case (_, opt_color) => opt_color })