src/Tools/jEdit/src/query_operation.scala
author wenzelm
Mon Aug 05 23:57:29 2013 +0200 (2013-08-05 ago)
changeset 52874 91032244e4ca
parent 52865 02a7e7180ee5
child 52875 e2d5c3ff5c3f
permissions -rw-r--r--
query process animation;
wenzelm@52865
     1
/*  Title:      Tools/jEdit/src/query_operation.scala
wenzelm@52865
     2
    Author:     Makarius
wenzelm@52865
     3
wenzelm@52865
     4
One-shot query operations via asynchronous print functions and temporary
wenzelm@52865
     5
document overlay.
wenzelm@52865
     6
*/
wenzelm@52865
     7
wenzelm@52865
     8
package isabelle.jedit
wenzelm@52865
     9
wenzelm@52865
    10
wenzelm@52865
    11
import isabelle._
wenzelm@52865
    12
wenzelm@52865
    13
import scala.actors.Actor._
wenzelm@52874
    14
import scala.swing.Label
wenzelm@52865
    15
wenzelm@52865
    16
import org.gjt.sp.jedit.View
wenzelm@52874
    17
import org.gjt.sp.jedit.gui.AnimatedIcon
wenzelm@52865
    18
wenzelm@52865
    19
wenzelm@52865
    20
object Query_Operation
wenzelm@52865
    21
{
wenzelm@52865
    22
  def apply(
wenzelm@52865
    23
      view: View,
wenzelm@52865
    24
      name: String,
wenzelm@52865
    25
      consume: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
wenzelm@52865
    26
    new Query_Operation(view, name, consume)
wenzelm@52865
    27
}
wenzelm@52865
    28
wenzelm@52865
    29
final class Query_Operation private(
wenzelm@52865
    30
  view: View,
wenzelm@52865
    31
  operation_name: String,
wenzelm@52865
    32
  consume_result: (Document.Snapshot, Command.Results, XML.Body) => Unit)
wenzelm@52865
    33
{
wenzelm@52865
    34
  private val instance = Document_ID.make().toString
wenzelm@52865
    35
wenzelm@52865
    36
wenzelm@52874
    37
  /* status animation */
wenzelm@52874
    38
wenzelm@52874
    39
  private val passive_icon =
wenzelm@52874
    40
    JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage
wenzelm@52874
    41
  private val active_icons =
wenzelm@52874
    42
    space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
wenzelm@52874
    43
      JEdit_Lib.load_image_icon(name).getImage)
wenzelm@52874
    44
wenzelm@52874
    45
  val animation = new Label
wenzelm@52874
    46
  val animation_icon = new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer)
wenzelm@52874
    47
  animation.icon = animation_icon
wenzelm@52874
    48
wenzelm@52874
    49
wenzelm@52865
    50
  /* implicit state -- owned by Swing thread */
wenzelm@52865
    51
wenzelm@52865
    52
  private var current_location: Option[Command] = None
wenzelm@52865
    53
  private var current_query: List[String] = Nil
wenzelm@52865
    54
  private var current_result = false
wenzelm@52865
    55
  private var current_snapshot = Document.State.init.snapshot()
wenzelm@52865
    56
  private var current_state = Command.empty.init_state
wenzelm@52865
    57
  private var current_output: List[XML.Tree] = Nil
wenzelm@52865
    58
wenzelm@52865
    59
  private def remove_overlay()
wenzelm@52865
    60
  {
wenzelm@52865
    61
    Swing_Thread.require()
wenzelm@52865
    62
wenzelm@52865
    63
    for {
wenzelm@52865
    64
      command <- current_location
wenzelm@52865
    65
      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
wenzelm@52865
    66
      model <- PIDE.document_model(buffer)
wenzelm@52865
    67
    } model.remove_overlay(command, operation_name, instance :: current_query)
wenzelm@52865
    68
  }
wenzelm@52865
    69
wenzelm@52865
    70
  private def handle_result()
