# HG changeset patch
# User wenzelm
# Date 1285164260 -7200
# Node ID a43a723753e6b353e4f6ae12eecc332a20cdae7b
# Parent 2258769f112f2c235a03cbbadd4e911c63c2355c
more content for Session_Dockable;
diff -r 2258769f112f -r a43a723753e6 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala Wed Sep 22 16:03:57 2010 +0200
+++ b/src/Pure/General/markup.scala Wed Sep 22 16:04:20 2010 +0200
@@ -247,7 +247,7 @@
val BAD = "bad"
- val Ready = Markup("ready", Nil)
+ val READY = "ready"
/* system data */
diff -r 2258769f112f -r a43a723753e6 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML Wed Sep 22 16:03:57 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Sep 22 16:04:20 2010 +0200
@@ -182,7 +182,7 @@
val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
val _ = init_message out_stream;
val _ = Keyword.status ();
- val _ = Output.status (Markup.markup Markup.ready "");
+ val _ = Output.status (Markup.markup Markup.ready "Prover ready");
in loop in_stream end));
end;
diff -r 2258769f112f -r a43a723753e6 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala Wed Sep 22 16:03:57 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Wed Sep 22 16:04:20 2010 +0200
@@ -44,7 +44,11 @@
def is_system = kind == Markup.SYSTEM
def is_status = kind == Markup.STATUS
def is_report = kind == Markup.REPORT
- def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
+ def is_ready = is_status && {
+ body match {
+ case List(XML.Elem(Markup(Markup.READY, _), _)) => true
+ case _ => false
+ }}
override def toString: String =
{
diff -r 2258769f112f -r a43a723753e6 src/Tools/jEdit/dist-template/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/README.html Wed Sep 22 16:04:20 2010 +0200
@@ -0,0 +1,24 @@
+
+
+
+
+
+
+Notes on Isabelle/Isar Prover IDE
+
+
+
+
+Notes on Isabelle/Isar Prover IDE
+
+
+
+
+
+
diff -r 2258769f112f -r a43a723753e6 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 22 16:03:57 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 22 16:04:20 2010 +0200
@@ -10,16 +10,27 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{TextArea, ScrollPane}
+import scala.swing.{TextArea, ScrollPane, TabbedPane, Component}
import org.gjt.sp.jedit.View
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
{
- private val text_area = new TextArea
- text_area.editable = false
- set_content(new ScrollPane(text_area))
+ /* main tabs */
+
+ private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
+ readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
+
+ private val syslog = new TextArea
+ syslog.editable = false
+
+ private val tabs = new TabbedPane {
+ pages += new TabbedPane.Page("README", Component.wrap(readme))
+ pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
+ }
+
+ set_content(tabs)
/* main actor */
@@ -28,8 +39,8 @@
loop {
react {
case result: Isabelle_Process.Result =>
- if (result.is_init || result.is_exit || result.is_system)
- Swing_Thread.now { text_area.append(XML.content(result.message).mkString + "\n") }
+ if (result.is_init || result.is_exit || result.is_system || result.is_ready)
+ Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") }
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
}