--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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 *)
--- 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 */
--- 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
}
--- 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*)
--- 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
--- 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;
--- 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;
--- 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)
--- 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 */