src/Tools/jEdit/src/theories_dockable.scala
author wenzelm
Mon Apr 07 21:23:02 2014 +0200 (2014-04-07)
changeset 56457 eea4bbe15745
parent 56407 8e7ebc4b30f1
child 56599 c4424d8c890f
permissions -rw-r--r--
tuned signature -- prefer static type Document.Node.Name;
     1 /*  Title:      Tools/jEdit/src/theories_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for theories managed by prover.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.actors.Actor._
    13 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
    14   ScrollPane, Component, CheckBox, BorderPanel}
    15 import scala.swing.event.{MouseClicked, MouseMoved}
    16 
    17 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
    18 import javax.swing.{JList, BorderFactory, UIManager}
    19 import javax.swing.border.{BevelBorder, SoftBevelBorder}
    20 
    21 import org.gjt.sp.jedit.{View, jEdit}
    22 
    23 
    24 class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
    25 {
    26   /* status */
    27 
    28   private val status = new ListView(Nil: List[Document.Node.Name]) {
    29     background =
    30     {
    31       // enforce default value
    32       val c = UIManager.getDefaults.getColor("Panel.background")
    33       new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
    34     }
    35     listenTo(mouse.clicks)
    36     listenTo(mouse.moves)
    37     reactions += {
    38       case MouseClicked(_, point, _, clicks, _) =>
    39         val index = peer.locationToIndex(point)
    40         if (index >= 0) {
    41           if (in_checkbox(peer.indexToLocation(index), point)) {
    42             if (clicks == 1) {
    43               for {
    44                 buffer <- JEdit_Lib.jedit_buffer(listData(index))
    45                 model <- PIDE.document_model(buffer)
    46               } model.node_required = !model.node_required
    47             }
    48           }
    49           else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node)
    50         }
    51       case MouseMoved(_, point, _) =>
    52         val index = peer.locationToIndex(point)
    53         if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
    54           tooltip = "Mark as required for continuous checking"
    55         else
    56           tooltip = null
    57     }
    58   }
    59   status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
    60   status.peer.setVisibleRowCount(0)
    61   status.selection.intervalMode = ListView.IntervalMode.Single
    62 
    63   set_content(new ScrollPane(status))
    64 
    65 
    66   /* controls */
    67 
    68   def phase_text(phase: Session.Phase): String =
    69     "Prover: " + Library.lowercase(phase.toString)
    70 
    71   private val session_phase = new Label(phase_text(PIDE.session.phase))
    72   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    73   session_phase.tooltip = "Status of prover session"
    74 
    75   private def handle_phase(phase: Session.Phase)
    76   {
    77     Swing_Thread.require()
    78     session_phase.text = " " + phase_text(phase) + " "
    79   }
    80 
    81   private val continuous_checking = new Isabelle.Continuous_Checking
    82   continuous_checking.focusable = false
    83 
    84   private val logic = Isabelle_Logic.logic_selector(true)
    85 
    86   private val controls =
    87     new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
    88   add(controls.peer, BorderLayout.NORTH)
    89 
    90 
    91   /* component state -- owned by Swing thread */
    92 
    93   private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
    94   private var nodes_required: Set[Document.Node.Name] = Set.empty
    95 
    96   private def update_nodes_required()
    97   {
    98     nodes_required = Set.empty
    99     for {
   100       buffer <- JEdit_Lib.jedit_buffers
   101       model <- PIDE.document_model(buffer)
   102       if model.node_required
   103     } nodes_required += model.node_name
   104   }
   105   update_nodes_required()
   106 
   107   private def in_checkbox(loc0: Point, p: Point): Boolean =
   108     Node_Renderer_Component != null &&
   109       (Node_Renderer_Component.checkbox_geometry match {
   110         case Some((loc, size)) =>
   111           loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
   112           loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
   113         case None => false
   114       })
   115 
   116   private object Node_Renderer_Component extends BorderPanel
   117   {
   118     opaque = true
   119     border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
   120 
   121     var node_name = Document.Node.Name.empty
   122 
   123     var checkbox_geometry: Option[(Point, Dimension)] = None
   124     val checkbox = new CheckBox {
   125       opaque = false
   126       override def paintComponent(gfx: Graphics2D)
   127       {
   128         super.paintComponent(gfx)
   129         if (location != null && size != null)
   130           checkbox_geometry = Some((location, size))
   131       }
   132     }
   133 
   134     val label = new Label {
   135       background = view.getTextArea.getPainter.getBackground
   136       foreground = view.getTextArea.getPainter.getForeground
   137       border =
   138         BorderFactory.createCompoundBorder(
   139           BorderFactory.createLineBorder(foreground, 1),
   140           BorderFactory.createEmptyBorder(1, 1, 1, 1))
   141       opaque = false
   142       xAlignment = Alignment.Leading
   143 
   144       override def paintComponent(gfx: Graphics2D)
   145       {
   146         def paint_segment(x: Int, w: Int, color: Color)
   147         {
   148           gfx.setColor(color)
   149           gfx.fillRect(x, 0, w, size.height)
   150         }
   151 
   152         paint_segment(0, size.width, background)
   153         nodes_status.get(node_name) match {
   154           case Some(st) if st.total > 0 =>
   155             val segments =
   156               List(
   157                 (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
   158                 (st.running, PIDE.options.color_value("running_color")),
   159                 (st.warned, PIDE.options.color_value("warning_color")),
   160                 (st.failed, PIDE.options.color_value("error_color"))
   161               ).filter(_._1 > 0)
   162 
   163             ((size.width - 1) /: segments)({ case (last, (n, color)) =>
   164               val w = (n * ((size.width - 2) - segments.length) / st.total) max 4
   165               paint_segment(last - w, w, color)
   166               last - w - 1
   167             })
   168 
   169           case _ =>
   170             paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
   171         }
   172         super.paintComponent(gfx)
   173       }
   174     }
   175 
   176     layout(checkbox) = BorderPanel.Position.West
   177     layout(label) = BorderPanel.Position.Center
   178   }
   179 
   180   private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
   181   {
   182     def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
   183       name: Document.Node.Name, index: Int): Component =
   184     {
   185       val component = Node_Renderer_Component
   186       component.node_name = name
   187       component.checkbox.selected = nodes_required.contains(name)
   188       component.label.text = name.theory
   189       component
   190     }
   191   }
   192   status.renderer = new Node_Renderer
   193 
   194   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   195   {
   196     Swing_Thread.require()
   197 
   198     val snapshot = PIDE.session.snapshot()
   199 
   200     val iterator =
   201       (restriction match {
   202         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   203         case None => snapshot.version.nodes.iterator
   204       }).filter(_._1.is_theory)
   205     val nodes_status1 =
   206       (nodes_status /: iterator)({ case (status, (name, node)) =>
   207           if (PIDE.resources.loaded_theories(name.theory)) status
   208           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   209 
   210     if (nodes_status != nodes_status1) {
   211       nodes_status = nodes_status1
   212       status.listData =
   213         snapshot.version.nodes.topological_order.filter(
   214           (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
   215     }
   216   }
   217 
   218 
   219   /* main actor */
   220 
   221   private val main_actor = actor {
   222     loop {
   223       react {
   224         case phase: Session.Phase =>
   225           Swing_Thread.later { handle_phase(phase) }
   226 
   227         case _: Session.Global_Options =>
   228           Swing_Thread.later {
   229             continuous_checking.load()
   230             logic.load ()
   231             update_nodes_required()
   232             status.repaint()
   233           }
   234 
   235         case changed: Session.Commands_Changed =>
   236           Swing_Thread.later { handle_update(Some(changed.nodes)) }
   237 
   238         case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
   239       }
   240     }
   241   }
   242 
   243   override def init()
   244   {
   245     PIDE.session.phase_changed += main_actor
   246     PIDE.session.global_options += main_actor
   247     PIDE.session.commands_changed += main_actor
   248 
   249     handle_phase(PIDE.session.phase)
   250     handle_update()
   251   }
   252 
   253   override def exit()
   254   {
   255     PIDE.session.phase_changed -= main_actor
   256     PIDE.session.global_options -= main_actor
   257     PIDE.session.commands_changed -= main_actor
   258   }
   259 }