# HG changeset patch
# User wenzelm
# Date 1274777822 -7200
# Node ID d37b5a9bec146b6efd19b9e494e7c6a6889a2f68
# Parent  844d9842aec7977c3d923cf10cd1087074f1fab5# Parent  5e42e36a6693c903134fd49b6c175bfd24452577
merged

diff -r 844d9842aec7 -r d37b5a9bec14 etc/settings
--- a/etc/settings	Mon May 24 21:19:25 2010 +0100
+++ b/etc/settings	Tue May 25 10:57:02 2010 +0200
@@ -157,11 +157,14 @@
 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
 
 # The pdf file viewer
-if [ $(uname -s) = Darwin ]; then
-  PDF_VIEWER="open -W -n"
-else
-  PDF_VIEWER=xpdf
-fi
+case "$ISABELLE_PLATFORM" in
+  *-darwin)
+    PDF_VIEWER="open -W -n"
+    ;;
+  *)
+    PDF_VIEWER=xpdf
+    ;;
+esac
 #PDF_VIEWER=acroread
 #PDF_VIEWER=evince
 
@@ -192,6 +195,14 @@
 
 
 ###
+### Rendering information
+###
+
+ISABELLE_FONT_FAMILY="IsabelleText"
+ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
+
+
+###
 ### External reasoning tools
 ###
 
