src/Tools/jEdit/src/theories_dockable.scala
changeset 75393 87ebf5a50283
parent 73987 fc363a3b690a
child 75829 b8a4f9b1eed6
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
    18 import javax.swing.border.{BevelBorder, SoftBevelBorder}
    18 import javax.swing.border.{BevelBorder, SoftBevelBorder}
    19 
    19 
    20 import org.gjt.sp.jedit.{View, jEdit}
    20 import org.gjt.sp.jedit.{View, jEdit}
    21 
    21 
    22 
    22 
    23 class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
    23 class Theories_Dockable(view: View, position: String) extends Dockable(view, position) {
    24 {
       
    25   /* status */
    24   /* status */
    26 
    25 
    27   private val status = new ListView(List.empty[Document.Node.Name]) {
    26   private val status = new ListView(List.empty[Document.Node.Name]) {
    28     background =
    27     background = {
    29     {
       
    30       // enforce default value
    28       // enforce default value
    31       val c = UIManager.getDefaults.getColor("Panel.background")
    29       val c = UIManager.getDefaults.getColor("Panel.background")
    32       new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
    30       new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
    33     }
    31     }
    34     listenTo(mouse.clicks)
    32     listenTo(mouse.clicks)
    70 
    68 
    71   private val session_phase = new Label(phase_text(PIDE.session.phase))
    69   private val session_phase = new Label(phase_text(PIDE.session.phase))
    72   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    70   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    73   session_phase.tooltip = "Status of prover session"
    71   session_phase.tooltip = "Status of prover session"
    74 
    72 
    75   private def handle_phase(phase: Session.Phase): Unit =
    73   private def handle_phase(phase: Session.Phase): Unit = {
    76   {
       
    77     GUI_Thread.require {}
    74     GUI_Thread.require {}
    78     session_phase.text = " " + phase_text(phase) + " "
    75     session_phase.text = " " + phase_text(phase) + " "
    79   }
    76   }
    80 
    77 
    81   private val purge = new Button("Purge") {
    78   private val purge = new Button("Purge") {
   112 
   109 
   113   private def in_label(loc0: Point, p: Point): Boolean =
   110   private def in_label(loc0: Point, p: Point): Boolean =
   114     Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
   111     Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
   115 
   112 
   116 
   113 
   117   private object Node_Renderer_Component extends BorderPanel
   114   private object Node_Renderer_Component extends BorderPanel {
   118   {
       
   119     opaque = true
   115     opaque = true
   120     border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
   116     border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
   121 
   117 
   122     var node_name = Document.Node.Name.empty
   118     var node_name = Document.Node.Name.empty
   123 
   119 
   124     var checkbox_geometry: Option[(Point, Dimension)] = None
   120     var checkbox_geometry: Option[(Point, Dimension)] = None
   125     val checkbox = new CheckBox {
   121     val checkbox = new CheckBox {
   126       opaque = false
   122       opaque = false
   127       override def paintComponent(gfx: Graphics2D): Unit =
   123       override def paintComponent(gfx: Graphics2D): Unit = {
   128       {
       
   129         super.paintComponent(gfx)
   124         super.paintComponent(gfx)
   130         if (location != null && size != null)
   125         if (location != null && size != null)
   131           checkbox_geometry = Some((location, size))
   126           checkbox_geometry = Some((location, size))
   132       }
   127       }
   133     }
   128     }
   137       background = view.getTextArea.getPainter.getBackground
   132       background = view.getTextArea.getPainter.getBackground
   138       foreground = view.getTextArea.getPainter.getForeground
   133       foreground = view.getTextArea.getPainter.getForeground
   139       opaque = false
   134       opaque = false
   140       xAlignment = Alignment.Leading
   135       xAlignment = Alignment.Leading
   141 
   136 
   142       override def paintComponent(gfx: Graphics2D): Unit =
   137       override def paintComponent(gfx: Graphics2D): Unit = {
   143       {
   138         def paint_segment(x: Int, w: Int, color: Color): Unit = {
   144         def paint_segment(x: Int, w: Int, color: Color): Unit =
       
   145         {
       
   146           gfx.setColor(color)
   139           gfx.setColor(color)
   147           gfx.fillRect(x, 0, w, size.height)
   140           gfx.fillRect(x, 0, w, size.height)
   148         }
   141         }
   149 
   142 
   150         paint_segment(0, size.width, background)
   143         paint_segment(0, size.width, background)
   173         if (location != null && size != null)
   166         if (location != null && size != null)
   174           label_geometry = Some((location, size))
   167           label_geometry = Some((location, size))
   175       }
   168       }
   176     }
   169     }
   177 
   170 
   178     def label_border(name: Document.Node.Name): Unit =
   171     def label_border(name: Document.Node.Name): Unit = {
   179     {
       
   180       val st = nodes_status.overall_node_status(name)
   172       val st = nodes_status.overall_node_status(name)
   181       val color =
   173       val color =
   182         st match {
   174         st match {
   183           case Document_Status.Overall_Node_Status.ok =>
   175           case Document_Status.Overall_Node_Status.ok =>
   184             PIDE.options.color_value("ok_color")
   176             PIDE.options.color_value("ok_color")
   197 
   189 
   198     layout(checkbox) = BorderPanel.Position.West
   190     layout(checkbox) = BorderPanel.Position.West
   199     layout(label) = BorderPanel.Position.Center
   191     layout(label) = BorderPanel.Position.Center
   200   }
   192   }
   201 
   193 
   202   private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
   194   private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
   203   {
   195     def componentFor(
   204     def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean,
   196       list: ListView[_ <: isabelle.Document.Node.Name],
   205       focused: Boolean, name: Document.Node.Name, index: Int): Component =
   197       isSelected: Boolean,
   206     {
   198       focused: Boolean,
       
   199       name: Document.Node.Name,
       
   200       index: Int
       
   201     ): Component = {
   207       val component = Node_Renderer_Component
   202       val component = Node_Renderer_Component
   208       component.node_name = name
   203       component.node_name = name
   209       component.checkbox.selected = nodes_required.contains(name)
   204       component.checkbox.selected = nodes_required.contains(name)
   210       component.label_border(name)
   205       component.label_border(name)
   211       component.label.text = name.theory_base_name
   206       component.label.text = name.theory_base_name
   213     }
   208     }
   214   }
   209   }
   215   status.renderer = new Node_Renderer
   210   status.renderer = new Node_Renderer
   216 
   211 
   217   private def handle_update(
   212   private def handle_update(
   218     domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit =
   213     domain: Option[Set[Document.Node.Name]] = None,
   219   {
   214     trim: Boolean = false
       
   215   ): Unit = {
   220     GUI_Thread.require {}
   216     GUI_Thread.require {}
   221 
   217 
   222     val snapshot = PIDE.session.snapshot()
   218     val snapshot = PIDE.session.snapshot()
   223 
   219 
   224     val (nodes_status_changed, nodes_status1) =
   220     val (nodes_status_changed, nodes_status1) =
   253 
   249 
   254       case changed: Session.Commands_Changed =>
   250       case changed: Session.Commands_Changed =>
   255         GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
   251         GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
   256     }
   252     }
   257 
   253 
   258   override def init(): Unit =
   254   override def init(): Unit = {
   259   {
       
   260     PIDE.session.phase_changed += main
   255     PIDE.session.phase_changed += main
   261     PIDE.session.global_options += main
   256     PIDE.session.global_options += main
   262     PIDE.session.commands_changed += main
   257     PIDE.session.commands_changed += main
   263 
   258 
   264     handle_phase(PIDE.session.phase)
   259     handle_phase(PIDE.session.phase)
   265     handle_update()
   260     handle_update()
   266   }
   261   }
   267 
   262 
   268   override def exit(): Unit =
   263   override def exit(): Unit = {
   269   {
       
   270     PIDE.session.phase_changed -= main
   264     PIDE.session.phase_changed -= main
   271     PIDE.session.global_options -= main
   265     PIDE.session.global_options -= main
   272     PIDE.session.commands_changed -= main
   266     PIDE.session.commands_changed -= main
   273   }
   267   }
   274 }
   268 }