# HG changeset patch # User wenzelm # Date 1364664273 -3600 # Node ID c3a7d6592e3f209f7dfb964f46593771046b3bfe # Parent 7c59fe17f49511ed0b1cdc575b587df467bfd31b# Parent e4aeb102ad70d39237ab31a33780ae43796aec27 merged diff -r 7c59fe17f495 -r c3a7d6592e3f src/Pure/General/time.scala --- 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" diff -r 7c59fe17f495 -r c3a7d6592e3f src/Pure/General/timing.scala --- 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" diff -r 7c59fe17f495 -r c3a7d6592e3f src/Pure/PIDE/command.ML --- 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) diff -r 7c59fe17f495 -r c3a7d6592e3f src/Pure/raw_simplifier.ML --- 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. diff -r 7c59fe17f495 -r c3a7d6592e3f src/Pure/simplifier.ML --- 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 diff -r 7c59fe17f495 -r c3a7d6592e3f src/Tools/jEdit/src/rendering.scala --- 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)