interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
--- a/CONTRIBUTORS Tue Feb 04 01:35:48 2014 +0100
+++ b/CONTRIBUTORS Tue Feb 04 09:04:59 2014 +0000
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* January 2014: Lars Hupel, TUM
+ An improved, interactive simplifier trace with integration into the
+ Isabelle/jEdit Prover IDE.
Contributions to Isabelle2013-1
-------------------------------
--- a/NEWS Tue Feb 04 01:35:48 2014 +0100
+++ b/NEWS Tue Feb 04 09:04:59 2014 +0000
@@ -37,6 +37,10 @@
process, without requiring old-fashioned command-line invocation of
"isabelle jedit -m MODE".
+* New panel: Simplifier trace. Provides an interactive view of the
+simplification process, enabled by the newly-introduced
+"simplifier_trace" declaration.
+
*** Pure ***
--- a/src/Pure/PIDE/markup.scala Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Feb 04 09:04:59 2014 +0000
@@ -273,7 +273,8 @@
/* messages */
- val Serial = new Properties.Long("serial")
+ val SERIAL = "serial"
+ val Serial = new Properties.Long(SERIAL)
val MESSAGE = "message"
@@ -386,6 +387,76 @@
case _ => None
}
}
+
+ /* simplifier trace */
+
+ val TEXT = "text"
+ val Text = new Properties.String(TEXT)
+
+ val PARENT = "parent"
+ val Parent = new Properties.Long(PARENT)
+
+ val SUCCESS = "success"
+ val Success = new Properties.Boolean(SUCCESS)
+
+ val CANCEL_SIMP_TRACE = "simp_trace_cancel"
+ object Cancel_Simp_Trace
+ {
+ def unapply(props: Properties.T): Option[Long] =
+ props match {
+ case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
+ case _ => None
+ }
+ }
+
+ val SIMP_TRACE = "simp_trace"
+ object Simp_Trace
+ {
+ def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
+ tree match {
+ case XML.Elem(Markup(SIMP_TRACE, props), _) =>
+ (props, props) match {
+ case (Serial(serial), Name(name)) =>
+ Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
+ case _ =>
+ None
+ }
+ case _ =>
+ None
+ }
+ }
+
+ /* trace items from the prover */
+
+ object Simp_Trace_Item
+ {
+
+ def unapply(tree: XML.Tree): Option[(String, Data)] =
+ tree match {
+ case XML.Elem(Markup(RESULT, Serial(serial)), List(
+ XML.Elem(Markup(markup, props), content)
+ )) if markup.startsWith("simp_trace_") =>
+ (props, props) match {
+ case (Text(text), Parent(parent)) =>
+ Some((markup, Data(serial, markup, text, parent, props, content)))
+ case _ =>
+ None
+ }
+ case _ =>
+ None
+ }
+
+ val LOG = "simp_trace_log"
+ val STEP = "simp_trace_step"
+ val RECURSE = "simp_trace_recurse"
+ val HINT = "simp_trace_hint"
+ val IGNORE = "simp_trace_ignore"
+
+ case class Data(serial: Long, markup: String, text: String,
+ parent: Long, props: Properties.T, content: XML.Body)
+
+ }
+
}
--- a/src/Pure/System/session.scala Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/System/session.scala Tue Feb 04 09:04:59 2014 +0000
@@ -139,7 +139,7 @@
val syslog_messages = new Event_Bus[Isabelle_Process.Output]
val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
-
+ val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
/** buffered command changes (delay_first discipline) **/
--- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 04 09:04:59 2014 +0000
@@ -1,38 +1,435 @@
(* Title: Pure/Tools/simplifier_trace.ML
- Author: Lars Hupel, TU Muenchen
+ Author: Lars Hupel
Interactive Simplifier trace.
*)
signature SIMPLIFIER_TRACE =
sig
- val simp_trace_test: bool Config.T
+ val add_term_breakpoint: term -> Context.generic -> Context.generic
+ val add_thm_breakpoint: thm -> Context.generic -> Context.generic
end
structure Simplifier_Trace: SIMPLIFIER_TRACE =
struct
-(* Simplifier trace operations *)
+(** background data **)
+
+datatype mode = Disabled | Normal | Full
+
+fun merge_modes Disabled m = m
+ | merge_modes Normal Full = Full
+ | merge_modes Normal _ = Normal
+ | merge_modes Full _ = Full
+
+val empty_breakpoints =
+ (Item_Net.init (op =) single (* FIXME equality on terms? *),
+ Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
+
+fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
+ (Item_Net.merge (term_bs1, term_bs2),
+ Item_Net.merge (thm_bs1, thm_bs2))
+
+structure Data = Generic_Data
+(
+ type T =
+ {max_depth: int,
+ depth: int,
+ mode: mode,
+ interactive: bool,
+ parent: int,
+ breakpoints: term Item_Net.T * rrule Item_Net.T}
+ val empty =
+ {max_depth = 10,
+ depth = 0,
+ mode = Disabled,
+ interactive = false,
+ parent = 0,
+ breakpoints = empty_breakpoints}
+ val extend = I
+ fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
+ breakpoints = breakpoints1, ...},
+ {max_depth = max_depth2, mode = mode2, interactive = interactive2,
+ breakpoints = breakpoints2, ...}) =
+ {max_depth = Int.max (max_depth1, max_depth2),
+ depth = 0,
+ mode = merge_modes mode1 mode2,
+ interactive = interactive1 orelse interactive2,
+ parent = 0,
+ breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}
+)
+
+fun map_breakpoints f_term f_thm =
+ Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} =>
+ {max_depth = max_depth,
+ depth = depth,
+ mode = mode,
+ interactive = interactive,
+ parent = parent,
+ breakpoints = (f_term term_bs, f_thm thm_bs)})
+
+fun add_term_breakpoint term =
+ map_breakpoints (Item_Net.update term) I
+
+fun add_thm_breakpoint thm context =
+ let
+ val rrules = mk_rrules (Context.proof_of context) [thm]
+ in
+ map_breakpoints I (fold Item_Net.update rrules) context
+ end
+
+fun is_breakpoint (term, rrule) context =
+ let
+ val {breakpoints, ...} = Data.get context
+
+ fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
+ val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
+
+ val {thm = thm, ...} = rrule
+ val thm_matches = exists (eq_rrule o pair rrule)
+ (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
+ in
+ (term_matches, thm_matches)
+ end
+
+(** config and attributes **)
+
+fun config raw_mode interactive max_depth =
+ let
+ val mode = case raw_mode of
+ "normal" => Normal
+ | "full" => Full
+ | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)
+
+ val update = Data.map (fn {depth, parent, breakpoints, ...} =>
+ {max_depth = max_depth,
+ depth = depth,
+ mode = mode,
+ interactive = interactive,
+ parent = parent,
+ breakpoints = breakpoints})
+ in Thm.declaration_attribute (K update) end
+
+fun term_breakpoint terms =
+ Thm.declaration_attribute (K (fold add_term_breakpoint terms))
+
+val thm_breakpoint =
+ Thm.declaration_attribute add_thm_breakpoint
+
+(** tracing state **)
+
+val futures =
+ Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
+
+(** markup **)
+
+fun output_result (id, data) =
+ Output.result (Markup.serial_properties id) data
+
+val serialN = "serial"
+val parentN = "parent"
+val textN = "text"
+val successN = "success"
+
+val logN = "simp_trace_log"
+val stepN = "simp_trace_step"
+val recurseN = "simp_trace_recurse"
+val hintN = "simp_trace_hint"
+val ignoreN = "simp_trace_ignore"
+
+val cancelN = "simp_trace_cancel"
+
+type payload =
+ {props: Properties.T,
+ pretty: Pretty.T}
+
+fun empty_payload () : payload =
+ {props = [], pretty = Pretty.str ""}
+
+fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
+ let
+ val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt)
+
+ val eligible =
+ case mode of
+ Disabled => false
+ | Normal => triggered
+ | Full => true
+
+ val markup' = if markup = stepN andalso not interactive then logN else markup
+ in
+ if not eligible orelse depth > max_depth then
+ NONE
+ else
+ let
+ val {props = more_props, pretty} = payload ()
+ val props =
+ [(textN, text),
+ (parentN, Markup.print_int parent)]
+ val data =
+ Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
+ in
+ SOME (serial (), data)
+ end
+ end
+
+(** tracing output **)
+
+fun send_request (result_id, content) =
+ let
+ fun break () =
+ (Output.protocol_message
+ [(Markup.functionN, cancelN),
+ (serialN, Markup.print_int result_id)]
+ "";
+ Synchronized.change futures (Inttab.delete_safe result_id))
+ val promise = Future.promise break : string future
+ in
+ Synchronized.change futures (Inttab.update_new (result_id, promise));
+ output_result (result_id, content);
+ promise
+ end
+
+
+fun step {term, thm, unconditional, ctxt, rrule} =
+ let
+ val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
+
+ val {name, ...} = rrule
+ val term_triggered = not (null matching_terms)
-val simp_trace_test =
- Attrib.setup_config_bool @{binding simp_trace_test} (K false)
+ val text =
+ if unconditional then
+ "Apply rewrite rule?"
+ else
+ "Apply conditional rewrite rule?"
+
+ fun payload () =
+ let
+ (* FIXME pretty printing via Proof_Context.pretty_fact *)
+ val pretty_thm = Pretty.block
+ [Pretty.str ("Instance of " ^ name ^ ":"),
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt (Thm.prop_of thm)]
+
+ val pretty_term = Pretty.block
+ [Pretty.str "Trying to rewrite:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt term]
+
+ val pretty_matchings =
+ let
+ val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms
+ in
+ if not (null matching_terms) then
+ [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))]
+ else
+ []
+ end
+
+ val pretty =
+ Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings)
+ in
+ {props = [], pretty = pretty}
+ end
+
+ val {max_depth, depth, mode, interactive, breakpoints, ...} =
+ Data.get (Context.Proof ctxt)
+
+ fun mk_promise result =
+ let
+ val result_id = #1 result
+
+ fun put mode' interactive' = Data.put
+ {max_depth = max_depth,
+ depth = depth,
+ mode = mode',
+ interactive = interactive',
+ parent = result_id,
+ breakpoints = breakpoints} (Context.Proof ctxt) |>
+ Context.the_proof
+
+ fun to_response "skip" = NONE
+ | to_response "continue" = SOME (put mode true)
+ | to_response "continue_trace" = SOME (put Full true)
+ | to_response "continue_passive" = SOME (put mode false)
+ | to_response "continue_disable" = SOME (put Disabled false)
+ | to_response _ = raise Fail "Simplifier_Trace.step: invalid message"
+ in
+ if not interactive then
+ (output_result result; Future.value (SOME (put mode false)))
+ else
+ Future.map to_response (send_request result)
+ end
+
+ in
+ case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
+ NONE => Future.value (SOME ctxt)
+ | SOME res => mk_promise res
+ end
+
+fun recurse text term ctxt =
+ let
+ fun payload () =
+ {props = [],
+ pretty = Syntax.pretty_term ctxt term}
+
+ val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt)
+
+ fun put result_id = Data.put
+ {max_depth = max_depth,
+ depth = depth + 1,
+ mode = if depth >= max_depth then Disabled else mode,
+ interactive = interactive,
+ parent = result_id,
+ breakpoints = breakpoints} (Context.Proof ctxt)
+
+ val context' =
+ case mk_generic_result recurseN text true payload ctxt of
+ NONE =>
+ put 0
+ | SOME res =>
+ (output_result res; put (#1 res))
+ in Context.the_proof context' end
+
+fun indicate_failure {term, ctxt, thm, rrule, ...} ctxt' =
+ let
+ fun payload () =
+ let
+ val {name, ...} = rrule
+ val pretty_thm =
+ (* FIXME pretty printing via Proof_Context.pretty_fact *)
+ Pretty.block
+ [Pretty.str ("In an instance of " ^ name ^ ":"),
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt (Thm.prop_of thm)]
+
+ val pretty_term =
+ Pretty.block
+ [Pretty.str "Was trying to rewrite:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt term]
+
+ val pretty =
+ Pretty.chunks [pretty_thm, pretty_term]
+ in
+ {props = [(successN, "false")], pretty = pretty}
+ end
+
+ val {interactive, ...} = Data.get (Context.Proof ctxt)
+ val {parent, ...} = Data.get (Context.Proof ctxt')
+
+ fun mk_promise result =
+ let
+ val result_id = #1 result
+
+ fun to_response "exit" =
+ false
+ | to_response "redo" =
+ (Option.app output_result
+ (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
+ true)
+ | to_response _ =
+ raise Fail "Simplifier_Trace.indicate_failure: invalid message"
+ in
+ if not interactive then
+ (output_result result; Future.value false)
+ else
+ Future.map to_response (send_request result)
+ end
+ in
+ case mk_generic_result hintN "Step failed" true payload ctxt' of
+ NONE => Future.value false
+ | SOME res => mk_promise res
+ end
+
+fun indicate_success thm ctxt =
+ let
+ fun payload () =
+ {props = [(successN, "true")],
+ pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
+ in
+ Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
+ end
+
+(** setup **)
+
+fun simp_if_continue args ctxt cont =
+ let
+ val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
+ val data =
+ {term = term,
+ unconditional = unconditional,
+ ctxt = ctxt,
+ thm = thm,
+ rrule = rrule}
+ in
+ case Future.join (step data) of
+ NONE =>
+ NONE
+ | SOME ctxt' =>
+ let val res = cont ctxt' in
+ case res of
+ NONE =>
+ if Future.join (indicate_failure data ctxt') then
+ simp_if_continue args ctxt cont
+ else
+ NONE
+ | SOME (thm, _) =>
+ (indicate_success thm ctxt';
+ res)
+ end
+ end
+
+val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
val _ = Theory.setup
(Simplifier.set_trace_ops
- {trace_invoke = fn {depth, term} => fn ctxt =>
- (if Config.get ctxt simp_trace_test then
- tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
- Syntax.string_of_term ctxt term)
- else (); ctxt),
- trace_apply = fn args => fn ctxt => fn cont =>
- (if Config.get ctxt simp_trace_test then
- tracing ("Simplifier " ^ @{make_string} args)
- else (); cont ctxt)})
+ {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
+ trace_apply = simp_if_continue})
+
+val _ =
+ Isabelle_Process.protocol_command "Document.simp_trace_reply"
+ (fn [s, r] =>
+ let
+ val serial = Markup.parse_int s
+ fun lookup_delete tab =
+ (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
+ fun apply_result (SOME promise) = Future.fulfill promise r
+ | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
+ in
+ (Synchronized.change_result futures lookup_delete |> apply_result)
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
+ end)
+
+(** attributes **)
+
+val pat_parser =
+ Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
+val mode_parser: string parser =
+ Scan.optional
+ (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
+ "normal"
-(* PIDE protocol *)
+val interactive_parser: bool parser =
+ Scan.optional (Args.$$$ "interactive" >> K true) false
+
+val depth_parser =
+ Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
+
+val config_parser =
+ (interactive_parser -- mode_parser -- depth_parser) >>
+ (fn ((interactive, mode), depth) => config mode interactive depth)
-val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
+val _ = Theory.setup
+ (Attrib.setup @{binding break_term}
+ ((Scan.repeat1 pat_parser) >> term_breakpoint)
+ "declaration of a term breakpoint" #>
+ Attrib.setup @{binding break_thm}
+ (Scan.succeed thm_breakpoint)
+ "declaration of a theorem breakpoint" #>
+ Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
+ "simplifier trace configuration")
end
-
--- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 04 09:04:59 2014 +0000
@@ -1,18 +1,279 @@
/* Title: Pure/Tools/simplifier_trace.scala
- Author: Lars Hupel, TU Muenchen
+ Author: Lars Hupel
Interactive Simplifier trace.
*/
package isabelle
+import scala.actors.Actor._
+import scala.annotation.tailrec
+import scala.collection.immutable.SortedMap
+
object Simplifier_Trace
{
- /* PIDE protocol */
+
+ import Markup.Simp_Trace_Item
+
+
+ /* replies to the prover */
+
+ case class Answer private[Simplifier_Trace](val name: String, val string: String)
+
+ object Answer
+ {
+
+ object step
+ {
+ val skip = Answer("skip", "Skip")
+ val continue = Answer("continue", "Continue")
+ val continue_trace = Answer("continue_trace", "Continue (with full trace)")
+ val continue_passive = Answer("continue_passive", "Continue (without asking)")
+ val continue_disable = Answer("continue_disable", "Continue (without any trace)")
+
+ val default = skip
+ val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
+ }
+
+ object hint_fail
+ {
+ val exit = Answer("exit", "Exit")
+ val redo = Answer("redo", "Redo")
+
+ val default = exit
+ val all = List(redo, exit)
+ }
+
+ }
+
+ val all_answers = Answer.step.all ++ Answer.hint_fail.all
+
+
+ /* GUI interaction */
+
+ case object Event
+
+
+ /* manager actor */
+
+ private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
+ private case class Generate_Trace(results: Command.Results)
+ private case class Cancel(serial: Long)
+ private object Clear_Memory
+ private object Stop
+ case class Reply(session: Session, serial: Long, answer: Answer)
+
+ case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
+
+ case class Context(
+ last_serial: Long = 0L,
+ questions: SortedMap[Long, Question] = SortedMap.empty
+ )
+ {
+
+ def +(q: Question): Context =
+ copy(questions = questions + ((q.data.serial, q)))
+
+ def -(s: Long): Context =
+ copy(questions = questions - s)
+
+ def with_serial(s: Long): Context =
+ copy(last_serial = Math.max(last_serial, s))
+
+ }
+
+ case class Trace(entries: List[Simp_Trace_Item.Data])
+
+ case class Index(text: String, content: XML.Body)
+
+ object Index
+ {
+ def of_data(data: Simp_Trace_Item.Data): Index =
+ Index(data.text, data.content)
+ }
+
+ def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
+ (manager !? Handle_Results(session, id, results)).asInstanceOf[Context]
+
+ def generate_trace(results: Command.Results): Trace =
+ (manager !? Generate_Trace(results)).asInstanceOf[Trace]
+
+ def clear_memory() =
+ manager ! Clear_Memory
+
+ def send_reply(session: Session, serial: Long, answer: Answer) =
+ manager ! Reply(session, serial, answer)
+
+ private val manager = actor {
+ var contexts = Map.empty[Document_ID.Command, Context]
+
+ var memory_children = Map.empty[Long, Set[Long]]
+ var memory = Map.empty[Index, Answer]
+
+ def find_question(serial: Long): Option[(Document_ID.Command, Question)] =
+ contexts collectFirst {
+ case (id, context) if context.questions contains serial =>
+ (id, context.questions(serial))
+ }
+
+ def do_cancel(serial: Long, id: Document_ID.Command)
+ {
+ // To save memory, we could try to remove empty contexts at this point.
+ // However, if a new serial gets attached to the same command_id after we deleted
+ // its context, its last_serial counter will start at 0 again, and we'll think the
+ // old serials are actually new
+ contexts += (id -> (contexts(id) - serial))
+ }
+
+ def do_reply(session: Session, serial: Long, answer: Answer)
+ {
+ session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
+ }
+
+ loop {
+ react {
+ case Handle_Results(session, id, results) =>
+ var new_context = contexts.getOrElse(id, Context())
+ var new_serial = new_context.last_serial
+
+ for ((serial, result) <- results.entries if serial > new_context.last_serial)
+ {
+ result match {
+ case Simp_Trace_Item(markup, data) =>
+ import Simp_Trace_Item._
+
+ memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
+
+ markup match {
+
+ case STEP =>
+ val index = Index.of_data(data)
+ memory.get(index) match {
+ case None =>
+ new_context += Question(data, Answer.step.all, Answer.step.default)
+ case Some(answer) =>
+ do_reply(session, serial, answer)
+ }
+
+ case HINT =>
+ data.props match {
+ case Markup.Success(false) =>
+ results.get(data.parent) match {
+ case Some(Simp_Trace_Item(STEP, _)) =>
+ new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
+ case _ =>
+ // unknown, better send a default reply
+ do_reply(session, data.serial, Answer.hint_fail.default)
+ }
+ case _ =>
+ }
+
+ case IGNORE =>
+ // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
+ // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
+ // to selectively purge the replies which have been memorized, going down from
+ // the parent to all leaves.
+
+ @tailrec
+ def purge(queue: Vector[Long]): Unit =
+ queue match {
+ case s +: rest =>
+ for (Simp_Trace_Item(STEP, data) <- results.get(s))
+ memory -= Index.of_data(data)
+ val children = memory_children.getOrElse(s, Set.empty)
+ memory_children -= s
+ purge(rest ++ children.toVector)
+ case _ =>
+ }
+
+ purge(Vector(data.parent))
+
+ case _ =>
+ }
+
+ case _ =>
+ }
+
+ new_serial = serial
+ }
+
+ new_context = new_context.with_serial(new_serial)
+ contexts += (id -> new_context)
+ reply(new_context)
+
+ case Generate_Trace(results) =>
+ // Since there are potentially lots of trace messages, we do not cache them here again.
+ // Instead, everytime the trace is being requested, we re-assemble it based on the
+ // current results.
+
+ val items =
+ for { (_, Simp_Trace_Item(_, data)) <- results.entries }
+ yield data
+
+ reply(Trace(items.toList))
+
+ case Cancel(serial) =>
+ find_question(serial) match {
+ case Some((id, _)) =>
+ do_cancel(serial, id)
+ case None =>
+ System.err.println("handle_cancel: unknown serial " + serial)
+ }
+
+ case Clear_Memory =>
+ memory_children = Map.empty
+ memory = Map.empty
+
+ case Stop =>
+ contexts = Map.empty
+ exit("Simplifier_Trace: manager actor stopped")
+
+ case Reply(session, serial, answer) =>
+ find_question(serial) match {
+ case Some((id, Question(data, _, _))) =>
+ if (data.markup == Markup.Simp_Trace_Item.STEP)
+ {
+ val index = Index.of_data(data)
+ memory += (index -> answer)
+ }
+ do_cancel(serial, id)
+ case None =>
+ System.err.println("send_reply: unknown serial " + serial)
+ }
+
+ do_reply(session, serial, answer)
+ session.trace_events.event(Event)
+
+ case bad =>
+ System.err.println("context_manager: bad message " + bad)
+ }
+ }
+ }
+
+
+ /* protocol handler */
class Handler extends Session.Protocol_Handler
{
- val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean]
+ private def cancel(
+ prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+ msg.properties match {
+ case Markup.Cancel_Simp_Trace(serial) =>
+ manager ! Cancel(serial)
+ true
+ case _ =>
+ false
+ }
+
+ override def stop(prover: Session.Prover) =
+ {
+ manager ! Clear_Memory
+ manager ! Stop
+ }
+
+ val functions = Map(
+ Markup.CANCEL_SIMP_TRACE -> cancel _)
}
+
}
--- a/src/Pure/raw_simplifier.ML Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Feb 04 09:04:59 2014 +0000
@@ -17,6 +17,7 @@
val simp_trace: bool Config.T
type cong_name = bool * string
type rrule
+ val mk_rrules: Proof.context -> thm list -> rrule list
val eq_rrule: rrule * rrule -> bool
type proc
type solver
@@ -571,6 +572,12 @@
fun extract_safe_rrules ctxt thm =
maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
+fun mk_rrules ctxt thms =
+ let
+ val rews = extract_rews ctxt thms
+ val raw_rrules = flat (map (mk_rrule ctxt) rews)
+ in map mk_rrule2 raw_rrules end
+
(* add/del rules explicitly *)
@@ -588,7 +595,6 @@
fun add_simp thm ctxt = ctxt addsimps [thm];
fun del_simp thm ctxt = ctxt delsimps [thm];
-
(* congs *)
local
@@ -814,7 +820,7 @@
type trace_ops =
{trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
- trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
+ trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
structure Trace_Ops = Theory_Data
@@ -919,8 +925,9 @@
val eta_thm = Thm.eta_conversion t;
val eta_t' = Thm.rhs_of eta_thm;
val eta_t = term_of eta_t';
- fun rew {thm, name, lhs, elhs, extra, fo, perm} =
+ fun rew rrule =
let
+ val {thm, name, lhs, elhs, extra, fo, perm} = rrule
val prop = Thm.prop_of thm;
val (rthm, elhs') =
if maxt = ~1 orelse not extra then (thm, elhs)
@@ -932,7 +939,7 @@
val prop' = Thm.prop_of thm';
val unconditional = (Logic.count_prems prop' = 0);
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
- val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name};
+ val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
in
if perm andalso not (termless (rhs', lhs'))
then
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Feb 04 09:04:59 2014 +0000
@@ -39,6 +39,8 @@
"src/rich_text_area.scala"
"src/scala_console.scala"
"src/sledgehammer_dockable.scala"
+ "src/simplifier_trace_dockable.scala"
+ "src/simplifier_trace_window.scala"
"src/symbols_dockable.scala"
"src/syslog_dockable.scala"
"src/text_overview.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Feb 04 09:04:59 2014 +0000
@@ -37,6 +37,7 @@
isabelle.protocol-panel \
isabelle.raw-output-panel \
isabelle.sledgehammer-panel \
+ isabelle.simp-trace-panel \
isabelle.symbols-panel \
isabelle.syslog-panel \
isabelle.theories-panel \
@@ -47,6 +48,7 @@
isabelle.output-panel.label=Output panel
isabelle.protocol-panel.label=Protocol panel
isabelle.raw-output-panel.label=Raw Output panel
+isabelle.simp-trace-panel.label=Simplifier trace panel
isabelle.sledgehammer-panel.label=Sledgehammer panel
isabelle.symbols-panel.label=Symbols panel
isabelle.syslog-panel.label=Syslog panel
@@ -59,6 +61,7 @@
isabelle-info.title=Info
isabelle-monitor.title=Monitor
isabelle-output.title=Output
+isabelle-simp-trace.title=Simplifier trace
isabelle-protocol.title=Protocol
isabelle-raw-output.title=Raw Output
isabelle-documentation.title=Documentation
--- a/src/Tools/jEdit/src/actions.xml Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/actions.xml Tue Feb 04 09:04:59 2014 +0000
@@ -42,6 +42,11 @@
wm.addDockableWindow("isabelle-raw-output");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.simp-trace-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-simp-trace");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.protocol-panel">
<CODE>
wm.addDockableWindow("isabelle-protocol");
@@ -147,4 +152,4 @@
isabelle.jedit.Isabelle.input_bsup(textArea);
</CODE>
</ACTION>
-</ACTIONS>
\ No newline at end of file
+</ACTIONS>
--- a/src/Tools/jEdit/src/active.scala Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/active.scala Tue Feb 04 09:04:59 2014 +0000
@@ -61,6 +61,9 @@
else text_area.setSelectedText(text)
}
+ case Markup.Simp_Trace(serial, answer) =>
+ Simplifier_Trace.send_reply(PIDE.session, serial, answer)
+
case Protocol.Dialog(id, serial, result) =>
model.session.dialog_result(id, serial, result)
@@ -72,4 +75,3 @@
}
}
}
-
--- a/src/Tools/jEdit/src/dockables.xml Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Tue Feb 04 09:04:59 2014 +0000
@@ -41,4 +41,7 @@
<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
new isabelle.jedit.Symbols_Dockable(view, position);
</DOCKABLE>
-</DOCKABLES>
\ No newline at end of file
+ <DOCKABLE NAME="isabelle-simp-trace" MOVABLE="TRUE">
+ new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
+ </DOCKABLE>
+</DOCKABLES>
--- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 04 09:04:59 2014 +0000
@@ -81,6 +81,12 @@
case _ => None
}
+ def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] =
+ wm(view).getDockableWindow("isabelle-simp-trace") match {
+ case dockable: Simplifier_Trace_Dockable => Some(dockable)
+ case _ => None
+ }
+
def docked_protocol(view: View): Option[Protocol_Dockable] =
wm(view).getDockableWindow("isabelle-protocol") match {
case dockable: Protocol_Dockable => Some(dockable)
--- a/src/Tools/jEdit/src/jEdit.props Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Tue Feb 04 09:04:59 2014 +0000
@@ -189,6 +189,7 @@
isabelle-output.height=174
isabelle-output.width=412
isabelle-sledgehammer.dock-position=bottom
+isabelle-simp-trace.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
isabelle.complete.label=Complete Isabelle text
--- a/src/Tools/jEdit/src/rendering.scala Tue Feb 04 01:35:48 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 04 09:04:59 2014 +0000
@@ -270,7 +270,7 @@
private val active_include =
- Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
+ Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
snapshot.select_markup(range, Some(active_include), command_state =>
@@ -281,7 +281,8 @@
case Text.Info(info_range, elem) =>
if (elem.name == Markup.BROWSER ||
elem.name == Markup.GRAPHVIEW ||
- elem.name == Markup.SENDBACK)
+ elem.name == Markup.SENDBACK ||
+ elem.name == Markup.SIMP_TRACE)
Some(Text.Info(snapshot.convert(info_range), elem))
else None
}) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 04 09:04:59 2014 +0000
@@ -0,0 +1,222 @@
+/* Title: Tools/jEdit/src/simplifier_trace_dockable.scala
+ Author: Lars Hupel
+
+Dockable window with interactive simplifier trace.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import scala.swing.{Button, CheckBox, Orientation, Separator}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import org.gjt.sp.jedit.View
+
+class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ Swing_Thread.require()
+
+ /* component state -- owned by Swing thread */
+
+ private var current_snapshot = Document.State.init.snapshot()
+ private var current_state = Command.empty.init_state
+ private var current_id = 0L
+ private var do_update = true
+ private var do_auto_reply = false
+
+
+ private val text_area = new Pretty_Text_Area(view)
+ set_content(text_area)
+
+ private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
+ {
+ val data = question.data
+
+ def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
+ XML.Wrapped_Elem(
+ Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
+ Nil,
+ List(XML.Text(answer.string))
+ )
+
+ def make_block(body: XML.Body): XML.Body =
+ List(Pretty.Block(0, body))
+
+ val all = Pretty.separate(
+ XML.Text(data.text) ::
+ data.content :::
+ make_block(Library.separate(XML.Text(", "), question.answers map make_button))
+ )
+
+ XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
+ }
+
+ private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
+ {
+ Swing_Thread.require()
+ val questions = context.questions.values
+ if (do_auto_reply && !questions.isEmpty)
+ {
+ questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
+ handle_update(do_update)
+ }
+ else
+ {
+ val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
+ text_area.update(snapshot, Command.Results.empty, contents)
+ do_paint()
+ }
+ }
+
+ private def show_trace()
+ {
+ val trace = Simplifier_Trace.generate_trace(current_state.results)
+ new Simplifier_Trace_Window(view, current_snapshot, trace)
+ }
+
+ private def do_paint()
+ {
+ Swing_Thread.later {
+ text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+ }
+ }
+
+ private def update_contents()
+ {
+ set_context(
+ current_snapshot,
+ Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results)
+ )
+ }
+
+ private def handle_resize()
+ {
+ do_paint()
+ }
+
+ private def handle_update(follow: Boolean)
+ {
+ val (new_snapshot, new_state, new_id) =
+ PIDE.editor.current_node_snapshot(view) match {
+ case Some(snapshot) =>
+ if (follow && !snapshot.is_outdated) {
+ PIDE.editor.current_command(view, snapshot) match {
+ case Some(cmd) =>
+ (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id)
+ case None =>
+ (Document.State.init.snapshot(), Command.empty.init_state, 0L)
+ }
+ }
+ else (current_snapshot, current_state, current_id)
+ case None => (current_snapshot, current_state, current_id)
+ }
+
+ current_snapshot = new_snapshot
+ current_state = new_state
+ current_id = new_id
+ update_contents()
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case _: Session.Global_Options =>
+ Swing_Thread.later { handle_resize() }
+ case changed: Session.Commands_Changed =>
+ Swing_Thread.later { handle_update(do_update) }
+ case Session.Caret_Focus =>
+ Swing_Thread.later { handle_update(do_update) }
+ case Simplifier_Trace.Event =>
+ Swing_Thread.later { handle_update(do_update) }
+ case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ PIDE.session.global_options += main_actor
+ PIDE.session.commands_changed += main_actor
+ PIDE.session.caret_focus += main_actor
+ PIDE.session.trace_events += main_actor
+ handle_update(true)
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ PIDE.session.global_options -= main_actor
+ PIDE.session.commands_changed -= main_actor
+ PIDE.session.caret_focus -= main_actor
+ PIDE.session.trace_events -= main_actor
+ delay_resize.revoke()
+ }
+
+
+ /* resize */
+
+ private val delay_resize =
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* controls */
+
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ new CheckBox("Auto update") {
+ selected = do_update
+ reactions += {
+ case ButtonClicked(_) =>
+ do_update = this.selected
+ handle_update(do_update)
+ }
+ },
+ new Button("Update") {
+ reactions += {
+ case ButtonClicked(_) =>
+ handle_update(true)
+ }
+ },
+ new Separator(Orientation.Vertical),
+ new CheckBox("Auto reply") {
+ selected = do_auto_reply
+ reactions += {
+ case ButtonClicked(_) =>
+ do_auto_reply = this.selected
+ handle_update(do_update)
+ }
+ },
+ new Separator(Orientation.Vertical),
+ new Button("Show trace") {
+ reactions += {
+ case ButtonClicked(_) =>
+ show_trace()
+ }
+ },
+ new Button("Clear memory") {
+ reactions += {
+ case ButtonClicked(_) =>
+ Simplifier_Trace.clear_memory()
+ }
+ }
+ )
+
+ add(controls.peer, BorderLayout.NORTH)
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 04 09:04:59 2014 +0000
@@ -0,0 +1,237 @@
+/* Title: Tools/jEdit/src/simplifier_trace_window.scala
+ Author: Lars Hupel
+
+Trace window with tree-style view of the simplifier trace.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.annotation.tailrec
+
+import scala.collection.immutable.SortedMap
+
+import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
+import scala.swing.event.{Key, KeyPressed}
+
+import scala.util.matching.Regex
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import javax.swing.SwingUtilities
+
+import org.gjt.sp.jedit.View
+
+private object Simplifier_Trace_Window
+{
+
+ import Markup.Simp_Trace_Item
+
+ sealed trait Trace_Tree
+ {
+ var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
+ val serial: Long
+ val parent: Option[Trace_Tree]
+ var hints: List[Simp_Trace_Item.Data]
+ def set_interesting(): Unit
+ }
+
+ final class Root_Tree(val serial: Long) extends Trace_Tree
+ {
+ val parent = None
+ val hints = Nil
+ def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
+ def set_interesting() = ()
+
+ def format(regex: Option[Regex]): XML.Body =
+ Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
+ }
+
+ final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
+ {
+ val serial = data.serial
+ var hints = List.empty[Simp_Trace_Item.Data]
+ var interesting: Boolean = false
+
+ def set_interesting(): Unit =
+ if (!interesting)
+ {
+ interesting = true
+ parent match {
+ case Some(p) =>
+ p.set_interesting()
+ case None =>
+ }
+ }
+
+ def format(regex: Option[Regex]): (Boolean, XML.Tree) =
+ {
+ def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
+ case (false, _) =>
+ None
+ case (true, res) =>
+ Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
+ }
+
+ def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
+ Pretty.block(Pretty.separate(
+ XML.Text(data.text) ::
+ data.content
+ ))
+
+ def body_contains(regex: Regex, body: XML.Body): Boolean =
+ body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
+
+ val children_bodies: XML.Body =
+ children.values.filter(_.interesting).flatMap(format_child).toList
+
+ lazy val hint_bodies: XML.Body =
+ hints.reverse.map(format_hint)
+
+ val eligible = regex match {
+ case None =>
+ true
+ case Some(r) =>
+ body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
+ }
+
+ val all =
+ if (eligible)
+ XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
+ else
+ XML.Text(data.text) :: children_bodies
+
+ val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
+
+ (eligible || children_bodies != Nil, res)
+ }
+ }
+
+ @tailrec
+ def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
+ rest match {
+ case Nil =>
+ ()
+ case head :: tail =>
+ lookup.get(head.parent) match {
+ case Some(parent) =>
+ if (head.markup == Simp_Trace_Item.HINT)
+ {
+ parent.hints ::= head
+ walk_trace(tail, lookup)
+ }
+ else if (head.markup == Simp_Trace_Item.IGNORE)
+ {
+ parent.parent match {
+ case None =>
+ System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
+ case Some(tree) =>
+ tree.children -= head.parent
+ walk_trace(tail, lookup) // FIXME discard from lookup
+ }
+ }
+ else
+ {
+ val entry = new Elem_Tree(head, Some(parent))
+ parent.children += ((head.serial, entry))
+ if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
+ entry.set_interesting()
+ walk_trace(tail, lookup + (head.serial -> entry))
+ }
+
+ case None =>
+ System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
+ }
+ }
+
+}
+
+class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
+{
+
+ import Simplifier_Trace_Window._
+
+ Swing_Thread.require()
+
+ val area = new Pretty_Text_Area(view)
+
+ size = new Dimension(500, 500)
+ contents = new BorderPanel {
+ layout(Component.wrap(area)) = BorderPanel.Position.Center
+ }
+
+ private val tree = trace.entries.headOption match {
+ case Some(first) =>
+ val tree = new Root_Tree(first.parent)
+ walk_trace(trace.entries, Map(first.parent -> tree))
+ tree
+ case None =>
+ new Root_Tree(0)
+ }
+
+ do_update(None)
+ open()
+ do_paint()
+
+ def do_update(regex: Option[Regex])
+ {
+ val xml = tree.format(regex)
+ area.update(snapshot, Command.Results.empty, xml)
+ }
+
+ def do_paint()
+ {
+ Swing_Thread.later {
+ area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+ }
+ }
+
+ def handle_resize()
+ {
+ do_paint()
+ }
+
+
+ /* resize */
+
+ private val delay_resize =
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ peer.addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* controls */
+
+ val use_regex = new CheckBox("Regex")
+
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ new Label {
+ text = "Search"
+ },
+ new TextField(30) {
+ listenTo(keys)
+ reactions += {
+ case KeyPressed(_, Key.Enter, 0, _) =>
+ val input = text.trim
+ val regex =
+ if (input.isEmpty)
+ None
+ else if (use_regex.selected)
+ Some(input.r)
+ else
+ Some(java.util.regex.Pattern.quote(input).r)
+ do_update(regex)
+ do_paint()
+ }
+ },
+ use_regex
+ )
+
+ peer.add(controls.peer, BorderLayout.NORTH)
+}