diff -r 844d9842aec7 -r d37b5a9bec14 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Mon May 24 21:19:25 2010 +0100
+++ b/lib/html/isabelle.css	Tue May 25 10:57:02 2010 +0200
@@ -26,7 +26,7 @@
 .tfree, tfree                 { color: #A020F0; }
 .tvar, tvar                   { color: #A020F0; }
 .free, free                   { color: blue; }
-.skolem, skolem               { color: #D2691E; font-weight: bold; }
+.skolem, skolem               { color: #D2691E; }
 .bound, bound                 { color: green; }
 .var, var                     { color: #00009B; }
 .numeral, numeral             { }
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/General/linear_set.scala	Tue May 25 10:57:02 2010 +0200
@@ -129,22 +129,26 @@
   def contains(elem: A): Boolean =
     !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
 
-  private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+  private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
     private var next_elem = start
     def hasNext = next_elem.isDefined
     def next =
       next_elem match {
         case Some(elem) =>
-          next_elem = rep.nexts.get(elem)
+          next_elem = which.get(elem)
           elem
         case None => throw new NoSuchElementException("next on empty iterator")
       }
   }
 
-  override def iterator: Iterator[A] = iterator_from(rep.start)
+  override def iterator: Iterator[A] = make_iterator(rep.start, rep.nexts)
 
   def iterator(elem: A): Iterator[A] =
-    if (contains(elem)) iterator_from(Some(elem))
+    if (contains(elem)) make_iterator(Some(elem), rep.nexts)
+    else throw new Linear_Set.Undefined(elem.toString)
+
+  def reverse_iterator(elem: A): Iterator[A] =
+    if (contains(elem)) make_iterator(Some(elem), rep.prevs)
     else throw new Linear_Set.Undefined(elem.toString)
 
   def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/PIDE/document.scala	Tue May 25 10:57:02 2010 +0200
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.annotation.tailrec
+
+
 object Document
 {
   /* command start positions */
@@ -80,27 +83,29 @@
 
     /* phase 2: recover command spans */
 
-    def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+    @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     {
-      // FIXME relative search!
       commands.iterator.find(is_unparsed) match {
         case Some(first_unparsed) =>
-          val prefix = commands.prev(first_unparsed)
-          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
-          val suffix = commands.next(body.last)
+          val first =
+            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+          val last =
+            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
+          val range =
+            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
 
-          val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
+          val sources = range.flatMap(_.span.map(_.source))
           val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
 
           val (before_edit, spans1) =
-            if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
-              (prefix, spans0.tail)
-            else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
+            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
+              (Some(first), spans0.tail)
+            else (commands.prev(first), spans0)
 
           val (after_edit, spans2) =
-            if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
-              (suffix, spans1.take(spans1.length - 1))
-            else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
+            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
+              (Some(last), spans1.take(spans1.length - 1))
+            else (commands.next(last), spans1)
 
           val inserted = spans2.map(span => new Command(session.create_id(), span))
           val new_commands =
@@ -114,23 +119,20 @@
 
     /* phase 3: resulting document edits */
 
-    val result = Library.timeit("text_edits") {
-      val commands0 = old_doc.commands
-      val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
-      val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
+    val commands0 = old_doc.commands
+    val commands1 = edit_text(edits, commands0)
+    val commands2 = parse_spans(commands1)
 
-      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
-      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+    val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+    val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
 
-      val doc_edits =
-        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
-        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+    val doc_edits =
+      removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+      inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
-      val former_states = old_doc.assignment.join -- removed_commands
+    val former_states = old_doc.assignment.join -- removed_commands
 
-      (doc_edits, new Document(new_id, commands2, former_states))
-    }
-    result
+    (doc_edits, new Document(new_id, commands2, former_states))
   }
 }
 
@@ -166,13 +168,11 @@
   def await_assignment { assignment.join }
 
   @volatile private var tmp_states = former_states
-  private val time0 = System.currentTimeMillis
 
   def assign_states(new_states: List[(Command, Command)])
   {
     assignment.fulfill(tmp_states ++ new_states)
     tmp_states = Map()
-    System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
   }
 
   def current_state(cmd: Command): State =
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/PIDE/state.scala	Tue May 25 10:57:02 2010 +0200
@@ -11,7 +11,7 @@
 class State(
   val command: Command,
   val status: Command.Status.Value,
-  val rev_results: List[XML.Tree],
+  val reverse_results: List[XML.Tree],
   val markup_root: Markup_Text)
 {
   def this(command: Command) =
@@ -21,15 +21,15 @@
   /* content */
 
   private def set_status(st: Command.Status.Value): State =
-    new State(command, st, rev_results, markup_root)
+    new State(command, st, reverse_results, markup_root)
 
   private def add_result(res: XML.Tree): State =
-    new State(command, status, res :: rev_results, markup_root)
+    new State(command, status, res :: reverse_results, markup_root)
 
   private def add_markup(node: Markup_Tree): State =
-    new State(command, status, rev_results, markup_root + node)
+    new State(command, status, reverse_results, markup_root + node)
 
-  lazy val results = rev_results.reverse
+  lazy val results = reverse_results.reverse
 
 
   /* markup */
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue May 25 10:57:02 2010 +0200
@@ -93,7 +93,7 @@
     if (value != "") value else error("Undefined environment variable: " + name)
   }
 
-  override def toString = getenv("ISABELLE_HOME")
+  override def toString = getenv_strict("ISABELLE_HOME")
 
 
 
@@ -164,10 +164,15 @@
 
   /* try_read */
 
-  def try_read(path: String): String =
+  def try_read(paths: Seq[String]): String =
   {
-    val file = platform_file(path)
-    if (file.isFile) Source.fromFile(file).mkString else ""
+    val buf = new StringBuilder
+    for {
+      path <- paths
+      file = platform_file(path) if file.isFile
+      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
+    } buf.append(c)
+    buf.toString
   }
 
 
@@ -303,7 +308,7 @@
   /* components */
 
   def components(): List[String] =
-    getenv("ISABELLE_COMPONENTS").split(":").toList
+    getenv_strict("ISABELLE_COMPONENTS").split(":").toList
 
 
   /* find logics */
@@ -324,17 +329,13 @@
 
   /* symbols */
 
-  private def read_symbols(path: String): List[String] =
-    Library.chunks(try_read(path)).map(_.toString).toList
-
   val symbols = new Symbol.Interpretation(
-    read_symbols("$ISABELLE_HOME/etc/symbols") :::
-    read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
+    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList).split("\n").toList)
 
 
   /* fonts */
 
-  val font_family = "IsabelleText"
+  val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
 
   def get_font(size: Int = 1, bold: Boolean = false): Font =
     new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
@@ -357,6 +358,7 @@
       val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
       ge.registerFont(font)
       // workaround strange problem with Apple's Java 1.6 font manager
+      // FIXME does not quite work!?
       if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
       if (!check_font()) error("Failed to install IsabelleText fonts")
     }
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/System/session.scala	Tue May 25 10:57:02 2010 +0200
@@ -36,6 +36,7 @@
 
   val global_settings = new Event_Bus[Session.Global_Settings.type]
   val raw_results = new Event_Bus[Isabelle_Process.Result]
+  val raw_output = new Event_Bus[Isabelle_Process.Result]
   val results = new Event_Bus[Command]
 
   val command_change = new Event_Bus[Command]
@@ -148,7 +149,9 @@
       }
       else if (result.kind == Isabelle_Process.Kind.EXIT)
         prover = null
-      else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
+      else if (result.is_raw)
+        raw_output.event(result)
+      else if (!result.is_system)   // FIXME syslog (!?)
         bad_result(result)
     }
 
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/System/session_manager.scala
--- a/src/Pure/System/session_manager.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/System/session_manager.scala	Tue May 25 10:57:02 2010 +0200
@@ -22,21 +22,21 @@
 
 
   // FIXME handle (potentially cyclic) directory graph
-  private def find_sessions(rev_prefix: List[String], rev_sessions: List[List[String]],
+  private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
     dir: File): List[List[String]] =
   {
-    val (rev_prefix1, rev_sessions1) =
+    val (reverse_prefix1, reverse_sessions1) =
       if (is_session_dir(dir)) {
         val name = dir.getName  // FIXME from root file
-        val rev_prefix1 = name :: rev_prefix
-        val rev_sessions1 = rev_prefix1.reverse :: rev_sessions
-        (rev_prefix1, rev_sessions1)
+        val reverse_prefix1 = name :: reverse_prefix
+        val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
+        (reverse_prefix1, reverse_sessions1)
       }
-      else (rev_prefix, rev_sessions)
+      else (reverse_prefix, reverse_sessions)
 
     val subdirs =
       dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
-    (rev_sessions1 /: subdirs)(find_sessions(rev_prefix1, _, _))
+    (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
   }
 
   def component_sessions(): List[List[String]] =
diff -r 844d9842aec7 -r d37b5a9bec14 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Pure/Thy/completion.scala	Tue May 25 10:57:02 2010 +0200
@@ -21,14 +21,14 @@
   {
     override val whiteSpace = "".r
 
-    def rev_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
-    def rev_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
+    def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
+    def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
     def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
 
     def read(in: CharSequence): Option[String] =
     {
-      val rev_in = new Library.Reverse(in)
-      parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
+      val reverse_in = new Library.Reverse(in)
+      parse((reverse_symbol | reverse_symb | word) ^^ (_.reverse), reverse_in) match {
         case Success(result, _) => Some(result)
         case _ => None
       }
@@ -86,8 +86,8 @@
   def complete(line: CharSequence): Option[(String, List[String])] =
   {
     abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
-      case abbrevs_lex.Success(rev_a, _) =>
-        val (word, c) = abbrevs_map(rev_a)
+      case abbrevs_lex.Success(reverse_a, _) =>
+        val (word, c) = abbrevs_map(reverse_a)
         Some(word, List(c))
       case _ =>
         Completion.Parse.read(line) match {
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/WWW_Find/lib/Tools/wwwfind
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Tue May 25 10:57:02 2010 +0200
@@ -35,12 +35,11 @@
 
 function checkplatform()
 {
-  PLAT=$(uname -s)
-  case "$PLAT" in
-    Linux)
+  case "$ISABELLE_PLATFORM" in
+    *-linux)
       ;;
     *)
-      fail "Platform $PLAT currently not supported by $PRG component."
+      fail "Platform $ISABELLE_PLATFORM currently not supported by $PRG component"
       ;;
   esac
 }
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/README_BUILD	Tue May 25 10:57:02 2010 +0200
@@ -88,3 +88,6 @@
 
 - Font.createFont mangles the font family of non-regular fonts,
   e.g. bold.
+
+- ToggleButton selected state is not rendered if window focus is lost,
+  which is probably a genuine feature of the Apple look-and-feel.
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Tue May 25 10:57:02 2010 +0200
@@ -1,6 +1,6 @@
 /* additional style file for Isabelle/jEdit output */
 
-pre.message { margin-top: 0.3ex; background-color: #F0F0F0; }
+.message { margin-top: 0.3ex; background-color: #F0F0F0; }
 
 .writeln { }
 .priority { }
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/dist-template/etc/settings
--- a/src/Tools/jEdit/dist-template/etc/settings	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/dist-template/etc/settings	Tue May 25 10:57:02 2010 +0200
@@ -6,6 +6,9 @@
 #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m $JEDIT_APPLE_PROPERTIES"
 JEDIT_OPTIONS="-reuseview -noserver -nobackground"
 
+JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
+
 ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
+
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Tue May 25 10:57:02 2010 +0200
@@ -31,13 +31,15 @@
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-raw-output isabelle.show-protocol
 isabelle.activate.label=Activate current buffer
 isabelle.show-output.label=Show Output
+isabelle.show-raw-output.label=Show Raw Output
 isabelle.show-protocol.label=Show Protocol
 
 #dockables
 isabelle-output.title=Output
+isabelle-raw-output.title=Raw Output
 isabelle-protocol.title=Protocol
 
 #SideKick
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/plugin/actions.xml
--- a/src/Tools/jEdit/plugin/actions.xml	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml	Tue May 25 10:57:02 2010 +0200
@@ -15,6 +15,11 @@
 			wm.addDockableWindow("isabelle-output");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.show-raw-output">
+		<CODE>
+			wm.addDockableWindow("isabelle-raw-output");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.show-protocol">
 		<CODE>
 			wm.addDockableWindow("isabelle-protocol");
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/plugin/dockables.xml
--- a/src/Tools/jEdit/plugin/dockables.xml	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml	Tue May 25 10:57:02 2010 +0200
@@ -5,6 +5,9 @@
 	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
 		new isabelle.jedit.Output_Dockable(view, position);
 	</DOCKABLE>
+	<DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+		new isabelle.jedit.Raw_Output_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
 		new isabelle.jedit.Protocol_Dockable(view, position);
 	</DOCKABLE>
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/src/jedit/dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/dockable.scala	Tue May 25 10:57:02 2010 +0200
@@ -0,0 +1,41 @@
+/*  Title:      Tools/jEdit/src/jedit/dockable.scala
+    Author:     Makarius
+
+Generic dockable window.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Dimension, Component, BorderLayout}
+import javax.swing.JPanel
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+{
+  if (position == DockableWindowManager.FLOATING)
+    setPreferredSize(new Dimension(500, 250))
+
+  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
+  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
+
+  protected def init() { }
+  protected def exit() { }
+
+  override def addNotify()
+  {
+    super.addNotify()
+    init()
+  }
+
+  override def removeNotify()
+  {
+    exit()
+    super.removeNotify()
+  }
+}
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Tue May 25 10:57:02 2010 +0200
@@ -13,7 +13,6 @@
 import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
 import java.awt.event.MouseEvent
 
-import javax.swing.{JButton, JPanel, JScrollPane}
 import java.util.logging.{Logger, Level}
 
 import org.w3c.dom.html2.HTMLElement
@@ -92,10 +91,7 @@
 <head>
 <style media="all" type="text/css">
 """ +
-  system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
-  system.try_read("$JEDIT_HOME/etc/isabelle-jedit.css") + "\n" +
-  system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
-  system.try_read("$ISABELLE_HOME_USER/etc/isabelle-jedit.css") + "\n"
+  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
 
   private val template_tail =
 """
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue May 25 10:57:02 2010 +0200
@@ -14,20 +14,14 @@
 import scala.swing.{FlowPanel, Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
-import javax.swing.JPanel
-import java.awt.{BorderLayout, Dimension}
+import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
 
 
-class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+class Output_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-
   val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
   add(html_panel, BorderLayout.CENTER)
 
@@ -81,7 +75,7 @@
           val document = model.recent_document
           document.command_at(view.getTextArea.getCaretPosition) match {
             case Some((cmd, _)) =>
-              output_actor ! Render(filtered_results(document, cmd))
+              main_actor ! Render(filtered_results(document, cmd))
             case None =>
           }
         case None =>
@@ -97,9 +91,9 @@
     }
 
 
-  /* actor wiring */
+  /* main actor */
 
-  private val output_actor = actor {
+  private val main_actor = actor {
     loop {
       react {
         case Session.Global_Settings => handle_resize()
@@ -114,23 +108,21 @@
               html_panel.render(filtered_results(model.recent_document, cmd))
           }
 
-        case bad => System.err.println("output_actor: ignoring bad message " + bad)
+        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def addNotify()
+  override def init()
   {
-    super.addNotify()
-    Isabelle.session.results += output_actor
-    Isabelle.session.global_settings += output_actor
+    Isabelle.session.results += main_actor
+    Isabelle.session.global_settings += main_actor
   }
 
-  override def removeNotify()
+  override def exit()
   {
-    Isabelle.session.results -= output_actor
-    Isabelle.session.global_settings -= output_actor
-    super.removeNotify()
+    Isabelle.session.results -= main_actor
+    Isabelle.session.global_settings -= main_actor
   }
 
 
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue May 25 10:57:02 2010 +0200
@@ -21,6 +21,7 @@
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
 object Isabelle
@@ -112,6 +113,29 @@
     jedit_text_areas().filter(_.getBuffer == buffer)
 
 
+  /* dockable windows */
+
+  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
+
+  def docked_output(view: View): Option[Output_Dockable] =
+    wm(view).getDockableWindow("isabelle-output") match {
+      case dockable: Output_Dockable => Some(dockable)
+      case _ => None
+    }
+
+  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
+    wm(view).getDockableWindow("isabelle-raw-output") match {
+      case dockable: Raw_Output_Dockable => Some(dockable)
+      case _ => None
+    }
+
+  def docked_protocol(view: View): Option[Protocol_Dockable] =
+    wm(view).getDockableWindow("isabelle-protocol") match {
+      case dockable: Protocol_Dockable => Some(dockable)
+      case _ => None
+    }
+
+
   /* manage prover */
 
   private def prover_started(view: View): Boolean =
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/src/jedit/protocol_dockable.scala
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Mon May 24 21:19:25 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Tue May 25 10:57:02 2010 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/jedit/protocol_dockable.scala
     Author:     Makarius
 
-Dockable window for raw process output.
+Dockable window for protocol messages.
 */
 
 package isabelle.jedit
@@ -10,45 +10,30 @@
 import isabelle._
 
 import scala.actors.Actor._
-
-import java.awt.{Dimension, Graphics, BorderLayout}
-import javax.swing.{JPanel, JTextArea, JScrollPane}
+import scala.swing.{TextArea, ScrollPane}
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
-class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-
-  private val text_area = new JTextArea
-  add(new JScrollPane(text_area), BorderLayout.CENTER)
+  private val text_area = new TextArea
+  set_content(new ScrollPane(text_area))
 
 
-  /* actor wiring */
+  /* main actor */
 
-  private val raw_actor = actor {
+  private val main_actor = actor {
     loop {
       react {
         case result: Isabelle_Process.Result =>
           Swing_Thread.now { text_area.append(result.message.toString + "\n") }
 
-        case bad => System.err.println("raw_actor: ignoring bad message " + bad)
+        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def addNotify()
-  {
-    super.addNotify()
-    Isabelle.session.raw_results += raw_actor
-  }
-
-  override def removeNotify()
-  {
-    Isabelle.session.raw_results -= raw_actor
-    super.removeNotify()
-  }
+  override def init() { Isabelle.session.raw_results += main_actor }
+  override def exit() { Isabelle.session.raw_results -= main_actor }
 }
diff -r 844d9842aec7 -r d37b5a9bec14 src/Tools/jEdit/src/jedit/raw_output_dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue May 25 10:57:02 2010 +0200
@@ -0,0 +1,40 @@
+/*  Title:      Tools/jEdit/src/jedit/raw_output_dockable.scala
+    Author:     Makarius
+
+Dockable window for raw process output (stdout).
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.{TextArea, ScrollPane}
+
+import org.gjt.sp.jedit.View
+
+
+class Raw_Output_Dockable(view: View, position: String)
+  extends Dockable(view: View, position: String)
+{
+  private val text_area = new TextArea
+  set_content(new ScrollPane(text_area))
+
+
+  /* main actor */
+
+  private val main_actor = actor {
+    loop {
+      react {
+        case result: Isabelle_Process.Result =>
+          Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
+
+        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def init() { Isabelle.session.raw_output += main_actor }
+  override def exit() { Isabelle.session.raw_output -= main_actor }
+}