# HG changeset patch # User wenzelm # Date 1346445277 -7200 # Node ID fa094e173cb95381230483a50a46ad23018447b7 # Parent 1a7b9e4c3153b527fe3181c7f4f95326ec7a4c71# Parent be6d4e8307c802f9fe59e5b613787e2d8fd972ba merged diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/Isar/local_theory.ML Fri Aug 31 22:34:37 2012 +0200 @@ -30,6 +30,8 @@ val raw_theory: (theory -> theory) -> local_theory -> local_theory val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val background_theory: (theory -> theory) -> local_theory -> local_theory + val begin_proofs: local_theory -> local_theory + val register_proofs: thm list -> local_theory -> local_theory val target_of: local_theory -> Proof.context val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val target_morphism: local_theory -> morphism @@ -190,6 +192,12 @@ fun background_theory f = #2 o background_theory_result (f #> pair ()); +(* forked proofs *) + +val begin_proofs = background_theory (Context.theory_map Thm.begin_proofs); +val register_proofs = background_theory o Thm.register_proofs_thy; + + (* target contexts *) val target_of = #target o get_last_lthy; diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/Isar/proof.ML Fri Aug 31 22:34:37 2012 +0200 @@ -78,15 +78,15 @@ val begin_block: state -> state val next_block: state -> state val end_block: state -> state - val begin_notepad: Proof.context -> state - val end_notepad: state -> Proof.context + val begin_notepad: context -> state + val end_notepad: state -> context val proof: Method.text option -> state -> state Seq.seq val defer: int option -> state -> state Seq.seq val prefer: int -> state -> state Seq.seq val apply: Method.text -> state -> state Seq.seq val apply_end: Method.text -> state -> state Seq.seq val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) -> - (Proof.context -> 'a -> attribute) -> + (context -> 'a -> attribute) -> ('b list -> context -> (term list list * (context -> context)) * context) -> string -> Method.text option -> (thm list list -> state -> state) -> ((binding * 'a list) * 'b) list -> state -> state @@ -116,7 +116,7 @@ (Attrib.binding * (string * string list) list) list -> bool -> state -> state val schematic_goal: state -> bool val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state - val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context + val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context end; @@ -939,7 +939,6 @@ |> burrow (Proof_Context.export goal_ctxt outer_ctxt); in outer_state - |> register_proofs (flat results) |> map_context (after_ctxt props) |> pair (after_qed, results) end; @@ -967,7 +966,7 @@ fun local_qeds txt = end_proof false txt #> Seq.map (generic_qed Proof_Context.auto_bind_facts #-> - (fn ((after_qed, _), results) => after_qed results)); + (fn ((after_qed, _), results) => register_proofs (flat results) #> after_qed results)); fun local_qed txt = local_qeds txt #> check_finish; diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/Isar/specification.ML Fri Aug 31 22:34:37 2012 +0200 @@ -395,7 +395,8 @@ let val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results; val (res, lthy') = - if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy) + if forall (Attrib.is_empty_binding o fst) stmt + then (map (pair "") results', Local_Theory.register_proofs (flat results) lthy) else Local_Theory.notes_kind kind (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Fri Aug 31 22:34:37 2012 +0200 @@ -425,8 +425,9 @@ (* forked proofs *) -val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint; -val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy); +val begin_proofs = + Context.mapping (Context.theory_map Thm.begin_proofs #> Theory.checkpoint) + Local_Theory.begin_proofs; fun join_recent_proofs st = (case try proof_of st of diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/PIDE/command.ML Fri Aug 31 22:34:37 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 1a7b9e4c3153 -r fa094e173cb9 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/PIDE/command.scala Fri Aug 31 22:34:37 2012 +0200 @@ -48,6 +48,11 @@ val props = Position.purge(atts) val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) state.add_markup(info) + case XML.Elem(Markup(name, atts), args) => + val range = command.proper_range + val props = Position.purge(atts) + val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) + state.add_markup(info) case _ => // FIXME System.err.println("Ignored report message: " + msg) state diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/PIDE/isabelle_markup.ML --- a/src/Pure/PIDE/isabelle_markup.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.ML Fri Aug 31 22:34:37 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 1a7b9e4c3153 -r fa094e173cb9 src/Pure/PIDE/isabelle_markup.scala --- a/src/Pure/PIDE/isabelle_markup.scala Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.scala Fri Aug 31 22:34:37 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 1a7b9e4c3153 -r fa094e173cb9 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Aug 31 22:34:37 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 && touched && 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 1a7b9e4c3153 -r fa094e173cb9 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/ROOT.ML Fri Aug 31 22:34:37 2012 +0200 @@ -158,11 +158,19 @@ use "conjunction.ML"; use "assumption.ML"; use "display.ML"; -use "goal.ML"; (* Isar -- Intelligible Semi-Automated Reasoning *) +(*ML support*) +use "ML/ml_syntax.ML"; +use "ML/ml_env.ML"; +use "Isar/runtime.ML"; +use "ML/ml_compiler.ML"; +if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else (); + +use "goal.ML"; + (*proof context*) use "Isar/object_logic.ML"; use "Isar/rule_cases.ML"; @@ -185,13 +193,6 @@ use "Isar/keyword.ML"; use "Isar/parse.ML"; use "Isar/args.ML"; - -(*ML support*) -use "ML/ml_syntax.ML"; -use "ML/ml_env.ML"; -use "Isar/runtime.ML"; -use "ML/ml_compiler.ML"; -if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else (); use "ML/ml_context.ML"; (*theory sources*) diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/global_theory.ML Fri Aug 31 22:34:37 2012 +0200 @@ -124,7 +124,7 @@ (* enter_thms *) -fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy); +fun register_proofs thms thy = (thms, Thm.register_proofs_thy thms thy); fun enter_thms pre_name post_name app_att (b, thms) thy = if Binding.is_empty b diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/goal.ML Fri Aug 31 22:34:37 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,21 @@ 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]; + val _ = + (case result of + Exn.Res _ => () + | Exn.Exn exn => + (status task [Isabelle_Markup.failed]; + Output.report (Markup.markup_only Isabelle_Markup.bad); + Output.error_msg (ML_Compiler.exn_message exn))); + 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 1a7b9e4c3153 -r fa094e173cb9 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Pure/more_thm.ML Fri Aug 31 22:34:37 2012 +0200 @@ -96,6 +96,7 @@ val kind_rule: string -> thm -> thm val kind: string -> attribute val register_proofs: thm list -> Context.generic -> Context.generic + val register_proofs_thy: thm list -> theory -> theory val begin_proofs: Context.generic -> Context.generic val join_local_proofs: Proof.context -> unit val join_recent_proofs: theory -> unit @@ -493,6 +494,7 @@ val begin_proofs = Proofs.map (apfst (K empty_proofs)); val register_proofs = Proofs.map o pairself o add_proofs; +val register_proofs_thy = Context.theory_map o register_proofs; val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof; val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory; diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 31 22:34:37 2012 +0200 @@ -166,8 +166,8 @@ markup == Isabelle_Markup.WARNING || markup == Isabelle_Markup.ERROR => msgs + (serial -> tooltip_text(msg)) - case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) => - msgs + (Document.new_id() -> tooltip_text(msg)) + case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body))) + if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg)) }).toList.flatMap(_.info) if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2))) } @@ -292,10 +292,10 @@ }) color <- (result match { - case (Some(status), _) => - if (status.is_running) Some(running1_color) - else if (status.is_unprocessed) Some(unprocessed1_color) - else None + case (Some(status), opt_color) => + if (status.is_unprocessed) Some(unprocessed1_color) + else if (status.is_running) Some(running1_color) + else opt_color case (_, opt_color) => opt_color }) } yield Text.Info(r, color) diff -r 1a7b9e4c3153 -r fa094e173cb9 src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Fri Aug 31 16:07:06 2012 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Fri Aug 31 22:34:37 2012 +0200 @@ -10,7 +10,7 @@ import isabelle._ import scala.actors.Actor._ -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, Component} +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component} import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged} import java.lang.System @@ -36,7 +36,7 @@ status.peer.setLayoutOrientation(JList.VERTICAL_WRAP) status.selection.intervalMode = ListView.IntervalMode.Single - set_content(status) + set_content(new ScrollPane(status)) /* controls */