tuned -- more explicit type Status.Value;
authorwenzelm
Tue Aug 06 21:34:58 2013 +0200 (2013-08-06 ago)
changeset 528779a26ec5739dd
parent 52876 78989972d5b8
child 52878 8069c8b9335e
tuned -- more explicit type Status.Value;
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/query_operation.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Aug 06 21:08:04 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Aug 06 21:34:58 2013 +0200
     1.3 @@ -245,8 +245,6 @@
     1.4    val FINISHED = "finished"
     1.5    val FAILED = "failed"
     1.6  
     1.7 -  val WAITING = "waiting"
     1.8 -
     1.9  
    1.10    /* interactive documents */
    1.11  
     2.1 --- a/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:08:04 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Tue Aug 06 21:34:58 2013 +0200
     2.3 @@ -34,36 +34,20 @@
     2.4    private val instance = Document_ID.make().toString
     2.5  
     2.6  
     2.7 -  /* animation */
     2.8 -
     2.9 -  private val passive_icon =
    2.10 -    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
    2.11 -  private val active_icons =
    2.12 -    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
    2.13 -      JEdit_Lib.load_image_icon(name).getImage)
    2.14 +  /* implicit state -- owned by Swing thread */
    2.15  
    2.16 -  val animation = new Label
    2.17 -  private val animation_icon =
    2.18 -    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
    2.19 -  animation.icon = animation_icon
    2.20 -
    2.21 -  private def animation_rate(rate: Int)
    2.22 +  private object Status extends Enumeration
    2.23    {
    2.24 -    animation_icon.stop
    2.25 -    if (rate > 0) {
    2.26 -      animation_icon.setRate(rate)
    2.27 -      animation_icon.start
    2.28 -    }
    2.29 +    val WAITING = Value("waiting")
    2.30 +    val RUNNING = Value("running")
    2.31 +    val FINISHED = Value("finished")
    2.32    }
    2.33  
    2.34 -
    2.35 -  /* implicit state -- owned by Swing thread */
    2.36 -
    2.37    private var current_location: Option[Command] = None
    2.38    private var current_query: List[String] = Nil
    2.39    private var current_update_pending = false
    2.40    private var current_output: List[XML.Tree] = Nil
    2.41 -  private var current_status = Markup.FINISHED
    2.42 +  private var current_status = Status.FINISHED
    2.43  
    2.44    private def reset_state()
    2.45    {
    2.46 @@ -71,7 +55,7 @@
    2.47      current_query = Nil
    2.48      current_update_pending = false
    2.49      current_output = Nil
    2.50 -    current_status = Markup.FINISHED
    2.51 +    current_status = Status.FINISHED
    2.52    }
    2.53  
    2.54    private def remove_overlay()
    2.55 @@ -85,7 +69,34 @@
    2.56      } model.remove_overlay(command, operation_name, instance :: current_query)
    2.57    }
    2.58  
    2.59 -  private def handle_update()
    2.60 +
    2.61 +  /* animation */
    2.62 +
    2.63 +  val animation = new Label
    2.64 +
    2.65 +  private val passive_icon =
    2.66 +    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
    2.67 +  private val active_icons =
    2.68 +    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
    2.69 +      JEdit_Lib.load_image_icon(name).getImage)
    2.70 +
    2.71 +  private val animation_icon =
    2.72 +    new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
    2.73 +  animation.icon = animation_icon
    2.74 +
    2.75 +  private def animation_update()
    2.76 +  {
    2.77 +    animation_icon.stop
    2.78 +    if (current_status != Status.FINISHED) {
    2.79 +      animation_icon.setRate(if (current_status == Status.RUNNING) 15 else 5)
    2.80 +      animation_icon.start
    2.81 +    }
    2.82 +  }
    2.83 +
    2.84 +
    2.85 +  /* content update */
    2.86 +
    2.87 +  private def content_update()
    2.88    {
    2.89      Swing_Thread.require()
    2.90  
    2.91 @@ -121,11 +132,13 @@
    2.92  
    2.93      /* status */
    2.94  
    2.95 -    def status(name: String): Option[String] =
    2.96 -      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => name })
    2.97 +    def get_status(name: String, status: Status.Value): Option[Status.Value] =
    2.98 +      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => status })
    2.99  
   2.100      val new_status =
   2.101 -      status(Markup.FINISHED) orElse status(Markup.RUNNING) getOrElse Markup.WAITING
   2.102 +      get_status(Markup.FINISHED, Status.FINISHED) orElse
   2.103 +      get_status(Markup.RUNNING, Status.RUNNING) getOrElse
   2.104 +      Status.WAITING
   2.105  
   2.106  
   2.107      /* state update */
   2.108 @@ -134,25 +147,26 @@
   2.109        if (snapshot.is_outdated)
   2.110          current_update_pending = true
   2.111        else {
   2.112 -        if (current_output != new_output)
   2.113 +        current_update_pending = false
   2.114 +        if (current_output != new_output) {
   2.115 +          current_output = new_output
   2.116            consume_result(snapshot, state.results, new_output)
   2.117 -        if (current_status != new_status)
   2.118 -          new_status match {
   2.119 -            case Markup.WAITING => animation_rate(5)
   2.120 -            case Markup.RUNNING => animation_rate(15)
   2.121 -            case Markup.FINISHED =>
   2.122 -              animation_rate(0)
   2.123 -              remove_overlay()
   2.124 -              PIDE.flush_buffers()
   2.125 -            case _ =>
   2.126 +        }
   2.127 +        if (current_status != new_status) {
   2.128 +          current_status = new_status
   2.129 +          animation_update()
   2.130 +          if (new_status == Status.FINISHED) {
   2.131 +            remove_overlay()
   2.132 +            PIDE.flush_buffers()
   2.133            }
   2.134 -        current_output = new_output
   2.135 -        current_status = new_status
   2.136 -        current_update_pending = false
   2.137 +        }
   2.138        }
   2.139      }
   2.140    }
   2.141  
   2.142 +
   2.143 +  /* apply query */
   2.144 +
   2.145    def apply_query(query: List[String])
   2.146    {
   2.147      Swing_Thread.require()
   2.148 @@ -162,21 +176,23 @@
   2.149          val snapshot = doc_view.model.snapshot()
   2.150          remove_overlay()
   2.151          reset_state()
   2.152 -        animation_rate(0)
   2.153          snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
   2.154            case Some(command) =>
   2.155              current_location = Some(command)
   2.156              current_query = query
   2.157 -            current_status = Markup.WAITING
   2.158 -            animation_rate(5)
   2.159 +            current_status = Status.WAITING
   2.160              doc_view.model.insert_overlay(command, operation_name, instance :: query)
   2.161            case None =>
   2.162          }
   2.163 +        animation_update()
   2.164          PIDE.flush_buffers()
   2.165        case None =>
   2.166      }
   2.167    }
   2.168  
   2.169 +
   2.170 +  /* locate query */
   2.171 +
   2.172    def locate_query()
   2.173    {
   2.174      Swing_Thread.require()
   2.175 @@ -205,8 +221,8 @@
   2.176            current_location match {
   2.177              case Some(command)
   2.178              if current_update_pending ||
   2.179 -              (current_status != Markup.FINISHED && changed.commands.contains(command)) =>
   2.180 -              Swing_Thread.later { handle_update() }
   2.181 +              (current_status != Status.FINISHED && changed.commands.contains(command)) =>
   2.182 +              Swing_Thread.later { content_update() }
   2.183              case _ =>
   2.184            }
   2.185          case bad =>