--- a/src/Pure/PIDE/command.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu May 20 16:25:22 2010 +0200
@@ -20,6 +20,7 @@
val UNPROCESSED = Value("UNPROCESSED")
val FINISHED = Value("FINISHED")
val FAILED = Value("FAILED")
+ val UNDEFINED = Value("UNDEFINED")
}
case class HighlightInfo(highlight: String) { override def toString = highlight }
--- a/src/Pure/PIDE/document.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Pure/PIDE/document.scala Thu May 20 16:25:22 2010 +0200
@@ -175,9 +175,12 @@
System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
}
- def current_state(cmd: Command): Option[State] =
+ def current_state(cmd: Command): State =
{
require(assignment.is_finished)
- (assignment.join).get(cmd).map(_.current_state)
+ (assignment.join).get(cmd) match {
+ case Some(cmd_state) => cmd_state.current_state
+ case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
+ }
}
}
--- a/src/Pure/System/gui_setup.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Pure/System/gui_setup.scala Thu May 20 16:25:22 2010 +0200
@@ -6,8 +6,8 @@
package isabelle
-import scala.swing._
-import scala.swing.event._
+import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
object GUI_Setup extends SwingApplication
@@ -27,16 +27,14 @@
editable = false
columns = 80
rows = 20
- xLayoutAlignment = 0.5
}
- val ok = new Button {
- text = "OK"
- xLayoutAlignment = 0.5
- }
- contents = new BoxPanel(Orientation.Vertical) {
- contents += text
- contents += ok
- }
+ val ok = new Button { text = "OK" }
+ val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
+
+ val panel = new BorderPanel
+ panel.layout(text) = BorderPanel.Position.Center
+ panel.layout(ok_panel) = BorderPanel.Position.South
+ contents = panel
// values
if (Platform.is_windows)
--- a/src/Pure/System/isabelle_system.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu May 20 16:25:22 2010 +0200
@@ -150,6 +150,15 @@
def platform_file(path: String) = new File(platform_path(path))
+ /* try_read */
+
+ def try_read(path: String): String =
+ {
+ val file = platform_file(path)
+ if (file.isFile) Source.fromFile(file).mkString else ""
+ }
+
+
/* source files */
private def try_file(file: File) = if (file.isFile) Some(file) else None
@@ -304,11 +313,8 @@
/* symbols */
private def read_symbols(path: String): List[String] =
- {
- val file = platform_file(path)
- if (file.isFile) Source.fromFile(file).getLines("\n").toList
- else Nil
- }
+ 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"))
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu May 20 16:25:22 2010 +0200
@@ -25,11 +25,11 @@
{
def choose_color(command: Command, doc: Document): Color =
{
- doc.current_state(command).map(_.status) match {
- case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
- case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
- case Some(Command.Status.FAILED) => new Color(255, 193, 193)
- case _ => Color.red
+ doc.current_state(command).status match {
+ case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+ case Command.Status.FINISHED => new Color(234, 248, 255)
+ case Command.Status.FAILED => new Color(255, 193, 193)
+ case Command.Status.UNDEFINED => Color.red
}
}
@@ -146,7 +146,7 @@
val offset = model.from_current(document, text_area.xyToOffset(x, y))
document.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
+ document.current_state(command).type_at(offset - command_start) getOrElse null
case None => null
}
}
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 16:25:22 2010 +0200
@@ -23,7 +23,6 @@
import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
-import scala.io.Source
import scala.actors.Actor._
@@ -39,7 +38,7 @@
class HTML_Panel(
- sys: Isabelle_System,
+ system: Isabelle_System,
initial_font_size: Int,
handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
{
@@ -47,8 +46,9 @@
Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
- /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
+ /* Lobo setup */
+ // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize
val screen_resolution =
if (GraphicsEnvironment.isHeadless()) 72
else Toolkit.getDefaultToolkit().getScreenResolution()
@@ -57,47 +57,7 @@
def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
- /* document template */
-
- private def try_file(name: String): String =
- {
- val file = sys.platform_file(name)
- if (file.isFile) Source.fromFile(file).mkString else ""
- }
-
- private def template(font_size: Int): String =
- {
- """<?xml version="1.0" encoding="utf-8"?>
-<!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>
-<style media="all" type="text/css">
-""" +
- try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
- try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
- "body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
-"""
-</style>
-</head>
-<body/>
-</html>
-"""
- }
-
- private def font_metrics(font_size: Int): FontMetrics =
- Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
-
- private def panel_width(font_size: Int): Int =
- Swing_Thread.now {
- (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
- }
-
-
- /* actor with local state */
-
private val ucontext = new SimpleUserAgentContext
-
private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
{
private def handle(event: HTML_Panel.Event): Boolean =
@@ -118,54 +78,87 @@
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
- private case class Init(font_size: Int)
- private case class Render(divs: List[XML.Tree])
+
+ /* physical document */
+
+ private def template(font_size: Int): String =
+ {
+ """<?xml version="1.0" encoding="utf-8"?>
+<!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>
+<style media="all" type="text/css">
+""" +
+ system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
+ system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
+ "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
+"""
+</style>
+</head>
+<body/>
+</html>
+"""
+ }
+
+ private class Doc
+ {
+ var current_font_size: Int = 0
+ var current_font_metrics: FontMetrics = null
+ var current_body: List[XML.Tree] = Nil
+ var current_DOM: org.w3c.dom.Document = null
+
+ def resize(font_size: Int)
+ {
+ if (font_size != current_font_size || current_font_metrics == null) {
+ Swing_Thread.now {
+ current_font_size = font_size
+ current_font_metrics =
+ getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
+ }
+ current_DOM =
+ builder.parse(
+ new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
+ render(current_body)
+ }
+ }
+
+ def render(body: List[XML.Tree])
+ {
+ current_body = body
+ val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
+ val html_body =
+ current_body.flatMap(div =>
+ Pretty.formatted(List(div), margin,
+ Pretty.font_metric(current_font_metrics))
+ .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
+
+ val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
+ current_DOM.removeChild(current_DOM.getLastChild())
+ current_DOM.appendChild(node)
+ Swing_Thread.now { setDocument(current_DOM, rcontext) }
+ }
+
+ resize(initial_font_size)
+ }
+
+
+ /* main actor and method wrappers */
+
+ private case class Resize(font_size: Int)
+ private case class Render(body: List[XML.Tree])
private val main_actor = actor {
- // crude double buffering
- var doc1: org.w3c.dom.Document = null
- var doc2: org.w3c.dom.Document = null
-
- var current_font_size = 16
- var current_font_metrics: FontMetrics = null
-
+ var doc = new Doc
loop {
react {
- case Init(font_size) =>
- current_font_size = font_size
- current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
-
- val src = template(font_size)
- def parse() =
- builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
- doc1 = parse()
- doc2 = parse()
- Swing_Thread.now { setDocument(doc1, rcontext) }
-
- case Render(divs) =>
- val doc = doc2
- val html_body =
- divs.flatMap(div =>
- Pretty.formatted(List(div), panel_width(current_font_size),
- Pretty.font_metric(current_font_metrics))
- .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
- val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
- doc.removeChild(doc.getLastChild())
- doc.appendChild(node)
- doc2 = doc1
- doc1 = doc
- Swing_Thread.now { setDocument(doc1, rcontext) }
-
+ case Resize(font_size) => doc.resize(font_size)
+ case Render(body) => doc.render(body)
case bad => System.err.println("main_actor: ignoring bad message " + bad)
}
}
}
-
- /* main method wrappers */
-
- def init(font_size: Int) { main_actor ! Init(font_size) }
- def render(divs: List[XML.Tree]) { main_actor ! Render(divs) }
-
- init(initial_font_size)
+ def resize(font_size: Int) { main_actor ! Resize(font_size) }
+ def render(body: List[XML.Tree]) { main_actor ! Render(body) }
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu May 20 16:25:22 2010 +0200
@@ -46,7 +46,7 @@
val offset = model.from_current(document, original_offset)
document.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).get.ref_at(offset - command_start) match {
+ document.current_state(command).ref_at(offset - command_start) match {
case Some(ref) =>
val begin = model.to_current(document, command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu May 20 16:25:22 2010 +0200
@@ -130,7 +130,7 @@
val root = data.root
val document = model.recent_document()
for ((command, command_start) <- document.command_range(0) if !stopped) {
- root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
+ root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
{
val content = command.source(node.start, node.stop).replace('\n', ' ')
val id = command.id
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu May 20 16:25:22 2010 +0200
@@ -116,7 +116,7 @@
var next_x = start
for {
(command, command_start) <- document.command_range(from(start), from(stop))
- markup <- document.current_state(command).get.highlight.flatten
+ markup <- document.current_state(command).highlight.flatten
val abs_start = to(command_start + markup.start)
val abs_stop = to(command_start + markup.stop)
if (abs_stop > start)
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 16:25:22 2010 +0200
@@ -11,6 +11,9 @@
import scala.actors.Actor._
+import scala.swing.{FlowPanel, Button, ToggleButton}
+import scala.swing.event.ButtonClicked
+
import javax.swing.JPanel
import java.awt.{BorderLayout, Dimension}
@@ -24,25 +27,58 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
+ val controls = new FlowPanel(FlowPanel.Alignment.Right)()
+ add(controls.peer, BorderLayout.NORTH)
+
val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
add(html_panel, BorderLayout.CENTER)
+ /* controls */
+
+ private case class Render(body: List[XML.Tree])
+
+ private def handle_update()
+ {
+ Swing_Thread.now {
+ Document_Model(view.getBuffer) match {
+ case Some(model) =>
+ val document = model.recent_document
+ document.command_at(view.getTextArea.getCaretPosition) match {
+ case Some((cmd, _)) =>
+ output_actor ! Render(document.current_state(cmd).results)
+ case None =>
+ }
+ case None =>
+ }
+ }
+ }
+
+ private val update = new Button("Update") {
+ reactions += { case ButtonClicked(_) => handle_update() }
+ }
+
+ val follow = new ToggleButton("Follow")
+ follow.selected = true
+
+
/* actor wiring */
private val output_actor = actor {
loop {
react {
+ case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
+
+ case Render(body) => html_panel.render(body)
+
case cmd: Command =>
- Swing_Thread.now { Document_Model(view.getBuffer) } match {
+ Swing_Thread.now {
+ if (follow.selected) Document_Model(view.getBuffer) else None
+ } match {
case None =>
- case Some(model) =>
- val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
- html_panel.render(body)
+ case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
}
- case Session.Global_Settings => html_panel.init(Isabelle.font_size())
-
case bad => System.err.println("output_actor: ignoring bad message " + bad)
}
}
@@ -61,4 +97,10 @@
Isabelle.session.global_settings -= output_actor
super.removeNotify()
}
+
+
+ /* init controls */
+
+ controls.contents ++= List(update, follow)
+ handle_update()
}
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu May 20 07:36:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu May 20 16:25:22 2010 +0200
@@ -33,7 +33,7 @@
loop {
react {
case result: Isabelle_Process.Result =>
- Swing_Thread.now { text_area.append(result.toString + "\n") }
+ Swing_Thread.now { text_area.append(result.message.toString + "\n") }
case bad => System.err.println("raw_actor: ignoring bad message " + bad)
}