--- a/src/Pure/Tools/simplifier_trace.scala Mon Jul 21 16:49:06 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala Mon Jul 21 16:58:12 2014 +0200
@@ -65,7 +65,6 @@
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)
}
@@ -74,27 +73,12 @@
val exit = Answer("exit", "Exit")
val redo = Answer("redo", "Redo")
- val default = exit
val all = List(redo, exit)
}
}
val all_answers: List[Answer] = 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 */
@@ -110,7 +94,7 @@
private object Clear_Memory
case class Reply(session: Session, serial: Long, answer: Answer)
- case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
+ case class Question(data: Item.Data, answers: List[Answer])
case class Context(
last_serial: Long = 0L,
@@ -207,7 +191,7 @@
case Some(answer) if data.memory =>
do_reply(session, serial, answer)
case _ =>
- new_context += Question(data, Answer.step.all, Answer.step.default)
+ new_context += Question(data, Answer.step.all)
}
case Markup.SIMP_TRACE_HINT =>
@@ -215,11 +199,10 @@
case Success(false) =>
results.get(data.parent) match {
case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
- new_context +=
- Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
+ new_context += Question(data, Answer.hint_fail.all)
case _ =>
// unknown, better send a default reply
- do_reply(session, data.serial, Answer.hint_fail.default)
+ do_reply(session, data.serial, Answer.hint_fail.exit)
}
case _ =>
}
@@ -263,8 +246,7 @@
// current results.
val items =
- (for { (_, Item(_, data)) <- results.iterator }
- yield data).toList
+ results.iterator.collect { case (_, Item(_, data)) => data }.toList
slot.fulfill(Trace(items))
@@ -281,7 +263,7 @@
case Reply(session, serial, answer) =>
find_question(serial) match {
- case Some((id, Question(data, _, _))) =>
+ case Some((id, Question(data, _))) =>
if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
{
val index = Index.of_data(data)
--- a/src/Tools/jEdit/src/active.scala Mon Jul 21 16:49:06 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala Mon Jul 21 16:58:12 2014 +0200
@@ -60,9 +60,6 @@
}
text_area.requestFocus
- case Simplifier_Trace.Active(serial, answer) =>
- Simplifier_Trace.send_reply(PIDE.session, serial, answer)
-
case Protocol.Dialog(id, serial, result) =>
model.session.dialog_result(id, serial, result)
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Jul 21 16:49:06 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Jul 21 16:58:12 2014 +0200
@@ -29,50 +29,38 @@
private var current_results = Command.Results.empty
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 =
+ private def update_contents()
{
- 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))
- )
+ Swing_Thread.require {}
- def make_block(body: XML.Body): XML.Body =
- List(Pretty.Block(0, body))
+ val snapshot = current_snapshot
+ val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
- 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)))
- }
+ answers.contents.clear()
+ context.questions.values.toList match {
+ case q :: _ =>
+ val data = q.data
+ val content = Pretty.separate(XML.Text(data.text) :: data.content)
+ text_area.update(snapshot, Command.Results.empty, content)
+ q.answers.foreach { answer =>
+ answers.contents += new Button(answer.string) {
+ reactions += {
+ case ButtonClicked(_) =>
+ Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
+ }
+ }
+ }
+ case Nil =>
+ text_area.update(snapshot, Command.Results.empty, Nil)
+ }
- 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()
- }
+ do_paint()
}
private def show_trace()
@@ -88,14 +76,6 @@
}
}
- private def update_contents()
- {
- set_context(
- current_snapshot,
- Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
- )
- }
-
private def handle_resize()
{
do_paint()
@@ -195,15 +175,6 @@
}
},
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(_) =>
@@ -218,5 +189,8 @@
}
)
+ private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
+
add(controls.peer, BorderLayout.NORTH)
+ add(answers.peer, BorderLayout.SOUTH)
}