src/Tools/jEdit/src/session_dockable.scala
changeset 44609 6ec4a5eb2fc0
parent 44335 156be0e43336
child 44613 a3255c85327b
equal deleted inserted replaced
44608:76c2e3ddc183 44609:6ec4a5eb2fc0
     8 
     8 
     9 
     9 
    10 import isabelle._
    10 import isabelle._
    11 
    11 
    12 import scala.actors.Actor._
    12 import scala.actors.Actor._
    13 import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
    13 import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
       
    14   ScrollPane, TabbedPane, Component, Swing}
    14 import scala.swing.event.{ButtonClicked, SelectionChanged}
    15 import scala.swing.event.{ButtonClicked, SelectionChanged}
    15 
    16 
    16 import java.lang.System
    17 import java.lang.System
    17 import java.awt.BorderLayout
    18 import java.awt.BorderLayout
       
    19 import javax.swing.JList
    18 import javax.swing.border.{BevelBorder, SoftBevelBorder}
    20 import javax.swing.border.{BevelBorder, SoftBevelBorder}
    19 
    21 
    20 import org.gjt.sp.jedit.View
    22 import org.gjt.sp.jedit.View
    21 
    23 
    22 
    24 
    25   /* main tabs */
    27   /* main tabs */
    26 
    28 
    27   private val readme = new HTML_Panel("SansSerif", 14)
    29   private val readme = new HTML_Panel("SansSerif", 14)
    28   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    30   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    29 
    31 
       
    32   val status = new ListView(Nil: List[String])
       
    33   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
       
    34   status.selection.intervalMode = ListView.IntervalMode.Single
       
    35 
    30   private val syslog = new TextArea(Isabelle.session.syslog())
    36   private val syslog = new TextArea(Isabelle.session.syslog())
    31 
    37 
    32   private val tabs = new TabbedPane {
    38   private val tabs = new TabbedPane {
    33     pages += new TabbedPane.Page("README", Component.wrap(readme))
    39     pages += new TabbedPane.Page("README", Component.wrap(readme))
    34     pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
    40     pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
       
    41     pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
    35 
    42 
    36     selection.index =
    43     selection.index =
    37     {
    44     {
    38       val index = Isabelle.Int_Property("session-panel.selection", 0)
    45       val index = Isabelle.Int_Property("session-panel.selection", 0)
    39       if (index >= pages.length) 0 else index
    46       if (index >= pages.length) 0 else index
    62 
    69 
    63   private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
    70   private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
    64   add(controls.peer, BorderLayout.NORTH)
    71   add(controls.peer, BorderLayout.NORTH)
    65 
    72 
    66 
    73 
       
    74   /* component state -- owned by Swing thread */
       
    75 
       
    76   private var nodes: Set[String] = Set.empty
       
    77 
       
    78   private def handle_changed(changed_nodes: Set[String])
       
    79   {
       
    80     Swing_Thread.now {
       
    81       val nodes1 = nodes ++ changed_nodes
       
    82       if (nodes1 != nodes) {
       
    83         nodes = nodes1
       
    84         status.listData = Library.sort_strings(nodes.toList)
       
    85       }
       
    86     }
       
    87   }
       
    88 
       
    89 
    67   /* main actor */
    90   /* main actor */
    68 
    91 
    69   private val main_actor = actor {
    92   private val main_actor = actor {
    70     loop {
    93     loop {
    71       react {
    94       react {
    81             }
   104             }
    82 
   105 
    83         case phase: Session.Phase =>
   106         case phase: Session.Phase =>
    84           Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
   107           Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    85 
   108 
       
   109         case changed: Session.Commands_Changed => handle_changed(changed.nodes)
       
   110 
    86         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
   111         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    87       }
   112       }
    88     }
   113     }
    89   }
   114   }
    90 
   115 
    91   override def init() {
   116   override def init() {
    92     Isabelle.session.raw_messages += main_actor
   117     Isabelle.session.raw_messages += main_actor
    93     Isabelle.session.phase_changed += main_actor
   118     Isabelle.session.phase_changed += main_actor
       
   119     Isabelle.session.commands_changed += main_actor
    94   }
   120   }
    95 
   121 
    96   override def exit() {
   122   override def exit() {
    97     Isabelle.session.raw_messages -= main_actor
   123     Isabelle.session.raw_messages -= main_actor
    98     Isabelle.session.phase_changed -= main_actor
   124     Isabelle.session.phase_changed -= main_actor
       
   125     Isabelle.session.commands_changed -= main_actor
    99   }
   126   }
   100 }
   127 }