--- 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 */
--- 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;
--- 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 =
{
--- /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 @@
+<?xml version="1.0" encoding="ISO-8859-1" ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<title>Notes on Isabelle/Isar Prover IDE</title>
+</head>
+
+<body>
+
+<h1>Notes on Isabelle/Isar Prover IDE</h1>
+
+<ul>
+
+<li>FIXME</li>
+
+<li>FIXME</li>
+
+</ul>
+
+</body>
+</html>
+
--- 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)
}