--- 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
###
--- 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 { }
--- 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)
--- 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 =
--- 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 */
--- 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")
}
--- 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)
}
--- 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]] =
--- 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 {
--- 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
}
--- 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.
--- 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 { }
--- 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"
+
--- 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
--- 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");
--- 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>
--- /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()
+ }
+}
--- 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 =
"""
--- 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
}
--- 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 =
--- 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 }
}
--- /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 }
+}