--- a/src/Pure/PIDE/markup.ML Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Feb 18 18:29:02 2014 +0100
@@ -164,6 +164,12 @@
val command_timing: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
+ val simp_trace_logN: string
+ val simp_trace_stepN: string
+ val simp_trace_recurseN: string
+ val simp_trace_hintN: string
+ val simp_trace_ignoreN: string
+ val simp_trace_cancel: serial -> Properties.T
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -516,6 +522,16 @@
| dest_loading_theory _ = NONE;
+(* simplifier trace *)
+
+val simp_trace_logN = "simp_trace_log";
+val simp_trace_stepN = "simp_trace_step";
+val simp_trace_recurseN = "simp_trace_recurse";
+val simp_trace_hintN = "simp_trace_hint";
+val simp_trace_ignoreN = "simp_trace_ignore";
+
+fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
+
(** print mode operations **)
--- a/src/Pure/PIDE/markup.scala Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Feb 18 18:29:02 2014 +0100
@@ -389,82 +389,26 @@
}
}
+
/* simplifier trace */
- val TEXT = "text"
- val Text = new Properties.String(TEXT)
-
- val PARENT = "parent"
- val Parent = new Properties.Long(PARENT)
+ val SIMP_TRACE = "simp_trace"
- val SUCCESS = "success"
- val Success = new Properties.Boolean(SUCCESS)
+ val SIMP_TRACE_LOG = "simp_trace_log"
+ val SIMP_TRACE_STEP = "simp_trace_step"
+ val SIMP_TRACE_RECURSE = "simp_trace_recurse"
+ val SIMP_TRACE_HINT = "simp_trace_hint"
+ val SIMP_TRACE_IGNORE = "simp_trace_ignore"
- val MEMORY = "memory"
- val Memory = new Properties.Boolean(MEMORY)
-
- val CANCEL_SIMP_TRACE = "simp_trace_cancel"
- object Cancel_Simp_Trace
+ val SIMP_TRACE_CANCEL = "simp_trace_cancel"
+ object Simp_Trace_Cancel
{
def unapply(props: Properties.T): Option[Long] =
props match {
- case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
+ case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
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)
- {
- def memory: Boolean =
- Memory.unapply(props) getOrElse true
- }
-
- }
-
}
--- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 18:29:02 2014 +0100
@@ -146,14 +146,6 @@
val memoryN = "memory"
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}
@@ -171,7 +163,10 @@
| Normal => triggered
| Full => true)
- val markup' = if markup = stepN andalso not interactive then logN else markup
+ val markup' =
+ if markup = Markup.simp_trace_stepN andalso not interactive
+ then Markup.simp_trace_logN
+ else markup
in
if not eligible orelse depth > max_depth then NONE
else
@@ -195,10 +190,7 @@
fun send_request (result_id, content) =
let
fun break () =
- (Output.protocol_message
- [(Markup.functionN, cancelN),
- (serialN, Markup.print_int result_id)]
- "";
+ (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
Synchronized.change futures (Inttab.delete_safe result_id))
val promise = Future.promise break : string future
in
@@ -279,7 +271,8 @@
end
in
- (case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
+ (case mk_generic_result Markup.simp_trace_stepN text
+ (thm_triggered orelse term_triggered) payload ctxt of
NONE => Future.value (SOME ctxt)
| SOME res => mk_promise res)
end
@@ -303,7 +296,7 @@
breakpoints = breakpoints} (Context.Proof ctxt)
val context' =
- (case mk_generic_result recurseN text true payload ctxt of
+ (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
NONE => put 0
| SOME res => (output_result res; put (#1 res)))
in Context.the_proof context' end
@@ -342,7 +335,7 @@
fun to_response "exit" = false
| to_response "redo" =
(Option.app output_result
- (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
+ (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt');
true)
| to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message"
in
@@ -351,7 +344,7 @@
else Future.map to_response (send_request result)
end
in
- (case mk_generic_result hintN "Step failed" true payload ctxt' of
+ (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of
NONE => Future.value false
| SOME res => mk_promise res)
end
@@ -362,7 +355,8 @@
{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)
+ Option.app output_result
+ (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt)
end
@@ -400,7 +394,7 @@
trace_apply = simp_apply})
val _ =
- Isabelle_Process.protocol_command "Document.simp_trace_reply"
+ Isabelle_Process.protocol_command "Simplifier_Trace.reply"
(fn [s, r] =>
let
val serial = Markup.parse_int s
--- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 18:29:02 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.actors.Actor._
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
@@ -13,8 +14,42 @@
object Simplifier_Trace
{
+ /* trace items from the prover */
- import Markup.Simp_Trace_Item
+ 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 MEMORY = "memory"
+ val Memory = new Properties.Boolean(MEMORY)
+
+ object Item
+ {
+ case class Data(
+ serial: Long, markup: String, text: String,
+ parent: Long, props: Properties.T, content: XML.Body)
+ {
+ def memory: Boolean = Memory.unapply(props) getOrElse true
+ }
+
+ def unapply(tree: XML.Tree): Option[(String, Data)] =
+ tree match {
+ case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)),
+ List(XML.Elem(Markup(markup, props), content)))
+ if markup.startsWith("simp_trace_") => // FIXME proper comparison of string constants
+ (props, props) match {
+ case (Text(text), Parent(parent)) =>
+ Some((markup, Data(serial, markup, text, parent, props, content)))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
/* replies to the prover */
@@ -23,7 +58,6 @@
object Answer
{
-
object step
{
val skip = Answer("skip", "Skip")
@@ -44,11 +78,24 @@
val default = exit
val all = List(redo, exit)
}
-
}
val all_answers = Answer.step.all ++ Answer.hint_fail.all
+ object Active
+ {
+ def unapply(tree: XML.Tree): Option[(Long, Answer)] =
+ tree match {
+ case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
+ (props, props) match {
+ case (Markup.Serial(serial), Markup.Name(name)) =>
+ all_answers.find(_.name == name).map((serial, _))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
/* GUI interaction */
@@ -64,7 +111,7 @@
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 Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
case class Context(
last_serial: Long = 0L,
@@ -83,13 +130,13 @@
}
- case class Trace(entries: List[Simp_Trace_Item.Data])
+ case class Trace(entries: List[Item.Data])
case class Index(text: String, content: XML.Body)
object Index
{
- def of_data(data: Simp_Trace_Item.Data): Index =
+ def of_data(data: Item.Data): Index =
Index(data.text, data.content)
}
@@ -128,7 +175,7 @@
def do_reply(session: Session, serial: Long, answer: Answer)
{
- session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
+ session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
}
loop {
@@ -140,14 +187,12 @@
for ((serial, result) <- results.entries if serial > new_context.last_serial)
{
result match {
- case Simp_Trace_Item(markup, data) =>
- import Simp_Trace_Item._
-
+ case Item(markup, data) =>
memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
markup match {
- case STEP =>
+ case Markup.SIMP_TRACE_STEP =>
val index = Index.of_data(data)
memory.get(index) match {
case Some(answer) if data.memory =>
@@ -156,11 +201,11 @@
new_context += Question(data, Answer.step.all, Answer.step.default)
}
- case HINT =>
+ case Markup.SIMP_TRACE_HINT =>
data.props match {
- case Markup.Success(false) =>
+ case Success(false) =>
results.get(data.parent) match {
- case Some(Simp_Trace_Item(STEP, _)) =>
+ case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
case _ =>
// unknown, better send a default reply
@@ -169,7 +214,7 @@
case _ =>
}
- case IGNORE =>
+ case Markup.SIMP_TRACE_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
@@ -179,7 +224,7 @@
def purge(queue: Vector[Long]): Unit =
queue match {
case s +: rest =>
- for (Simp_Trace_Item(STEP, data) <- results.get(s))
+ for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
memory -= Index.of_data(data)
val children = memory_children.getOrElse(s, Set.empty)
memory_children -= s
@@ -208,7 +253,7 @@
// current results.
val items =
- for { (_, Simp_Trace_Item(_, data)) <- results.entries }
+ for { (_, Item(_, data)) <- results.entries }
yield data
reply(Trace(items.toList))
@@ -232,7 +277,7 @@
case Reply(session, serial, answer) =>
find_question(serial) match {
case Some((id, Question(data, _, _))) =>
- if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory)
+ if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
{
val index = Index.of_data(data)
memory += (index -> answer)
@@ -256,10 +301,9 @@
class Handler extends Session.Protocol_Handler
{
- private def cancel(
- prover: Session.Prover, msg: 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) =>
+ case Markup.Simp_Trace_Cancel(serial) =>
manager ! Cancel(serial)
true
case _ =>
@@ -272,8 +316,6 @@
manager ! Stop
}
- val functions = Map(
- Markup.CANCEL_SIMP_TRACE -> cancel _)
+ val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
}
-
}
--- a/src/Tools/jEdit/src/active.scala Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Tools/jEdit/src/active.scala Tue Feb 18 18:29:02 2014 +0100
@@ -61,7 +61,7 @@
else text_area.setSelectedText(text)
}
- case Markup.Simp_Trace(serial, answer) =>
+ case Simplifier_Trace.Active(serial, answer) =>
Simplifier_Trace.send_reply(PIDE.session, serial, answer)
case Protocol.Dialog(id, serial, result) =>
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 17:26:13 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 18:29:02 2014 +0100
@@ -10,12 +10,9 @@
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
@@ -25,17 +22,15 @@
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]
+ var hints: List[Simplifier_Trace.Item.Data]
def set_interesting(): Unit
}
@@ -43,17 +38,19 @@
{
val parent = None
val hints = Nil
- def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
+ def hints_=(xs: List[Simplifier_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
+ final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
+ extends Trace_Tree
{
val serial = data.serial
- var hints = List.empty[Simp_Trace_Item.Data]
+ var hints = List.empty[Simplifier_Trace.Item.Data]
var interesting: Boolean = false
def set_interesting(): Unit =
@@ -76,7 +73,7 @@
Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
}
- def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
+ def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
Pretty.block(Pretty.separate(
XML.Text(data.text) ::
data.content
@@ -111,19 +108,19 @@
}
@tailrec
- def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
+ def walk_trace(rest: List[Simplifier_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)
+ if (head.markup == Markup.SIMP_TRACE_HINT)
{
parent.hints ::= head
walk_trace(tail, lookup)
}
- else if (head.markup == Simp_Trace_Item.IGNORE)
+ else if (head.markup == Markup.SIMP_TRACE_IGNORE)
{
parent.parent match {
case None =>
@@ -137,7 +134,7 @@
{
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)
+ if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG)
entry.set_interesting()
walk_trace(tail, lookup + (head.serial -> entry))
}