--- a/NEWS Thu Jan 03 15:05:48 2013 +0100
+++ b/NEWS Fri Jan 04 01:39:32 2013 +0100
@@ -82,6 +82,8 @@
* Dockable window "Symbols" provides some editing support for Isabelle
symbols.
+* Dockable window "Monitor" shows ML runtime statistics.
+
* Improved editing support for control styles: subscript, superscript,
bold, reset of style -- operating on single symbols or text
selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.
@@ -427,6 +429,8 @@
picked up from some surrounding directory. Potential INCOMPATIBILITY
for home-made settings.
+* Improved ML runtime statistics (heap, threads, future tasks etc.).
+
* Discontinued support for Poly/ML 5.2.1, which was the last version
without exception positions and advanced ML compiler/toplevel
configuration.
--- a/etc/options Thu Jan 03 15:05:48 2013 +0100
+++ b/etc/options Fri Jan 04 01:39:32 2013 +0100
@@ -53,8 +53,6 @@
-- "level of parallel proof checking: 0, 1, 2"
option parallel_proofs_threshold : int = 100
-- "threshold for sub-proof parallelization"
-option ML_statistics : bool = false
- -- "ML runtime statistics of parallel execution environment"
section "Detail of Proof Recording"
@@ -98,3 +96,6 @@
option editor_tracing_messages : int = 100
-- "initial number of tracing messages for each command transaction"
+
+option editor_chart_delay : real = 3.0
+ -- "delay for chart repainting"
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Fri Jan 04 01:39:32 2013 +0100
@@ -1467,7 +1467,7 @@
also
from ass_ok
have "\<dots> \<subseteq> dom (locals (store (assign f v s2)))"
- by (rule dom_locals_assign_mono)
+ by (rule dom_locals_assign_mono [where f = f])
finally show ?thesis by simp
next
case False
--- a/src/HOL/Metis_Examples/Binary_Tree.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Fri Jan 04 01:39:32 2013 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
datatype 'a bt =
Lf
--- a/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy Fri Jan 04 01:39:32 2013 +0100
@@ -10,10 +10,6 @@
imports Complex_Main
begin
-(* FIXME: shouldn't need this *)
-declare [[unify_search_bound = 100]]
-declare [[unify_trace_bound = 100]]
-
text {* Definitional CNF for facts *}
@@ -22,7 +18,7 @@
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-declare [[metis_new_skolemizer = false]]
+declare [[metis_new_skolem = false]]
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
by (metis qax)
@@ -36,7 +32,7 @@
lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
by (metis (full_types) qax)
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
by (metis qax)
@@ -58,7 +54,7 @@
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
-declare [[metis_new_skolemizer = false]]
+declare [[metis_new_skolem = false]]
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
by (metis rax)
@@ -66,7 +62,7 @@
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
by (metis (full_types) rax)
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
by (metis rax)
@@ -92,7 +88,7 @@
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
-declare [[metis_new_skolemizer = false]]
+declare [[metis_new_skolem = false]]
lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
@@ -102,7 +98,7 @@
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metis (full_types) pax)
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
@@ -115,7 +111,7 @@
text {* New Skolemizer *}
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma
fixes x :: real
@@ -139,7 +135,7 @@
lemma
"(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
(\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
-by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
+by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
lemma ex_tl: "EX ys. tl ys = xs"
using tl.simps(2) by fast
--- a/src/HOL/Metis_Examples/Message.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Fri Jan 04 01:39:32 2013 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
by (metis Un_commute Un_left_absorb)
--- a/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Fri Jan 04 01:39:32 2013 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
(S(x,y) | ~S(y,z) | Q(Z,Z)) &
--- a/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Fri Jan 04 01:39:32 2013 +0100
@@ -11,7 +11,7 @@
imports Main "~~/src/HOL/Library/FuncSet"
begin
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
(*Many of these higher-order problems appear to be impossible using the
current linkup. They often seem to need either higher-order unification
--- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Fri Jan 04 01:39:32 2013 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
type_synonym addr = nat
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jan 04 01:39:32 2013 +0100
@@ -12,7 +12,7 @@
imports Main
begin
-declare [[metis_new_skolemizer]]
+declare [[metis_new_skolem]]
sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
preplay_timeout = 0, dont_minimize]
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jan 04 01:39:32 2013 +0100
@@ -1027,7 +1027,7 @@
| add_formula_vars bounds (AConn (_, phis)) =
fold (add_formula_vars bounds) phis
| add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
- in mk_aquant AForall (add_formula_vars [] phi []) phi end
+ in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end
fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
(if is_tptp_variable s andalso
@@ -1039,6 +1039,7 @@
#> fold (add_term_vars bounds) tms
| add_term_vars bounds (AAbs (((name, _), tm), args)) =
add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
+
fun close_formula_universally phi = close_universally add_term_vars phi
fun add_iterm_vars bounds (IApp (tm1, tm2)) =
@@ -1277,7 +1278,7 @@
handle TERM _ => @{const True}
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
- for obscure technical reasons. *)
+ for technical reasons. *)
fun should_use_iff_for_eq CNF _ = false
| should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
| should_use_iff_for_eq _ _ = true
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Jan 04 01:39:32 2013 +0100
@@ -522,23 +522,22 @@
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
-fun map_term_names_in_term f (ATerm ((s, tys), ts)) =
- ATerm ((f s, tys), map (map_term_names_in_term f) ts)
-fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
- AQuant (q, xs, map_term_names_in_formula f phi)
- | map_term_names_in_formula f (AConn (c, phis)) =
- AConn (c, map (map_term_names_in_formula f) phis)
- | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t)
-fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) =
- Definition_Step (name, map_term_names_in_formula f phi1,
- map_term_names_in_formula f phi2)
- | map_term_names_in_step f (Inference_Step (name, role, phi, rule, deps)) =
- Inference_Step (name, role, map_term_names_in_formula f phi, rule, deps)
-fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
+fun map_term_names_in_atp_proof f =
+ let
+ fun do_term (ATerm ((s, tys), ts)) = ATerm ((f s, tys), map do_term ts)
+ fun do_formula (AQuant (q, xs, phi)) =
+ AQuant (q, map (apfst f) xs, do_formula phi)
+ | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
+ | do_formula (AAtom t) = AAtom (do_term t)
+ fun do_step (Definition_Step (name, phi1, phi2)) =
+ Definition_Step (name, do_formula phi1, do_formula phi2)
+ | do_step (Inference_Step (name, role, phi, rule, deps)) =
+ Inference_Step (name, role, do_formula phi, rule, deps)
+ in map do_step end
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
+
fun nasty_atp_proof pool =
- if Symtab.is_empty pool then I
- else map_term_names_in_atp_proof (nasty_name pool)
+ not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool)
end;
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Jan 04 01:39:32 2013 +0100
@@ -131,7 +131,7 @@
fun repair_var_name s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map Char.toLower s
+ val s = s |> String.map Char.toLower
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -158,6 +158,8 @@
fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+val vampire_skolem_prefix = "sK"
+
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred. *)
fun term_from_atp ctxt textual sym_tab =
@@ -246,7 +248,11 @@
end with a digit and "variant_frees" appends letters. *)
fun fresh_up s =
[(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
- val term_ts = map (do_term [] NONE) us
+ val term_ts =
+ map (do_term [] NONE) us
+ (* Vampire (2.6) passes arguments to Skolem functions in reverse
+ order *)
+ |> String.isPrefix vampire_skolem_prefix s ? rev
val ts = term_ts @ extra_ts
val T =
case opt_T of
--- a/src/HOL/Tools/Meson/meson.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Jan 04 01:39:32 2013 +0100
@@ -167,21 +167,36 @@
(rename_bound_vars_RS th rl handle THM _ => tryall rls)
in tryall rls end;
+(* Special version of "rtac" that works around an explosion in the unifier.
+ If the goal has the form "?P c", the danger is that resolving it against a
+ property of the form "... c ... c ... c ..." will lead to a huge unification
+ problem, due to the (spurious) choices between projection and imitation. The
+ workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
+fun quant_rtac th i st =
+ case (concl_of st, prop_of th) of
+ (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
+ let
+ val cc = cterm_of (theory_of_thm th) c
+ val ct = Thm.dest_arg (cprop_of th)
+ in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+ | _ => rtac th i st
+
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
e.g. from conj_forward, should have the form
"[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
fun forward_res ctxt nf st =
- let fun forward_tacf [prem] = rtac (nf prem) 1
- | forward_tacf prems =
- error (cat_lines
- ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
- Display.string_of_thm ctxt st ::
- "Premises:" :: map (Display.string_of_thm ctxt) prems))
+ let
+ fun tacf [prem] = quant_rtac (nf prem) 1
+ | tacf prems =
+ error (cat_lines
+ ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
+ Display.string_of_thm ctxt st ::
+ "Premises:" :: map (Display.string_of_thm ctxt) prems))
in
- case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
- of SOME(th,_) => th
- | NONE => raise THM("forward_res", 0, [st])
+ case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of
+ SOME (th, _) => th
+ | NONE => raise THM ("forward_res", 0, [st])
end;
(*Are any of the logical connectives in "bs" present in the term?*)
@@ -635,7 +650,6 @@
val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
-(* "RS" can fail if "unify_search_bound" is too small. *)
fun try_skolemize_etc ctxt th =
let
val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Jan 04 01:39:32 2013 +0100
@@ -300,20 +300,20 @@
|> Skip_Proof.make_thm @{theory}
(* Converts an Isabelle theorem into NNF. *)
-fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt =
+fun nnf_axiom choice_ths new_skolem ax_no th ctxt =
let
val thy = Proof_Context.theory_of ctxt
val th =
th |> transform_elim_theorem
|> zero_var_indexes
- |> new_skolemizer ? forall_intr_vars
+ |> new_skolem ? forall_intr_vars
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
val th = th |> Conv.fconv_rule Object_Logic.atomize
|> cong_extensionalize_thm thy
|> abs_extensionalize_thm ctxt
|> make_nnf ctxt
in
- if new_skolemizer then
+ if new_skolem then
let
fun skolemize choice_ths =
skolemize_with_choice_theorems ctxt choice_ths
@@ -364,14 +364,14 @@
end
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th =
+fun cnf_axiom ctxt0 new_skolem combinators ax_no th =
let
val thy = Proof_Context.theory_of ctxt0
val choice_ths = choice_theorems thy
val (opt, (nnf_th, ctxt)) =
- nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
+ nnf_axiom choice_ths new_skolem ax_no th ctxt0
fun clausify th =
- make_cnf (if new_skolemizer orelse null choice_ths then []
+ make_cnf (if new_skolem orelse null choice_ths then []
else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
th ctxt ctxt
val (cnf_ths, ctxt) = clausify nnf_th
--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Jan 04 01:39:32 2013 +0100
@@ -11,7 +11,7 @@
sig
val trace : bool Config.T
val verbose : bool Config.T
- val new_skolemizer : bool Config.T
+ val new_skolem : bool Config.T
val advisory_simp : bool Config.T
val type_has_top_sort : typ -> bool
val metis_tac :
@@ -29,8 +29,8 @@
open Metis_Generate
open Metis_Reconstruct
-val new_skolemizer =
- Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
+val new_skolem =
+ Attrib.setup_config_bool @{binding metis_new_skolem} (K false)
val advisory_simp =
Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
@@ -137,8 +137,8 @@
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
- val new_skolemizer =
- Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
+ val new_skolem =
+ Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
val do_lams =
(lam_trans = liftingN orelse lam_trans = lam_liftingN)
? introduce_lam_wrappers ctxt
@@ -146,7 +146,7 @@
map2 (fn j => fn th =>
(Thm.get_name_hint th,
th |> Drule.eta_contraction_rule
- |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
+ |> Meson_Clausify.cnf_axiom ctxt new_skolem
(lam_trans = combsN) j
||> map do_lams))
(0 upto length ths0 - 1) ths0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jan 04 01:39:32 2013 +0100
@@ -482,8 +482,8 @@
#> simplify_spaces
#> maybe_quote
val reconstr = Metis (type_enc, lam_trans)
- fun do_metis ind (ls, ss) =
- "\n" ^ do_indent (ind + 1) ^
+ fun do_metis ind options (ls, ss) =
+ "\n" ^ do_indent (ind + 1) ^ options ^
reconstructor_command reconstr 1 1 [] 0
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
@@ -495,15 +495,19 @@
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
| do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) =
do_indent ind ^ do_obtain qs xs ^ " " ^
- do_label l ^ do_term t ^ do_metis ind facts ^ "\n"
+ do_label l ^ do_term t ^
+ (* The new skolemizer puts the arguments in the same order as the ATPs
+ (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
+ Vampire). *)
+ do_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
| do_step ind (Prove (qs, l, t, By_Metis facts)) =
do_indent ind ^ do_have qs ^ " " ^
- do_label l ^ do_term t ^ do_metis ind facts ^ "\n"
+ do_label l ^ do_term t ^ do_metis ind "" facts ^ "\n"
| do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
proofs) ^
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
- do_metis ind facts ^ "\n"
+ do_metis ind "" facts ^ "\n"
and do_steps prefix suffix ind steps =
let val s = implode (map (do_step ind) steps) in
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
--- a/src/Pure/ML/ml_statistics.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala Fri Jan 04 01:39:32 2013 +0100
@@ -24,6 +24,8 @@
def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
def apply(log: Path): ML_Statistics = apply(read_log(log))
+ val empty = apply(Nil)
+
/* standard fields */
@@ -84,11 +86,12 @@
final class ML_Statistics private(val stats: List[Properties.T])
{
val Now = new Properties.Double("now")
-
- require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined))
+ def now(props: Properties.T): Double = Now.unapply(props).get
- val time_start = Now.unapply(stats.head).get
- val duration = Now.unapply(stats.last).get - time_start
+ require(stats.forall(props => Now.unapply(props).isDefined))
+
+ val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
+ val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
val fields: Set[String] =
SortedSet.empty[String] ++
@@ -97,7 +100,7 @@
val content: List[ML_Statistics.Entry] =
stats.map(props => {
- val time = Now.unapply(props).get - time_start
+ val time = now(props) - time_start
require(time >= 0.0)
val data =
SortedMap.empty[String, Double] ++
@@ -109,10 +112,9 @@
/* charts */
- def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
+ def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
{
- val data = new XYSeriesCollection
-
+ data.removeAllSeries
for {
field <- selected_fields.iterator
series = new XYSeries(field)
@@ -120,20 +122,23 @@
content.foreach(entry => series.add(entry.time, entry.data(field)))
data.addSeries(series)
}
+ }
+
+ def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
+ {
+ val data = new XYSeriesCollection
+ update_data(data, selected_fields)
ChartFactory.createXYLineChart(title, "time", "value", data,
PlotOrientation.VERTICAL, true, true, true)
}
- def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel =
- new ChartPanel(chart(title, selected_fields))
+ def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
def standard_frames: Unit =
- for ((title, selected_fields) <- ML_Statistics.standard_fields) {
- val c = chart(title, selected_fields)
+ ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
Swing_Thread.later {
new Frame { contents = Component.wrap(new ChartPanel(c)); visible = true }
- }
- }
+ })
}
--- a/src/Pure/System/isabelle_process.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML Fri Jan 04 01:39:32 2013 +0100
@@ -238,7 +238,7 @@
protocol_command "Isabelle_Process.options"
(fn [options_yxml] =>
let val options = Options.decode (YXML.parse_body options_yxml) in
- Future.ML_statistics := Options.bool options "ML_statistics";
+ Future.ML_statistics := true;
Multithreading.trace := Options.int options "threads_trace";
Multithreading.max_threads := Options.int options "threads";
if Multithreading.max_threads_value () < 2
--- a/src/Pure/System/session.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/System/session.ML Fri Jan 04 01:39:32 2013 +0100
@@ -8,6 +8,7 @@
sig
val id: unit -> string list
val name: unit -> string
+ val path: unit -> string list
val welcome: unit -> string
val finish: unit -> unit
val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
--- a/src/Pure/System/session.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/System/session.scala Fri Jan 04 01:39:32 2013 +0100
@@ -22,7 +22,7 @@
/* events */
//{{{
- case class Statistics(stats: Properties.T)
+ case class Statistics(props: Properties.T)
case class Global_Options(options: Options)
case object Caret_Focus
case class Raw_Edits(edits: List[Document.Edit_Text])
@@ -361,8 +361,8 @@
case None =>
}
- case Markup.ML_Statistics(stats) if output.is_protocol =>
- statistics.event(Session.Statistics(stats))
+ case Markup.ML_Statistics(props) if output.is_protocol =>
+ statistics.event(Session.Statistics(props))
case _ if output.is_init =>
phase = Session.Ready
--- a/src/Pure/Thy/html.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/Thy/html.scala Fri Jan 04 01:39:32 2013 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/html.scala
Author: Makarius
-Basic HTML output.
+HTML presentation elements.
*/
package isabelle
@@ -29,75 +29,19 @@
}
- /// FIXME unused stuff
-
- // common elements and attributes
-
- val BODY = "body"
- val DIV = "div"
- val SPAN = "span"
- val BR = "br"
- val PRE = "pre"
- val CLASS = "class"
- val STYLE = "style"
-
+ // common markup elements
- // document markup
-
- def span(cls: String, body: XML.Body): XML.Elem =
- XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
-
- def user_font(font: String, txt: String): XML.Elem =
- XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
-
- def hidden(txt: String): XML.Elem =
- span(Markup.HIDDEN, List(XML.Text(txt)))
-
- def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
- def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
- def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
+ def session_entry(name: String): String =
+ XML.string_of_tree(
+ XML.elem("li",
+ List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
+ List(XML.Text(name)))))) + "\n"
- def spans(input: XML.Tree): XML.Body =
- {
- def html_spans(tree: XML.Tree): XML.Body =
- tree match {
- case XML.Wrapped_Elem(markup, _, ts) =>
- List(span(markup.name, ts.flatMap(html_spans)))
- case XML.Elem(markup, ts) =>
- List(span(markup.name, ts.flatMap(html_spans)))
- case XML.Text(txt) =>
- val ts = new ListBuffer[XML.Tree]
- val t = new StringBuilder
- def flush() {
- if (!t.isEmpty) {
- ts += XML.Text(t.toString)
- t.clear
- }
- }
- def add(elem: XML.Tree) {
- flush()
- ts += elem
- }
- val syms = Symbol.iterator(txt)
- while (syms.hasNext) {
- val s1 = syms.next
- def s2() = if (syms.hasNext) syms.next else ""
- if (s1 == "\n") add(XML.elem(BR))
- else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
- { add(hidden(s1)); add(sub(s2())) }
- else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
- { add(hidden(s1)); add(sup(s2())) }
- else if (s1 == Symbol.bsub_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.esub_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.bsup_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.esup_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
- else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
- else t ++= s1
- }
- flush()
- ts.toList
- }
- html_spans(input)
- }
+ def session_entries(names: List[String]): String =
+ if (names.isEmpty) "</ul>"
+ else
+ "</ul>\n</div>\n<div class=\"sessions\">\n" +
+ "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
+
+ val end_document = "\n</div>\n</body>\n</html>\n"
}
--- a/src/Pure/Thy/present.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/Thy/present.ML Fri Jan 04 01:39:32 2013 +0100
@@ -213,7 +213,7 @@
(** document preparation **)
-(* maintain index *)
+(* maintain session index *)
val session_entries =
HTML.session_entries o
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/present.scala Fri Jan 04 01:39:32 2013 +0100
@@ -0,0 +1,41 @@
+/* Title: Pure/Thy/present.scala
+ Author: Makarius
+
+Theory presentation: HTML.
+*/
+
+package isabelle
+
+
+object Present
+{
+ /* maintain session index -- NOT thread-safe */
+
+ private val index_path = Path.basic("index.html")
+ private val session_entries_path = Path.explode(".session/entries")
+ private val pre_index_path = Path.explode(".session/pre-index")
+
+ private def get_entries(dir: Path): List[String] =
+ split_lines(File.read(dir + session_entries_path))
+
+ private def put_entries(entries: List[String], dir: Path): Unit =
+ File.write(dir + session_entries_path, cat_lines(entries))
+
+ def create_index(dir: Path): Unit =
+ File.write(dir + index_path,
+ File.read(dir + pre_index_path) +
+ HTML.session_entries(get_entries(dir)) +
+ HTML.end_document)
+
+ def update_index(dir: Path, names: List[String]): Unit =
+ try {
+ put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir)
+ create_index(dir)
+ }
+ catch {
+ case ERROR(msg) =>
+ java.lang.System.err.println(
+ "### " + msg + "\n### Browser info: failed to update session index of " + dir)
+ }
+}
+
--- a/src/Pure/Tools/build.ML Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/Tools/build.ML Fri Jan 04 01:39:32 2013 +0100
@@ -43,7 +43,7 @@
(Options.int options "parallel_proofs_threshold")
|> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
- |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
+ |> Unsynchronized.setmp Future.ML_statistics true
|> no_document options ? Present.no_document
|> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
|> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
@@ -89,6 +89,10 @@
| dups => error ("Duplicate document variants: " ^ commas_quote dups));
val _ =
+ (case Session.path () of
+ [] => ()
+ | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
+ val _ =
Session.init do_output false
(Options.bool options "browser_info") browser_info
(Options.string options "document")
--- a/src/Pure/Tools/build.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/Tools/build.scala Fri Jan 04 01:39:32 2013 +0100
@@ -412,7 +412,7 @@
/* jobs */
- private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
+ private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
verbose: Boolean, browser_info: Path)
{
// global browser info dir
@@ -515,6 +515,8 @@
private def log(name: String): Path = LOG + Path.basic(name)
private def log_gz(name: String): Path = log(name).ext("gz")
+ private val SESSION_PARENT_PATH = "\fSession.parent_path = "
+
private def sources_stamp(digests: List[SHA1.Digest]): String =
digests.map(_.toString).sorted.mkString("sources: ", " ", "")
@@ -600,7 +602,7 @@
}
// scheduler loop
- case class Result(current: Boolean, heap: String, rc: Int)
+ case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
def sleep(): Unit = Thread.sleep(500)
@@ -620,9 +622,10 @@
//{{{ finish job
val (out, err, rc) = job.join
+ val out_lines = split_lines(out)
progress.echo(Library.trim_line(err))
- val heap =
+ val (parent_path, heap) =
if (rc == 0) {
(output_dir + log(name)).file.delete
@@ -631,7 +634,13 @@
File.write_gzip(output_dir + log_gz(name),
sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
- heap
+ val parent_path =
+ if (job.info.options.bool("browser_info"))
+ out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
+ line.substring(SESSION_PARENT_PATH.length))
+ else None
+
+ (parent_path, heap)
}
else {
(output_dir + Path.basic(name)).file.delete
@@ -641,14 +650,14 @@
progress.echo(name + " FAILED")
if (rc != 130) {
progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
- val lines = split_lines(out)
- val tail = lines.drop(lines.length - 20 max 0)
+ val tail = out_lines.drop(out_lines.length - 20 max 0)
progress.echo("\n" + cat_lines(tail))
}
- no_heap
+ (None, no_heap)
}
- loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
+ loop(pending - name, running - name,
+ results + (name -> Result(false, parent_path, heap, rc)))
//}}}
case None if (running.size < (max_jobs max 1)) =>
//{{{ check/start next job
@@ -656,7 +665,7 @@
case Some((name, info)) =>
val parent_result =
info.parent match {
- case None => Result(true, no_heap, 0)
+ case None => Result(true, None, no_heap, 0)
case Some(parent) => results(parent)
}
val output = output_dir + Path.basic(name)
@@ -679,10 +688,10 @@
val all_current = current && parent_result.current
if (all_current)
- loop(pending - name, running, results + (name -> Result(true, heap, 0)))
+ loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
else if (no_build) {
if (verbose) progress.echo("Skipping " + name + " ...")
- loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+ loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
}
else if (parent_result.rc == 0) {
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
@@ -691,7 +700,7 @@
}
else {
progress.echo(name + " CANCELLED")
- loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+ loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
}
case None => sleep(); loop(pending, running, results)
}
@@ -703,10 +712,17 @@
val results =
if (deps.is_empty) {
progress.echo("### Nothing to build")
- Map.empty
+ Map.empty[String, Result]
}
else loop(queue, Map.empty, Map.empty)
+ val session_entries =
+ (for ((name, res) <- results.iterator if res.parent_path.isDefined)
+ yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
+ { case (p, es) => (p, es.map(_._2).sorted) })
+ for ((p, names) <- session_entries)
+ Present.update_index(browser_info + Path.explode(p), names)
+
val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
if (rc != 0 && (verbose || !no_build)) {
val unfinished =
--- a/src/Pure/build-jars Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Pure/build-jars Fri Jan 04 01:39:32 2013 +0100
@@ -57,6 +57,7 @@
System/utf8.scala
Thy/completion.scala
Thy/html.scala
+ Thy/present.scala
Thy/thy_header.scala
Thy/thy_info.scala
Thy/thy_load.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Jan 04 01:39:32 2013 +0100
@@ -43,9 +43,9 @@
private val relevant_options =
Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
"jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
- "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
+ "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
"editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
- "editor_tracing_messages", "editor_update_delay")
+ "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
relevant_options.foreach(PIDE.options.value.check_name _)
--- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Fri Jan 04 01:39:32 2013 +0100
@@ -12,59 +12,38 @@
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane, Component}
-import org.jfree.chart.{ChartFactory, ChartPanel}
-import org.jfree.data.time.{Millisecond, TimeSeries, TimeSeriesCollection}
+import org.jfree.chart.ChartPanel
+import org.jfree.data.xy.XYSeriesCollection
import org.gjt.sp.jedit.View
class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
{
- /* properties */ // FIXME avoid hardwired stuff
-
- private val Now = new Properties.Double("now")
- private val Size_Heap = new Properties.Double("size_heap")
+ /* chart data -- owned by Swing thread */
- private val series = new TimeSeries("ML heap size", classOf[Millisecond])
-
-
- /* chart */
+ private val chart = ML_Statistics.empty.chart(null, Nil)
+ private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
+ private var rev_stats: List[Properties.T] = Nil
- private val chart_panel =
- {
- val data = new TimeSeriesCollection(series)
- val chart = ChartFactory.createTimeSeriesChart(null, "Time", "Value", data, true, true, false)
- val plot = chart.getXYPlot()
+ private val delay_update =
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
+ ML_Statistics(rev_stats.reverse)
+ .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
+ }
- val x_axis = plot.getDomainAxis()
- x_axis.setAutoRange(true)
- x_axis.setFixedAutoRange(60000.0)
-
- val y_axis = plot.getRangeAxis()
- y_axis.setAutoRange(true)
-
- new ChartPanel(chart)
- }
- set_content(chart_panel)
+ set_content(new ChartPanel(chart))
/* main actor */
private val main_actor = actor {
- var t0: Option[Double] = None
loop {
react {
- case Session.Statistics(stats) =>
- java.lang.System.err.println(stats)
- stats match {
- case Now(t1) =>
- if (t0.isEmpty) t0 = Some(t1)
- val t = t1 - t0.get
- stats match {
- case Size_Heap(x) => series.add(new Millisecond(), x) // FIXME proper time point
- case _ =>
- }
- case _ =>
+ case Session.Statistics(props) =>
+ Swing_Thread.later {
+ rev_stats ::= props
+ delay_update.invoke()
}
case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/plugin.scala Thu Jan 03 15:05:48 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Jan 04 01:39:32 2013 +0100
@@ -13,7 +13,7 @@
import scala.swing.{ListView, ScrollPane}
-import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View}
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.ModeProvider
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
@@ -271,6 +271,8 @@
override def start()
{
try {
+ Debug.DISABLE_SEARCH_DIALOG_POOL = true
+
PIDE.plugin = this
Isabelle_System.init()
Isabelle_System.install_fonts()