proper Swing buttons instead of active areas within text (by Lars Hupel);
authorwenzelm
Mon Jul 21 16:58:12 2014 +0200 (2014-07-21)
changeset 575932f7d91242b99
parent 57592 b73d74d0e428
child 57594 037f3b251df5
proper Swing buttons instead of active areas within text (by Lars Hupel);
src/Pure/Tools/simplifier_trace.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
     1.1 --- a/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 16:49:06 2014 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 16:58:12 2014 +0200
     1.3 @@ -65,7 +65,6 @@
     1.4        val continue_passive = Answer("continue_passive", "Continue (without asking)")
     1.5        val continue_disable = Answer("continue_disable", "Continue (without any trace)")
     1.6  
     1.7 -      val default = skip
     1.8        val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
     1.9      }
    1.10  
    1.11 @@ -74,27 +73,12 @@
    1.12        val exit = Answer("exit", "Exit")
    1.13        val redo = Answer("redo", "Redo")
    1.14  
    1.15 -      val default = exit
    1.16        val all = List(redo, exit)
    1.17      }
    1.18    }
    1.19  
    1.20    val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
    1.21  
    1.22 -  object Active
    1.23 -  {
    1.24 -    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
    1.25 -      tree match {
    1.26 -        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
    1.27 -          (props, props) match {
    1.28 -            case (Markup.Serial(serial), Markup.Name(name)) =>
    1.29 -              all_answers.find(_.name == name).map((serial, _))
    1.30 -            case _ => None
    1.31 -          }
    1.32 -        case _ => None
    1.33 -      }
    1.34 -  }
    1.35 -
    1.36  
    1.37    /* GUI interaction */
    1.38  
    1.39 @@ -110,7 +94,7 @@
    1.40    private object Clear_Memory
    1.41    case class Reply(session: Session, serial: Long, answer: Answer)
    1.42  
    1.43 -  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
    1.44 +  case class Question(data: Item.Data, answers: List[Answer])
    1.45  
    1.46    case class Context(
    1.47      last_serial: Long = 0L,
    1.48 @@ -207,7 +191,7 @@
    1.49                          case Some(answer) if data.memory =>
    1.50                            do_reply(session, serial, answer)
    1.51                          case _ =>
    1.52 -                          new_context += Question(data, Answer.step.all, Answer.step.default)
    1.53 +                          new_context += Question(data, Answer.step.all)
    1.54                        }
    1.55  
    1.56                      case Markup.SIMP_TRACE_HINT =>
    1.57 @@ -215,11 +199,10 @@
    1.58                          case Success(false) =>
    1.59                            results.get(data.parent) match {
    1.60                              case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
    1.61 -                              new_context +=
    1.62 -                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
    1.63 +                              new_context += Question(data, Answer.hint_fail.all)
    1.64                              case _ =>
    1.65                                // unknown, better send a default reply
    1.66 -                              do_reply(session, data.serial, Answer.hint_fail.default)
    1.67 +                              do_reply(session, data.serial, Answer.hint_fail.exit)
    1.68                            }
    1.69                          case _ =>
    1.70                        }
    1.71 @@ -263,8 +246,7 @@
    1.72              // current results.
    1.73  
    1.74              val items =
    1.75 -              (for { (_, Item(_, data)) <- results.iterator }
    1.76 -                yield data).toList
    1.77 +              results.iterator.collect { case (_, Item(_, data)) => data }.toList
    1.78  
    1.79              slot.fulfill(Trace(items))
    1.80  
    1.81 @@ -281,7 +263,7 @@
    1.82  
    1.83            case Reply(session, serial, answer) =>
    1.84              find_question(serial) match {
    1.85 -              case Some((id, Question(data, _, _))) =>
    1.86 +              case Some((id, Question(data, _))) =>
    1.87                  if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
    1.88                  {
    1.89                    val index = Index.of_data(data)
     2.1 --- a/src/Tools/jEdit/src/active.scala	Mon Jul 21 16:49:06 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/active.scala	Mon Jul 21 16:58:12 2014 +0200
     2.3 @@ -60,9 +60,6 @@
     2.4                  }
     2.5                  text_area.requestFocus
     2.6  
     2.7 -              case Simplifier_Trace.Active(serial, answer) =>
     2.8 -                Simplifier_Trace.send_reply(PIDE.session, serial, answer)
     2.9 -
    2.10                case Protocol.Dialog(id, serial, result) =>
    2.11                  model.session.dialog_result(id, serial, result)
    2.12  
     3.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 16:49:06 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 16:58:12 2014 +0200
     3.3 @@ -29,50 +29,38 @@
     3.4    private var current_results = Command.Results.empty
     3.5    private var current_id = 0L
     3.6    private var do_update = true
     3.7 -  private var do_auto_reply = false
     3.8  
     3.9  
    3.10    private val text_area = new Pretty_Text_Area(view)
    3.11    set_content(text_area)
    3.12  
    3.13 -  private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
    3.14 +  private def update_contents()
    3.15    {
    3.16 -    val data = question.data
    3.17  
    3.18 -    def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
    3.19 -      XML.Wrapped_Elem(
    3.20 -        Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
    3.21 -        Nil,
    3.22 -        List(XML.Text(answer.string))
    3.23 -      )
    3.24 +    Swing_Thread.require {}
    3.25  
    3.26 -    def make_block(body: XML.Body): XML.Body =
    3.27 -      List(Pretty.Block(0, body))
    3.28 +    val snapshot = current_snapshot
    3.29 +    val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
    3.30  
    3.31 -    val all = Pretty.separate(
    3.32 -      XML.Text(data.text) ::
    3.33 -      data.content :::
    3.34 -      make_block(Library.separate(XML.Text(", "), question.answers map make_button))
    3.35 -    )
    3.36 -
    3.37 -    XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
    3.38 -  }
    3.39 +    answers.contents.clear()
    3.40 +    context.questions.values.toList match {
    3.41 +      case q :: _ =>
    3.42 +        val data = q.data
    3.43 +        val content = Pretty.separate(XML.Text(data.text) :: data.content)
    3.44 +        text_area.update(snapshot, Command.Results.empty, content)
    3.45 +        q.answers.foreach { answer =>
    3.46 +          answers.contents += new Button(answer.string) {
    3.47 +            reactions += {
    3.48 +              case ButtonClicked(_) =>
    3.49 +                Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
    3.50 +            }
    3.51 +          }
    3.52 +        }
    3.53 +      case Nil =>
    3.54 +        text_area.update(snapshot, Command.Results.empty, Nil)
    3.55 +    }
    3.56  
    3.57 -  private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
    3.58 -  {
    3.59 -    Swing_Thread.require {}
    3.60 -    val questions = context.questions.values
    3.61 -    if (do_auto_reply && !questions.isEmpty)
    3.62 -    {
    3.63 -      questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
    3.64 -      handle_update(do_update)
    3.65 -    }
    3.66 -    else
    3.67 -    {
    3.68 -      val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
    3.69 -      text_area.update(snapshot, Command.Results.empty, contents)
    3.70 -      do_paint()
    3.71 -    }
    3.72 +    do_paint()
    3.73    }
    3.74  
    3.75    private def show_trace()
    3.76 @@ -88,14 +76,6 @@
    3.77      }
    3.78    }
    3.79  
    3.80 -  private def update_contents()
    3.81 -  {
    3.82 -    set_context(
    3.83 -      current_snapshot,
    3.84 -      Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
    3.85 -    )
    3.86 -  }
    3.87 -
    3.88    private def handle_resize()
    3.89    {
    3.90      do_paint()
    3.91 @@ -195,15 +175,6 @@
    3.92        }
    3.93      },
    3.94      new Separator(Orientation.Vertical),
    3.95 -    new CheckBox("Auto reply") {
    3.96 -      selected = do_auto_reply
    3.97 -      reactions += {
    3.98 -        case ButtonClicked(_) =>
    3.99 -          do_auto_reply = this.selected
   3.100 -          handle_update(do_update)
   3.101 -      }
   3.102 -    },
   3.103 -    new Separator(Orientation.Vertical),
   3.104      new Button("Show trace") {
   3.105        reactions += {
   3.106          case ButtonClicked(_) =>
   3.107 @@ -218,5 +189,8 @@
   3.108      }
   3.109    )
   3.110  
   3.111 +  private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
   3.112 +
   3.113    add(controls.peer, BorderLayout.NORTH)
   3.114 +  add(answers.peer, BorderLayout.SOUTH)
   3.115  }