# HG changeset patch # User wenzelm # Date 1405954692 -7200 # Node ID 2f7d91242b999af7ad47de40cf4f7f631c26b106 # Parent b73d74d0e42871c4e5ae11a4f23317f0a5572d8a proper Swing buttons instead of active areas within text (by Lars Hupel); diff -r b73d74d0e428 -r 2f7d91242b99 src/Pure/Tools/simplifier_trace.scala --- 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) diff -r b73d74d0e428 -r 2f7d91242b99 src/Tools/jEdit/src/active.scala --- 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) diff -r b73d74d0e428 -r 2f7d91242b99 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- 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) }