refined output panel: more value-oriented approach to update and caret focus;
authorwenzelm
Fri Sep 14 20:49:54 2012 +0200 (2012-09-14)
changeset 49359c1262d7389fb
parent 49358 0fa351b1bd14
child 49360 37c1297aa562
refined output panel: more value-oriented approach to update and caret focus;
src/Pure/PIDE/command.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/output_dockable.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Sep 14 18:12:41 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Sep 14 20:49:54 2012 +0200
     1.3 @@ -102,6 +102,8 @@
     1.4    def unparsed(source: String): Command =
     1.5      Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
     1.6  
     1.7 +  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
     1.8 +
     1.9  
    1.10    /* perspective */
    1.11  
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 18:12:41 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 20:49:54 2012 +0200
     2.3 @@ -274,12 +274,6 @@
     2.4  
     2.5    /* caret handling */
     2.6  
     2.7 -  def selected_command(): Option[Command] =
     2.8 -  {
     2.9 -    Swing_Thread.require()
    2.10 -    model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
    2.11 -  }
    2.12 -
    2.13    private val delay_caret_update =
    2.14      Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
    2.15        session.caret_focus.event(Session.Caret_Focus)
     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 14 18:12:41 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 14 20:49:54 2012 +0200
     3.3 @@ -25,6 +25,18 @@
     3.4  {
     3.5    Swing_Thread.require()
     3.6  
     3.7 +
     3.8 +  /* component state -- owned by Swing thread */
     3.9 +
    3.10 +  private var zoom_factor = 100
    3.11 +  private var show_tracing = false
    3.12 +  private var do_update = true
    3.13 +  private var current_state = Command.empty.empty_state
    3.14 +  private var current_body: XML.Body = Nil
    3.15 +
    3.16 +
    3.17 +  /* HTML panel */
    3.18 +
    3.19    private val html_panel =
    3.20      new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    3.21    {
    3.22 @@ -36,23 +48,20 @@
    3.23          Document_View(view.getTextArea) match {
    3.24            case Some(doc_view) =>
    3.25              doc_view.robust_body() {
    3.26 -              current_command match {
    3.27 -                case Some(cmd) =>
    3.28 -                  val model = doc_view.model
    3.29 -                  val buffer = model.buffer
    3.30 -                  val snapshot = model.snapshot()
    3.31 -                  snapshot.node.command_start(cmd) match {
    3.32 -                    case Some(start) if !snapshot.is_outdated =>
    3.33 -                      val text = Pretty.string_of(sendback)
    3.34 -                      try {
    3.35 -                        buffer.beginCompoundEdit()
    3.36 -                        buffer.remove(start, cmd.proper_range.length)
    3.37 -                        buffer.insert(start, text)
    3.38 -                      }
    3.39 -                      finally { buffer.endCompoundEdit() }
    3.40 -                    case _ =>
    3.41 +              val cmd = current_state.command
    3.42 +              val model = doc_view.model
    3.43 +              val buffer = model.buffer
    3.44 +              val snapshot = model.snapshot()
    3.45 +              snapshot.node.command_start(cmd) match {
    3.46 +                case Some(start) if !snapshot.is_outdated =>
    3.47 +                  val text = Pretty.string_of(sendback)
    3.48 +                  try {
    3.49 +                    buffer.beginCompoundEdit()
    3.50 +                    buffer.remove(start, cmd.proper_range.length)
    3.51 +                    buffer.insert(start, text)
    3.52                    }
    3.53 -                case None =>
    3.54 +                  finally { buffer.endCompoundEdit() }
    3.55 +                case _ =>
    3.56                }
    3.57              }
    3.58            case None =>
    3.59 @@ -63,55 +72,45 @@
    3.60    set_content(html_panel)
    3.61  
    3.62  
    3.63 -  /* component state -- owned by Swing thread */
    3.64 -
    3.65 -  private var zoom_factor = 100
    3.66 -  private var show_tracing = false
    3.67 -  private var follow_caret = true
    3.68 -  private var current_command: Option[Command] = None
    3.69 -
    3.70 -
    3.71    private def handle_resize()
    3.72    {
    3.73 -    Swing_Thread.now {
    3.74 -      html_panel.resize(Isabelle.font_family(),
    3.75 -        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    3.76 -    }
    3.77 +    Swing_Thread.require()
    3.78 +
    3.79 +    html_panel.resize(Isabelle.font_family(),
    3.80 +      scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    3.81    }
    3.82  
    3.83 -  private def handle_perspective(): Boolean =
    3.84 -    Swing_Thread.now {
    3.85 -      Document_View(view.getTextArea) match {
    3.86 -        case Some(doc_view) =>
    3.87 -          val cmd = doc_view.selected_command()
    3.88 -          if (current_command == cmd) false
    3.89 -          else { current_command = cmd; true }
    3.90 -        case None => false
    3.91 -      }
    3.92 -    }
    3.93 -
    3.94 -  private def handle_update(restriction: Option[Set[Command]] = None)
    3.95 +  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    3.96    {
    3.97 -    Swing_Thread.now {
    3.98 -      if (follow_caret) handle_perspective()
    3.99 -      Document_View(view.getTextArea) match {
   3.100 -        case Some(doc_view) =>
   3.101 -          current_command match {
   3.102 -            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
   3.103 -              val snapshot = doc_view.model.snapshot()
   3.104 -              val filtered_results =
   3.105 -                snapshot.state.command_state(snapshot.version, cmd).results.iterator
   3.106 -                  .map(_._2).filter(
   3.107 -                  { // FIXME not scalable
   3.108 -                    case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
   3.109 -                    case _ => true
   3.110 -                  }).toList
   3.111 -              html_panel.render(filtered_results)
   3.112 -            case _ => html_panel.render(Nil)
   3.113 -          }
   3.114 -        case None => html_panel.render(Nil)
   3.115 +    Swing_Thread.require()
   3.116 +
   3.117 +    val new_state =
   3.118 +      if (follow) {
   3.119 +        Document_View(view.getTextArea) match {
   3.120 +          case Some(doc_view) =>
   3.121 +            val snapshot = doc_view.model.snapshot()
   3.122 +            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
   3.123 +              case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
   3.124 +              case None => Command.empty.empty_state
   3.125 +            }
   3.126 +          case None => Command.empty.empty_state
   3.127 +        }
   3.128        }
   3.129 -    }
   3.130 +      else current_state
   3.131 +
   3.132 +    val new_body =
   3.133 +      if (!restriction.isDefined || restriction.get.contains(new_state.command))
   3.134 +        new_state.results.iterator.map(_._2).filter(
   3.135 +        { // FIXME not scalable
   3.136 +          case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
   3.137 +          case _ => true
   3.138 +        }).toList
   3.139 +      else current_body
   3.140 +
   3.141 +    if (new_body != current_body) html_panel.render(new_body)
   3.142 +
   3.143 +    current_state = new_state
   3.144 +    current_body = new_body
   3.145    }
   3.146  
   3.147  
   3.148 @@ -120,9 +119,12 @@
   3.149    private val main_actor = actor {
   3.150      loop {
   3.151        react {
   3.152 -        case Session.Global_Settings => handle_resize()
   3.153 -        case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
   3.154 -        case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
   3.155 +        case Session.Global_Settings =>
   3.156 +          Swing_Thread.later { handle_resize() }
   3.157 +        case changed: Session.Commands_Changed =>
   3.158 +          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
   3.159 +        case Session.Caret_Focus =>
   3.160 +          Swing_Thread.later { handle_update(do_update, None) }
   3.161          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
   3.162        }
   3.163      }
   3.164 @@ -130,14 +132,18 @@
   3.165  
   3.166    override def init()
   3.167    {
   3.168 +    Swing_Thread.require()
   3.169 +
   3.170      Isabelle.session.global_settings += main_actor
   3.171      Isabelle.session.commands_changed += main_actor
   3.172      Isabelle.session.caret_focus += main_actor
   3.173 -    handle_update()
   3.174 +    handle_update(true, None)
   3.175    }
   3.176  
   3.177    override def exit()
   3.178    {
   3.179 +    Swing_Thread.require()
   3.180 +
   3.181      Isabelle.session.global_settings -= main_actor
   3.182      Isabelle.session.commands_changed -= main_actor
   3.183      Isabelle.session.caret_focus -= main_actor
   3.184 @@ -162,19 +168,21 @@
   3.185    zoom.tooltip = "Zoom factor for basic font size"
   3.186  
   3.187    private val tracing = new CheckBox("Tracing") {
   3.188 -    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
   3.189 +    reactions += {
   3.190 +      case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }
   3.191    }
   3.192    tracing.selected = show_tracing
   3.193    tracing.tooltip = "Indicate output of tracing messages"
   3.194  
   3.195    private val auto_update = new CheckBox("Auto update") {
   3.196 -    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
   3.197 +    reactions += {
   3.198 +      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
   3.199    }
   3.200 -  auto_update.selected = follow_caret
   3.201 +  auto_update.selected = do_update
   3.202    auto_update.tooltip = "Indicate automatic update following cursor movement"
   3.203  
   3.204    private val update = new Button("Update") {
   3.205 -    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
   3.206 +    reactions += { case ButtonClicked(_) => handle_update(true, None) }
   3.207    }
   3.208    update.tooltip = "Update display according to the command at cursor position"
   3.209