src/Tools/jEdit/src/theories_dockable.scala
changeset 50299 f70b3712040f
parent 50250 267bd685a69f
child 50300 6658097758ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Nov 30 21:30:24 2012 +0100
     1.3 @@ -0,0 +1,179 @@
     1.4 +/*  Title:      Tools/jEdit/src/theories_dockable.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Dockable window for theories managed by prover.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import scala.actors.Actor._
    1.16 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
    1.17 +import scala.swing.event.{ButtonClicked, MouseClicked}
    1.18 +
    1.19 +import java.lang.System
    1.20 +import java.awt.{BorderLayout, Graphics2D, Insets}
    1.21 +import javax.swing.{JList, BorderFactory}
    1.22 +import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.23 +
    1.24 +import org.gjt.sp.jedit.{View, jEdit}
    1.25 +
    1.26 +
    1.27 +class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
    1.28 +{
    1.29 +  /* status */
    1.30 +
    1.31 +  private val status = new ListView(Nil: List[Document.Node.Name]) {
    1.32 +    listenTo(mouse.clicks)
    1.33 +    reactions += {
    1.34 +      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    1.35 +        val index = peer.locationToIndex(point)
    1.36 +        if (index >= 0) jEdit.openFile(view, listData(index).node)
    1.37 +    }
    1.38 +  }
    1.39 +  status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
    1.40 +  status.peer.setVisibleRowCount(0)
    1.41 +  status.selection.intervalMode = ListView.IntervalMode.Single
    1.42 +
    1.43 +  set_content(new ScrollPane(status))
    1.44 +
    1.45 +
    1.46 +  /* controls */
    1.47 +
    1.48 +  def phase_text(phase: Session.Phase): String =
    1.49 +    "Prover: " + Library.lowercase(phase.toString)
    1.50 +
    1.51 +  private val session_phase = new Label(phase_text(PIDE.session.phase))
    1.52 +  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    1.53 +  session_phase.tooltip = "Status of prover session"
    1.54 +
    1.55 +  private def handle_phase(phase: Session.Phase)
    1.56 +  {
    1.57 +    Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
    1.58 +  }
    1.59 +
    1.60 +  private val cancel = new Button("Cancel") {
    1.61 +    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
    1.62 +  }
    1.63 +  cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
    1.64 +
    1.65 +  private val check = new Button("Check") {
    1.66 +    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
    1.67 +  }
    1.68 +  check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
    1.69 +
    1.70 +  private val logic = Isabelle_Logic.logic_selector(true)
    1.71 +
    1.72 +  private val controls =
    1.73 +    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
    1.74 +  add(controls.peer, BorderLayout.NORTH)
    1.75 +
    1.76 +
    1.77 +  /* component state -- owned by Swing thread */
    1.78 +
    1.79 +  private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
    1.80 +
    1.81 +  private object Node_Renderer_Component extends Label
    1.82 +  {
    1.83 +    opaque = false
    1.84 +    xAlignment = Alignment.Leading
    1.85 +    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.86 +
    1.87 +    var node_name = Document.Node.Name.empty
    1.88 +    override def paintComponent(gfx: Graphics2D)
    1.89 +    {
    1.90 +      nodes_status.get(node_name) match {
    1.91 +        case Some(st) if st.total > 0 =>
    1.92 +          val size = peer.getSize()
    1.93 +          val insets = border.getBorderInsets(this.peer)
    1.94 +          val w = size.width - insets.left - insets.right
    1.95 +          val h = size.height - insets.top - insets.bottom
    1.96 +          var end = size.width - insets.right
    1.97 +          for {
    1.98 +            (n, color) <- List(
    1.99 +              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
   1.100 +              (st.running, PIDE.options.color_value("running_color")),
   1.101 +              (st.warned, PIDE.options.color_value("warning_color")),
   1.102 +              (st.failed, PIDE.options.color_value("error_color"))) }
   1.103 +          {
   1.104 +            gfx.setColor(color)
   1.105 +            val v = (n * w / st.total) max (if (n > 0) 2 else 0)
   1.106 +            gfx.fillRect(end - v, insets.top, v, h)
   1.107 +            end -= v
   1.108 +          }
   1.109 +        case _ =>
   1.110 +      }
   1.111 +      super.paintComponent(gfx)
   1.112 +    }
   1.113 +  }
   1.114 +
   1.115 +  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
   1.116 +  {
   1.117 +    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
   1.118 +      name: Document.Node.Name, index: Int): Component =
   1.119 +    {
   1.120 +      val component = Node_Renderer_Component
   1.121 +      component.node_name = name
   1.122 +      component.text = name.theory
   1.123 +      component
   1.124 +    }
   1.125 +  }
   1.126 +  status.renderer = new Node_Renderer
   1.127 +
   1.128 +  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   1.129 +  {
   1.130 +    Swing_Thread.now {
   1.131 +      val snapshot = PIDE.session.snapshot()
   1.132 +
   1.133 +      val iterator =
   1.134 +        restriction match {
   1.135 +          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   1.136 +          case None => snapshot.version.nodes.entries
   1.137 +        }
   1.138 +      val nodes_status1 =
   1.139 +        (nodes_status /: iterator)({ case (status, (name, node)) =>
   1.140 +            if (PIDE.thy_load.loaded_theories(name.theory)) status
   1.141 +            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   1.142 +
   1.143 +      if (nodes_status != nodes_status1) {
   1.144 +        nodes_status = nodes_status1
   1.145 +        status.listData =
   1.146 +          snapshot.version.nodes.topological_order.filter(
   1.147 +            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
   1.148 +      }
   1.149 +    }
   1.150 +  }
   1.151 +
   1.152 +
   1.153 +  /* main actor */
   1.154 +
   1.155 +  private val main_actor = actor {
   1.156 +    loop {
   1.157 +      react {
   1.158 +        case phase: Session.Phase => handle_phase(phase)
   1.159 +
   1.160 +        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
   1.161 +
   1.162 +        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
   1.163 +
   1.164 +        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
   1.165 +      }
   1.166 +    }
   1.167 +  }
   1.168 +
   1.169 +  override def init()
   1.170 +  {
   1.171 +    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
   1.172 +    PIDE.session.global_options += main_actor
   1.173 +    PIDE.session.commands_changed += main_actor; handle_update()
   1.174 +  }
   1.175 +
   1.176 +  override def exit()
   1.177 +  {
   1.178 +    PIDE.session.phase_changed -= main_actor
   1.179 +    PIDE.session.global_options -= main_actor
   1.180 +    PIDE.session.commands_changed -= main_actor
   1.181 +  }
   1.182 +}