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