wenzelm@52865
    71
  {
wenzelm@52865
    72
    Swing_Thread.require()
wenzelm@52865
    73
wenzelm@52865
    74
    val (new_snapshot, new_state) =
wenzelm@52865
    75
      Document_View(view.getTextArea) match {
wenzelm@52865
    76
        case Some(doc_view) =>
wenzelm@52865
    77
          val snapshot = doc_view.model.snapshot()
wenzelm@52865
    78
          current_location match {
wenzelm@52865
    79
            case Some(cmd) =>
wenzelm@52865
    80
              (snapshot, snapshot.state.command_state(snapshot.version, cmd))
wenzelm@52865
    81
            case None =>
wenzelm@52865
    82
              (Document.State.init.snapshot(), Command.empty.init_state)
wenzelm@52865
    83
          }
wenzelm@52865
    84
        case None => (current_snapshot, current_state)
wenzelm@52865
    85
      }
wenzelm@52865
    86
wenzelm@52865
    87
    val new_output =
wenzelm@52865
    88
      (for {
wenzelm@52865
    89
        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
wenzelm@52865
    90
          new_state.results.entries
wenzelm@52865
    91
        if props.contains((Markup.INSTANCE, instance))
wenzelm@52865
    92
      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
wenzelm@52865
    93
wenzelm@52865
    94
    if (new_output != current_output)
wenzelm@52865
    95
      consume_result(new_snapshot, new_state.results, new_output)
wenzelm@52865
    96
wenzelm@52865
    97
    if (!new_output.isEmpty) {
wenzelm@52865
    98
      current_result = true
wenzelm@52874
    99
      animation_icon.stop
wenzelm@52865
   100
      remove_overlay()
wenzelm@52865
   101
      PIDE.flush_buffers()
wenzelm@52865
   102
    }
wenzelm@52865
   103
wenzelm@52865
   104
    current_snapshot = new_snapshot
wenzelm@52865
   105
    current_state = new_state
wenzelm@52865
   106
    current_output = new_output
wenzelm@52865
   107
  }
wenzelm@52865
   108
wenzelm@52865
   109
  def apply_query(query: List[String])
wenzelm@52865
   110
  {
wenzelm@52865
   111
    Swing_Thread.require()
wenzelm@52865
   112
wenzelm@52865
   113
    Document_View(view.getTextArea) match {
wenzelm@52865
   114
      case Some(doc_view) =>
wenzelm@52865
   115
        val snapshot = doc_view.model.snapshot()
wenzelm@52865
   116
        remove_overlay()
wenzelm@52865
   117
        current_location = None
wenzelm@52865
   118
        current_query = Nil
wenzelm@52865
   119
        current_result = false
wenzelm@52874
   120
        animation_icon.start
wenzelm@52865
   121
        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
wenzelm@52865
   122
          case Some(command) =>
wenzelm@52865
   123
            current_location = Some(command)
wenzelm@52865
   124
            current_query = query
wenzelm@52865
   125
            doc_view.model.insert_overlay(command, operation_name, instance :: query)
wenzelm@52865
   126
          case None =>
wenzelm@52865
   127
        }
wenzelm@52865
   128
        PIDE.flush_buffers()
wenzelm@52865
   129
      case None =>
wenzelm@52865
   130
    }
wenzelm@52865
   131
  }
wenzelm@52865
   132
wenzelm@52865
   133
  def locate_query()
wenzelm@52865
   134
  {
wenzelm@52865
   135
    Swing_Thread.require()
wenzelm@52865
   136
wenzelm@52865
   137
    current_location match {
wenzelm@52865
   138
      case Some(command) =>
wenzelm@52865
   139
        val snapshot = PIDE.session.snapshot(command.node_name)
wenzelm@52865
   140
        val commands = snapshot.node.commands
wenzelm@52865
   141
        if (commands.contains(command)) {
wenzelm@52865
   142
          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
wenzelm@52865
   143
          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@52865
   144
          Hyperlink(command.node_name.node, line, column).follow(view)
wenzelm@52865
   145
        }
wenzelm@52865
   146
      case None =>
wenzelm@52865
   147
    }
wenzelm@52865
   148
  }
wenzelm@52865
   149
wenzelm@52865
   150
wenzelm@52865
   151
  /* main actor */
wenzelm@52865
   152
wenzelm@52865
   153
  private val main_actor = actor {
wenzelm@52865
   154
    loop {
wenzelm@52865
   155
      react {
wenzelm@52865
   156
        case changed: Session.Commands_Changed =>
wenzelm@52865
   157
          current_location match {
wenzelm@52865
   158
            case Some(command) if !current_result && changed.commands.contains(command) =>
wenzelm@52865
   159
              Swing_Thread.later { handle_result() }
wenzelm@52865
   160
            case _ =>
wenzelm@52865
   161
          }
wenzelm@52865
   162
        case bad =>
wenzelm@52865
   163
          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
wenzelm@52865
   164
      }
wenzelm@52865
   165
    }
wenzelm@52865
   166
  }
wenzelm@52865
   167
wenzelm@52865
   168
  def activate() { PIDE.session.commands_changed += main_actor }
wenzelm@52865
   169
  def deactivate() { PIDE.session.commands_changed -= main_actor }
wenzelm@52865
   170
}