1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue May 29 21:48:05 2012 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue May 29 22:24:31 2012 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    "src/readme_dockable.scala"
     1.5    "src/scala_console.scala"
     1.6    "src/session_dockable.scala"
     1.7 +  "src/syslog_dockable.scala"
     1.8    "src/text_area_painter.scala"
     1.9    "src/text_overview.scala"
    1.10    "src/token_markup.scala"

     2.1 --- a/src/Tools/jEdit/src/Isabelle.props	Tue May 29 21:48:05 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Tue May 29 22:24:31 2012 +0200
     2.3 @@ -50,12 +50,13 @@
     2.4  
     2.5  #menu actions
     2.6  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
     2.7 -plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel
     2.8 +plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
     2.9  isabelle.session-panel.label=Prover Session panel
    2.10  isabelle.output-panel.label=Output panel
    2.11  isabelle.raw-output-panel.label=Raw Output panel
    2.12  isabelle.protocol-panel.label=Protocol panel
    2.13  isabelle.readme-panel.label=README panel
    2.14 +isabelle.syslog-panel.label=Syslog panel
    2.15  
    2.16  #dockables
    2.17  isabelle-session.title=Prover Session
    2.18 @@ -63,6 +64,7 @@
    2.19  isabelle-raw-output.title=Raw Output
    2.20  isabelle-protocol.title=Protocol
    2.21  isabelle-readme.title=README
    2.22 +isabelle-syslog.title=Syslog
    2.23  
    2.24  #SideKick
    2.25  sidekick.parser.isabelle.label=Isabelle

     3.1 --- a/src/Tools/jEdit/src/actions.xml	Tue May 29 21:48:05 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/actions.xml	Tue May 29 22:24:31 2012 +0200
     3.3 @@ -7,6 +7,11 @@
     3.4  			wm.addDockableWindow("isabelle-session");
     3.5  		</CODE>
     3.6  	</ACTION>
     3.7 +	<ACTION NAME="isabelle.syslog-panel">
     3.8 +		<CODE>
     3.9 +			wm.addDockableWindow("isabelle-syslog");
    3.10 +		</CODE>
    3.11 +	</ACTION>
    3.12  	<ACTION NAME="isabelle.readme-panel">
    3.13  		<CODE>
    3.14  			wm.addDockableWindow("isabelle-readme");

     4.1 --- a/src/Tools/jEdit/src/dockables.xml	Tue May 29 21:48:05 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/dockables.xml	Tue May 29 22:24:31 2012 +0200
     4.3 @@ -5,6 +5,9 @@
     4.4  	<DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
     4.5  		new isabelle.jedit.Session_Dockable(view, position);
     4.6  	</DOCKABLE>
     4.7 +	<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
     4.8 +		new isabelle.jedit.Syslog_Dockable(view, position);
     4.9 +	</DOCKABLE>
    4.10  	<DOCKABLE NAME="isabelle-readme" MOVABLE="TRUE">
    4.11  		new isabelle.jedit.README_Dockable(view, position);
    4.12  	</DOCKABLE>

     5.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue May 29 21:48:05 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue May 29 22:24:31 2012 +0200
     5.3 @@ -10,8 +10,7 @@
     5.4  import isabelle._
     5.5  
     5.6  import scala.actors.Actor._
     5.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     5.8 -  ScrollPane, TabbedPane, Component, Swing}
     5.9 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, Component}
    5.10  import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
    5.11  
    5.12  import java.lang.System
    5.13 @@ -24,9 +23,9 @@
    5.14  
    5.15  class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
    5.16  {
    5.17 -  /* main tabs */
    5.18 +  /* status */
    5.19  
    5.20 -  val status = new ListView(Nil: List[Document.Node.Name]) {
    5.21 +  private val status = new ListView(Nil: List[Document.Node.Name]) {
    5.22      listenTo(mouse.clicks)
    5.23      reactions += {
    5.24        case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    5.25 @@ -37,30 +36,12 @@
    5.26    status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    5.27    status.selection.intervalMode = ListView.IntervalMode.Single
    5.28  
    5.29 -  private val syslog = new TextArea(Isabelle.session.current_syslog())
    5.30 -
    5.31 -  private val tabs = new TabbedPane {
    5.32 -    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
    5.33 -    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
    5.34 -
    5.35 -    selection.index =
    5.36 -    {
    5.37 -      val index = Isabelle.Int_Property("session-panel.selection", 0)
    5.38 -      if (index >= pages.length) 0 else index
    5.39 -    }
    5.40 -    listenTo(selection)
    5.41 -    reactions += {
    5.42 -      case SelectionChanged(_) =>
    5.43 -        Isabelle.Int_Property("session-panel.selection") = selection.index
    5.44 -    }
    5.45 -  }
    5.46 -
    5.47 -  set_content(tabs)
    5.48 +  set_content(status)
    5.49  
    5.50  
    5.51    /* controls */
    5.52  
    5.53 -  val session_phase = new Label(Isabelle.session.phase.toString)
    5.54 +  private val session_phase = new Label(Isabelle.session.phase.toString)
    5.55    session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    5.56    session_phase.tooltip = "Prover status"
    5.57  
    5.58 @@ -171,13 +152,6 @@
    5.59    private val main_actor = actor {
    5.60      loop {
    5.61        react {
    5.62 -        case output: Isabelle_Process.Output =>
    5.63 -          if (output.is_syslog)
    5.64 -            Swing_Thread.later {
    5.65 -              val text = Isabelle.session.current_syslog()
    5.66 -              if (text != syslog.text) syslog.text = text
    5.67 -            }
    5.68 -
    5.69          case phase: Session.Phase => handle_phase(phase)
    5.70  
    5.71          case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
    5.72 @@ -189,20 +163,13 @@
    5.73  
    5.74    override def init()
    5.75    {
    5.76 -    Isabelle.session.syslog_messages += main_actor
    5.77 -    Isabelle.session.phase_changed += main_actor
    5.78 -    handle_phase(Isabelle.session.phase)
    5.79 -    Isabelle.session.commands_changed += main_actor
    5.80 -    handle_update()
    5.81 +    Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
    5.82 +    Isabelle.session.commands_changed += main_actor; handle_update()
    5.83    }
    5.84  
    5.85    override def exit()
    5.86    {
    5.87 -    Isabelle.session.syslog_messages -= main_actor
    5.88      Isabelle.session.phase_changed -= main_actor
    5.89      Isabelle.session.commands_changed -= main_actor
    5.90    }
    5.91 -
    5.92 -  handle_phase(Isabelle.session.phase)
    5.93 -  handle_update()
    5.94  }

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Tue May 29 22:24:31 2012 +0200
     6.3 @@ -0,0 +1,60 @@
     6.4 +/*  Title:      Tools/jEdit/src/syslog_dockable.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Dockable window for syslog.
     6.8 +*/
     6.9 +
    6.10 +package isabelle.jedit
    6.11 +
    6.12 +
    6.13 +import isabelle._
    6.14 +
    6.15 +import scala.actors.Actor._
    6.16 +import scala.swing.TextArea
    6.17 +
    6.18 +import java.lang.System
    6.19 +
    6.20 +import org.gjt.sp.jedit.View
    6.21 +
    6.22 +
    6.23 +class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
    6.24 +{
    6.25 +  /* GUI components */
    6.26 +
    6.27 +  private val syslog = new TextArea()
    6.28 +
    6.29 +  private def update_syslog()
    6.30 +  {
    6.31 +    Swing_Thread.later {
    6.32 +      val text = Isabelle.session.current_syslog()
    6.33 +      if (text != syslog.text) syslog.text = text
    6.34 +    }
    6.35 +  }
    6.36 +
    6.37 +  set_content(syslog)
    6.38 +
    6.39 +
    6.40 +  /* main actor */
    6.41 +
    6.42 +  private val main_actor = actor {
    6.43 +    loop {
    6.44 +      react {
    6.45 +        case output: Isabelle_Process.Output =>
    6.46 +          if (output.is_syslog) update_syslog()
    6.47 +
    6.48 +        case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    6.49 +      }
    6.50 +    }
    6.51 +  }
    6.52 +
    6.53 +  override def init()
    6.54 +  {
    6.55 +    Isabelle.session.syslog_messages += main_actor
    6.56 +    update_syslog()
    6.57 +  }
    6.58 +
    6.59 +  override def exit()
    6.60 +  {
    6.61 +    Isabelle.session.syslog_messages -= main_actor
    6.62 +  }
    6.63 +}