--- a/src/Pure/General/time.scala Fri Mar 29 18:57:47 2013 +0100
+++ b/src/Pure/General/time.scala Sat Mar 30 18:24:33 2013 +0100
@@ -15,6 +15,7 @@
{
def seconds(s: Double): Time = new Time((s * 1000.0).round)
def ms(m: Long): Time = new Time(m)
+ val zero: Time = ms(0)
def print_seconds(s: Double): String =
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
@@ -22,6 +23,8 @@
final class Time private(val ms: Long)
{
+ def + (t: Time): Time = new Time(ms + t.ms)
+
def seconds: Double = ms / 1000.0
def min(t: Time): Time = if (ms < t.ms) this else t
@@ -29,6 +32,13 @@
def is_relevant: Boolean = ms >= 1
+ override def hashCode: Int = ms.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Time => ms == other.ms
+ case _ => false
+ }
+
override def toString = Time.print_seconds(seconds)
def message: String = toString + "s"
--- a/src/Pure/General/timing.scala Fri Mar 29 18:57:47 2013 +0100
+++ b/src/Pure/General/timing.scala Sat Mar 30 18:24:33 2013 +0100
@@ -10,6 +10,8 @@
object Timing
{
+ val zero = Timing(Time.zero, Time.zero, Time.zero)
+
def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
if (enabled) {
val start = java.lang.System.currentTimeMillis()
@@ -27,10 +29,12 @@
else e
}
-class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
+sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
{
def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
+ def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
+
def message: String =
elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
--- a/src/Pure/PIDE/command.ML Fri Mar 29 18:57:47 2013 +0100
+++ b/src/Pure/PIDE/command.ML Sat Mar 30 18:24:33 2013 +0100
@@ -61,11 +61,19 @@
local
+fun timing tr t =
+ if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
+
fun run int tr st =
if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
Toplevel.setmp_thread_position tr (fn () =>
(Goal.fork_name "Toplevel.diag" ~1
- (fn () => Toplevel.command_exception int tr st); ([], SOME st))) ()
+ (fn () =>
+ let
+ val start = Timing.start ();
+ val res = Exn.interruptible_capture (fn () => Toplevel.command_exception int tr st) ();
+ val _ = timing tr (Timing.result start);
+ in Exn.release res end); ([], SOME st))) ()
else Toplevel.command_errors int tr st;
fun check_cmts tr cmts st =
@@ -75,9 +83,6 @@
(Thy_Output.check_text (Token.source_position_of cmt) st; [])
handle exn => ML_Compiler.exn_messages_ids exn)) ();
-fun timing tr t =
- if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
-
fun proof_status tr st =
(case try Toplevel.proof_of st of
SOME prf => Toplevel.status tr (Proof.status_markup prf)
--- a/src/Pure/raw_simplifier.ML Fri Mar 29 18:57:47 2013 +0100
+++ b/src/Pure/raw_simplifier.ML Sat Mar 30 18:24:33 2013 +0100
@@ -15,6 +15,7 @@
val simp_trace_depth_limit: int Config.T
val simp_debug: bool Config.T
val simp_trace: bool Config.T
+ type cong_name = bool * string
type rrule
val eq_rrule: rrule * rrule -> bool
type simpset
@@ -26,8 +27,8 @@
val dest_ss: simpset ->
{simps: (string * thm) list,
procs: (string * cterm list) list,
- congs: (string * thm) list,
- weak_congs: string list,
+ congs: (cong_name * thm) list,
+ weak_congs: cong_name list,
loopers: string list,
unsafe_solvers: string list,
safe_solvers: string list}
@@ -72,7 +73,7 @@
bounds: int * ((string * typ) * string) list,
depth: int * bool Unsynchronized.ref,
context: Proof.context option} *
- {congs: (string * thm) list * string list,
+ {congs: (cong_name * thm) list * cong_name list,
procs: proc Net.net,
mk_rews:
{mk: simpset -> thm -> thm list,
@@ -135,6 +136,15 @@
(** datatype simpset **)
+(* congruence rules *)
+
+type cong_name = bool * string;
+
+fun cong_name (Const (a, _)) = SOME (true, a)
+ | cong_name (Free (a, _)) = SOME (false, a)
+ | cong_name _ = NONE;
+
+
(* rewrite rules *)
type rrule =
@@ -188,7 +198,7 @@
bounds: int * ((string * typ) * string) list,
depth: int * bool Unsynchronized.ref,
context: Proof.context option} *
- {congs: (string * thm) list * string list,
+ {congs: (cong_name * thm) list * cong_name list,
procs: proc Net.net,
mk_rews:
{mk: simpset -> thm -> thm list,
@@ -268,7 +278,8 @@
val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
(rules, prems, bounds,
(depth + 1,
- if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
+ if depth = simp_trace_depth_limit_of context
+ then Unsynchronized.ref false else exceeded), context));
fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
@@ -538,10 +549,6 @@
(* congs *)
-fun cong_name (Const (a, _)) = SOME a
- | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
- | cong_name _ = NONE;
-
local
fun is_full_cong_prems [] [] = true
@@ -582,7 +589,7 @@
val (xs, weak) = congs;
val _ =
if AList.defined (op =) xs a
- then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
+ then if_visible ss warning ("Overwriting congruence rule for " ^ quote (#2 a))
else ();
val xs' = AList.update (op =) (a, thm) xs;
val weak' = if is_full_cong thm then weak else a :: weak;
@@ -597,7 +604,7 @@
val a = the (cong_name (head_of lhs)) handle Option.Option =>
raise SIMPLIFIER ("Congruence must start with a constant", thm);
val (xs, _) = congs;
- val xs' = filter_out (fn (x : string, _) => x = a) xs;
+ val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
val weak' = xs' |> map_filter (fn (a, thm) =>
if is_full_cong thm then NONE else SOME a);
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
@@ -876,7 +883,10 @@
fun uncond_skel ((_, weak), (lhs, rhs)) =
if null weak then rhs (*optimization*)
- else if exists_Const (member (op =) weak o #1) lhs then skel0
+ else if exists_subterm
+ (fn Const (a, _) => member (op =) weak (true, a)
+ | Free (a, _) => member (op =) weak (false, a)
+ | _ => false) lhs then skel0
else rhs;
(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
--- a/src/Pure/simplifier.ML Fri Mar 29 18:57:47 2013 +0100
+++ b/src/Pure/simplifier.ML Sat Mar 30 18:24:33 2013 +0100
@@ -119,14 +119,17 @@
fun pretty_ss ctxt ss =
let
- val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
+ val pretty_term = Syntax.pretty_term ctxt;
val pretty_thm = Display.pretty_thm ctxt;
val pretty_thm_item = Display.pretty_thm_item ctxt;
fun pretty_proc (name, lhss) =
- Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
+ Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_term o Thm.term_of) lhss);
+
+ fun pretty_cong_name (const, name) =
+ pretty_term ((if const then Const else Free) (name, dummyT));
fun pretty_cong (name, thm) =
- Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
+ Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
in
--- a/src/Tools/jEdit/src/rendering.scala Fri Mar 29 18:57:47 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 30 18:24:33 2013 +0100
@@ -320,27 +320,39 @@
Markup.DOCUMENT_SOURCE -> "document source")
private val tooltip_elements =
- Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
- tooltips.keys
+ Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
+ Markup.ML_TYPING, Markup.PATH) ++ tooltips.keys
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
+ private val timing_threshold: Double = options.real("jedit_timing_threshold")
+
def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
{
- def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r0: Text.Range, p: (Boolean, XML.Tree)) =
+ def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])],
+ r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] =
{
val r = snapshot.convert(r0)
- if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
+ val (t, info) = prev.info
+ if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
}
val results =
- snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
- range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
+ snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
+ range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
{
+ case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
+ Text.Info(r, (t1 + t2, info))
case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
val kind1 = space_explode('_', kind).mkString(" ")
- add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
+ val txt1 = kind1 + " " + quote(name)
+ val t = prev.info._1
+ val txt2 =
+ if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
+ "\n" + t.message
+ else ""
+ add(prev, r, (true, XML.Text(txt1 + txt2)))
case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
@@ -351,10 +363,11 @@
case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
add(prev, r, (false, pretty_typing("ML:", body)))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
- if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
+ if tooltips.isDefinedAt(name) =>
+ add(prev, r, (true, XML.Text(tooltips(name))))
}).toList.map(_.info)
- results.flatMap(_.info) match {
+ results.map(_.info).flatMap(_._2) match {
case Nil => None
case tips =>
val r = Text.Range(results.head.range.start, results.last.range.stop)