more content for Session_Dockable;
authorwenzelm
Wed Sep 22 16:04:20 2010 +0200 (2010-09-22 ago)
changeset 39591a43a723753e6
parent 39590 2258769f112f
child 39592 5638fe4f0843
more content for Session_Dockable;
src/Pure/General/markup.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Tools/jEdit/dist-template/README.html
src/Tools/jEdit/src/jedit/session_dockable.scala
     1.1 --- a/src/Pure/General/markup.scala	Wed Sep 22 16:03:57 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Wed Sep 22 16:04:20 2010 +0200
     1.3 @@ -247,7 +247,7 @@
     1.4  
     1.5    val BAD = "bad"
     1.6  
     1.7 -  val Ready = Markup("ready", Nil)
     1.8 +  val READY = "ready"
     1.9  
    1.10  
    1.11    /* system data */
     2.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 22 16:03:57 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Sep 22 16:04:20 2010 +0200
     2.3 @@ -182,7 +182,7 @@
     2.4      val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
     2.5      val _ = init_message out_stream;
     2.6      val _ = Keyword.status ();
     2.7 -    val _ = Output.status (Markup.markup Markup.ready "");
     2.8 +    val _ = Output.status (Markup.markup Markup.ready "Prover ready");
     2.9    in loop in_stream end));
    2.10  
    2.11  end;
     3.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 22 16:03:57 2010 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 22 16:04:20 2010 +0200
     3.3 @@ -44,7 +44,11 @@
     3.4      def is_system = kind == Markup.SYSTEM
     3.5      def is_status = kind == Markup.STATUS
     3.6      def is_report = kind == Markup.REPORT
     3.7 -    def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
     3.8 +    def is_ready = is_status && {
     3.9 +      body match {
    3.10 +        case List(XML.Elem(Markup(Markup.READY, _), _)) => true
    3.11 +        case _ => false
    3.12 +      }}
    3.13  
    3.14      override def toString: String =
    3.15      {
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/dist-template/README.html	Wed Sep 22 16:04:20 2010 +0200
     4.3 @@ -0,0 +1,24 @@
     4.4 +<?xml version="1.0" encoding="ISO-8859-1" ?>
     4.5 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
     4.6 +<html xmlns="http://www.w3.org/1999/xhtml">
     4.7 +
     4.8 +<head>
     4.9 +<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
    4.10 +<title>Notes on Isabelle/Isar Prover IDE</title>
    4.11 +</head>
    4.12 +
    4.13 +<body>
    4.14 +
    4.15 +<h1>Notes on Isabelle/Isar Prover IDE</h1>
    4.16 +
    4.17 +<ul>
    4.18 +
    4.19 +<li>FIXME</li>
    4.20 +
    4.21 +<li>FIXME</li>
    4.22 +
    4.23 +</ul>
    4.24 +
    4.25 +</body>
    4.26 +</html>
    4.27 +
     5.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Sep 22 16:03:57 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Sep 22 16:04:20 2010 +0200
     5.3 @@ -10,16 +10,27 @@
     5.4  import isabelle._
     5.5  
     5.6  import scala.actors.Actor._
     5.7 -import scala.swing.{TextArea, ScrollPane}
     5.8 +import scala.swing.{TextArea, ScrollPane, TabbedPane, Component}
     5.9  
    5.10  import org.gjt.sp.jedit.View
    5.11  
    5.12  
    5.13  class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
    5.14  {
    5.15 -  private val text_area = new TextArea
    5.16 -  text_area.editable = false
    5.17 -  set_content(new ScrollPane(text_area))
    5.18 +  /* main tabs */
    5.19 +
    5.20 +  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
    5.21 +  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
    5.22 +
    5.23 +  private val syslog = new TextArea
    5.24 +  syslog.editable = false
    5.25 +
    5.26 +  private val tabs = new TabbedPane {
    5.27 +    pages += new TabbedPane.Page("README", Component.wrap(readme))
    5.28 +    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
    5.29 +  }
    5.30 +
    5.31 +  set_content(tabs)
    5.32  
    5.33  
    5.34    /* main actor */
    5.35 @@ -28,8 +39,8 @@
    5.36      loop {
    5.37        react {
    5.38          case result: Isabelle_Process.Result =>
    5.39 -          if (result.is_init || result.is_exit || result.is_system)
    5.40 -            Swing_Thread.now { text_area.append(XML.content(result.message).mkString + "\n") }
    5.41 +          if (result.is_init || result.is_exit || result.is_system || result.is_ready)
    5.42 +            Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") }
    5.43  
    5.44          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    5.45        }