1.1 --- a/src/Pure/PIDE/command.scala Thu May 20 07:36:50 2010 +0200
1.2 +++ b/src/Pure/PIDE/command.scala Thu May 20 16:25:22 2010 +0200
1.3 @@ -20,6 +20,7 @@
1.4 val UNPROCESSED = Value("UNPROCESSED")
1.5 val FINISHED = Value("FINISHED")
1.6 val FAILED = Value("FAILED")
1.7 + val UNDEFINED = Value("UNDEFINED")
1.8 }
1.9
1.10 case class HighlightInfo(highlight: String) { override def toString = highlight }
2.1 --- a/src/Pure/PIDE/document.scala Thu May 20 07:36:50 2010 +0200
2.2 +++ b/src/Pure/PIDE/document.scala Thu May 20 16:25:22 2010 +0200
2.3 @@ -175,9 +175,12 @@
2.4 System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
2.5 }
2.6
2.7 - def current_state(cmd: Command): Option[State] =
2.8 + def current_state(cmd: Command): State =
2.9 {
2.10 require(assignment.is_finished)
2.11 - (assignment.join).get(cmd).map(_.current_state)
2.12 + (assignment.join).get(cmd) match {
2.13 + case Some(cmd_state) => cmd_state.current_state
2.14 + case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
2.15 + }
2.16 }
2.17 }
3.1 --- a/src/Pure/System/gui_setup.scala Thu May 20 07:36:50 2010 +0200
3.2 +++ b/src/Pure/System/gui_setup.scala Thu May 20 16:25:22 2010 +0200
3.3 @@ -6,8 +6,8 @@
3.4
3.5 package isabelle
3.6
3.7 -import scala.swing._
3.8 -import scala.swing.event._
3.9 +import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
3.10 +import scala.swing.event.ButtonClicked
3.11
3.12
3.13 object GUI_Setup extends SwingApplication
3.14 @@ -27,16 +27,14 @@
3.15 editable = false
3.16 columns = 80
3.17 rows = 20
3.18 - xLayoutAlignment = 0.5
3.19 }
3.20 - val ok = new Button {
3.21 - text = "OK"
3.22 - xLayoutAlignment = 0.5
3.23 - }
3.24 - contents = new BoxPanel(Orientation.Vertical) {
3.25 - contents += text
3.26 - contents += ok
3.27 - }
3.28 + val ok = new Button { text = "OK" }
3.29 + val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
3.30 +
3.31 + val panel = new BorderPanel
3.32 + panel.layout(text) = BorderPanel.Position.Center
3.33 + panel.layout(ok_panel) = BorderPanel.Position.South
3.34 + contents = panel
3.35
3.36 // values
3.37 if (Platform.is_windows)
4.1 --- a/src/Pure/System/isabelle_system.scala Thu May 20 07:36:50 2010 +0200
4.2 +++ b/src/Pure/System/isabelle_system.scala Thu May 20 16:25:22 2010 +0200
4.3 @@ -150,6 +150,15 @@
4.4 def platform_file(path: String) = new File(platform_path(path))
4.5
4.6
4.7 + /* try_read */
4.8 +
4.9 + def try_read(path: String): String =
4.10 + {
4.11 + val file = platform_file(path)
4.12 + if (file.isFile) Source.fromFile(file).mkString else ""
4.13 + }
4.14 +
4.15 +
4.16 /* source files */
4.17
4.18 private def try_file(file: File) = if (file.isFile) Some(file) else None
4.19 @@ -304,11 +313,8 @@
4.20 /* symbols */
4.21
4.22 private def read_symbols(path: String): List[String] =
4.23 - {
4.24 - val file = platform_file(path)
4.25 - if (file.isFile) Source.fromFile(file).getLines("\n").toList
4.26 - else Nil
4.27 - }
4.28 + Library.chunks(try_read(path)).map(_.toString).toList
4.29 +
4.30 val symbols = new Symbol.Interpretation(
4.31 read_symbols("$ISABELLE_HOME/etc/symbols") :::
4.32 read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
5.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Thu May 20 07:36:50 2010 +0200
5.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu May 20 16:25:22 2010 +0200
5.3 @@ -25,11 +25,11 @@
5.4 {
5.5 def choose_color(command: Command, doc: Document): Color =
5.6 {
5.7 - doc.current_state(command).map(_.status) match {
5.8 - case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
5.9 - case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
5.10 - case Some(Command.Status.FAILED) => new Color(255, 193, 193)
5.11 - case _ => Color.red
5.12 + doc.current_state(command).status match {
5.13 + case Command.Status.UNPROCESSED => new Color(255, 228, 225)
5.14 + case Command.Status.FINISHED => new Color(234, 248, 255)
5.15 + case Command.Status.FAILED => new Color(255, 193, 193)
5.16 + case Command.Status.UNDEFINED => Color.red
5.17 }
5.18 }
5.19
5.20 @@ -146,7 +146,7 @@
5.21 val offset = model.from_current(document, text_area.xyToOffset(x, y))
5.22 document.command_at(offset) match {
5.23 case Some((command, command_start)) =>
5.24 - document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
5.25 + document.current_state(command).type_at(offset - command_start) getOrElse null
5.26 case None => null
5.27 }
5.28 }
6.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 07:36:50 2010 +0200
6.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 16:25:22 2010 +0200
6.3 @@ -23,7 +23,6 @@
6.4 import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
6.5 import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
6.6
6.7 -import scala.io.Source
6.8 import scala.actors.Actor._
6.9
6.10
6.11 @@ -39,7 +38,7 @@
6.12
6.13
6.14 class HTML_Panel(
6.15 - sys: Isabelle_System,
6.16 + system: Isabelle_System,
6.17 initial_font_size: Int,
6.18 handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
6.19 {
6.20 @@ -47,8 +46,9 @@
6.21 Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
6.22
6.23
6.24 - /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
6.25 + /* Lobo setup */
6.26
6.27 + // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize
6.28 val screen_resolution =
6.29 if (GraphicsEnvironment.isHeadless()) 72
6.30 else Toolkit.getDefaultToolkit().getScreenResolution()
6.31 @@ -57,47 +57,7 @@
6.32 def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
6.33
6.34
6.35 - /* document template */
6.36 -
6.37 - private def try_file(name: String): String =
6.38 - {
6.39 - val file = sys.platform_file(name)
6.40 - if (file.isFile) Source.fromFile(file).mkString else ""
6.41 - }
6.42 -
6.43 - private def template(font_size: Int): String =
6.44 - {
6.45 - """<?xml version="1.0" encoding="utf-8"?>
6.46 -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
6.47 - "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
6.48 -<html xmlns="http://www.w3.org/1999/xhtml">
6.49 -<head>
6.50 -<style media="all" type="text/css">
6.51 -""" +
6.52 - try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
6.53 - try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
6.54 - "body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
6.55 -"""
6.56 -</style>
6.57 -</head>
6.58 -<body/>
6.59 -</html>
6.60 -"""
6.61 - }
6.62 -
6.63 - private def font_metrics(font_size: Int): FontMetrics =
6.64 - Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
6.65 -
6.66 - private def panel_width(font_size: Int): Int =
6.67 - Swing_Thread.now {
6.68 - (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
6.69 - }
6.70 -
6.71 -
6.72 - /* actor with local state */
6.73 -
6.74 private val ucontext = new SimpleUserAgentContext
6.75 -
6.76 private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
6.77 {
6.78 private def handle(event: HTML_Panel.Event): Boolean =
6.79 @@ -118,54 +78,87 @@
6.80
6.81 private val builder = new DocumentBuilderImpl(ucontext, rcontext)
6.82
6.83 - private case class Init(font_size: Int)
6.84 - private case class Render(divs: List[XML.Tree])
6.85 +
6.86 + /* physical document */
6.87 +
6.88 + private def template(font_size: Int): String =
6.89 + {
6.90 + """<?xml version="1.0" encoding="utf-8"?>
6.91 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
6.92 + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
6.93 +<html xmlns="http://www.w3.org/1999/xhtml">
6.94 +<head>
6.95 +<style media="all" type="text/css">
6.96 +""" +
6.97 + system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
6.98 + system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
6.99 + "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
6.100 +"""
6.101 +</style>
6.102 +</head>
6.103 +<body/>
6.104 +</html>
6.105 +"""
6.106 + }
6.107 +
6.108 + private class Doc
6.109 + {
6.110 + var current_font_size: Int = 0
6.111 + var current_font_metrics: FontMetrics = null
6.112 + var current_body: List[XML.Tree] = Nil
6.113 + var current_DOM: org.w3c.dom.Document = null
6.114 +
6.115 + def resize(font_size: Int)
6.116 + {
6.117 + if (font_size != current_font_size || current_font_metrics == null) {
6.118 + Swing_Thread.now {
6.119 + current_font_size = font_size
6.120 + current_font_metrics =
6.121 + getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
6.122 + }
6.123 + current_DOM =
6.124 + builder.parse(
6.125 + new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
6.126 + render(current_body)
6.127 + }
6.128 + }
6.129 +
6.130 + def render(body: List[XML.Tree])
6.131 + {
6.132 + current_body = body
6.133 + val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
6.134 + val html_body =
6.135 + current_body.flatMap(div =>
6.136 + Pretty.formatted(List(div), margin,
6.137 + Pretty.font_metric(current_font_metrics))
6.138 + .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
6.139 +
6.140 + val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
6.141 + current_DOM.removeChild(current_DOM.getLastChild())
6.142 + current_DOM.appendChild(node)
6.143 + Swing_Thread.now { setDocument(current_DOM, rcontext) }
6.144 + }
6.145 +
6.146 + resize(initial_font_size)
6.147 + }
6.148 +
6.149 +
6.150 + /* main actor and method wrappers */
6.151 +
6.152 + private case class Resize(font_size: Int)
6.153 + private case class Render(body: List[XML.Tree])
6.154
6.155 private val main_actor = actor {
6.156 - // crude double buffering
6.157 - var doc1: org.w3c.dom.Document = null
6.158 - var doc2: org.w3c.dom.Document = null
6.159 -
6.160 - var current_font_size = 16
6.161 - var current_font_metrics: FontMetrics = null
6.162 -
6.163 + var doc = new Doc
6.164 loop {
6.165 react {
6.166 - case Init(font_size) =>
6.167 - current_font_size = font_size
6.168 - current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
6.169 -
6.170 - val src = template(font_size)
6.171 - def parse() =
6.172 - builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
6.173 - doc1 = parse()
6.174 - doc2 = parse()
6.175 - Swing_Thread.now { setDocument(doc1, rcontext) }
6.176 -
6.177 - case Render(divs) =>
6.178 - val doc = doc2
6.179 - val html_body =
6.180 - divs.flatMap(div =>
6.181 - Pretty.formatted(List(div), panel_width(current_font_size),
6.182 - Pretty.font_metric(current_font_metrics))
6.183 - .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
6.184 - val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
6.185 - doc.removeChild(doc.getLastChild())
6.186 - doc.appendChild(node)
6.187 - doc2 = doc1
6.188 - doc1 = doc
6.189 - Swing_Thread.now { setDocument(doc1, rcontext) }
6.190 -
6.191 + case Resize(font_size) => doc.resize(font_size)
6.192 + case Render(body) => doc.render(body)
6.193 case bad => System.err.println("main_actor: ignoring bad message " + bad)
6.194 }
6.195 }
6.196 }
6.197
6.198 -
6.199 - /* main method wrappers */
6.200 -
6.201 - def init(font_size: Int) { main_actor ! Init(font_size) }
6.202 - def render(divs: List[XML.Tree]) { main_actor ! Render(divs) }
6.203 -
6.204 - init(initial_font_size)
6.205 + def resize(font_size: Int) { main_actor ! Resize(font_size) }
6.206 + def render(body: List[XML.Tree]) { main_actor ! Render(body) }
6.207 }
7.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu May 20 07:36:50 2010 +0200
7.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu May 20 16:25:22 2010 +0200
7.3 @@ -46,7 +46,7 @@
7.4 val offset = model.from_current(document, original_offset)
7.5 document.command_at(offset) match {
7.6 case Some((command, command_start)) =>
7.7 - document.current_state(command).get.ref_at(offset - command_start) match {
7.8 + document.current_state(command).ref_at(offset - command_start) match {
7.9 case Some(ref) =>
7.10 val begin = model.to_current(document, command_start + ref.start)
7.11 val line = buffer.getLineOfOffset(begin)
8.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu May 20 07:36:50 2010 +0200
8.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu May 20 16:25:22 2010 +0200
8.3 @@ -130,7 +130,7 @@
8.4 val root = data.root
8.5 val document = model.recent_document()
8.6 for ((command, command_start) <- document.command_range(0) if !stopped) {
8.7 - root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
8.8 + root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
8.9 {
8.10 val content = command.source(node.start, node.stop).replace('\n', ' ')
8.11 val id = command.id
9.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu May 20 07:36:50 2010 +0200
9.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu May 20 16:25:22 2010 +0200
9.3 @@ -116,7 +116,7 @@
9.4 var next_x = start
9.5 for {
9.6 (command, command_start) <- document.command_range(from(start), from(stop))
9.7 - markup <- document.current_state(command).get.highlight.flatten
9.8 + markup <- document.current_state(command).highlight.flatten
9.9 val abs_start = to(command_start + markup.start)
9.10 val abs_stop = to(command_start + markup.stop)
9.11 if (abs_stop > start)
10.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 07:36:50 2010 +0200
10.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 16:25:22 2010 +0200
10.3 @@ -11,6 +11,9 @@
10.4
10.5 import scala.actors.Actor._
10.6
10.7 +import scala.swing.{FlowPanel, Button, ToggleButton}
10.8 +import scala.swing.event.ButtonClicked
10.9 +
10.10 import javax.swing.JPanel
10.11 import java.awt.{BorderLayout, Dimension}
10.12
10.13 @@ -24,25 +27,58 @@
10.14 if (position == DockableWindowManager.FLOATING)
10.15 setPreferredSize(new Dimension(500, 250))
10.16
10.17 + val controls = new FlowPanel(FlowPanel.Alignment.Right)()
10.18 + add(controls.peer, BorderLayout.NORTH)
10.19 +
10.20 val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
10.21 add(html_panel, BorderLayout.CENTER)
10.22
10.23
10.24 + /* controls */
10.25 +
10.26 + private case class Render(body: List[XML.Tree])
10.27 +
10.28 + private def handle_update()
10.29 + {
10.30 + Swing_Thread.now {
10.31 + Document_Model(view.getBuffer) match {
10.32 + case Some(model) =>
10.33 + val document = model.recent_document
10.34 + document.command_at(view.getTextArea.getCaretPosition) match {
10.35 + case Some((cmd, _)) =>
10.36 + output_actor ! Render(document.current_state(cmd).results)
10.37 + case None =>
10.38 + }
10.39 + case None =>
10.40 + }
10.41 + }
10.42 + }
10.43 +
10.44 + private val update = new Button("Update") {
10.45 + reactions += { case ButtonClicked(_) => handle_update() }
10.46 + }
10.47 +
10.48 + val follow = new ToggleButton("Follow")
10.49 + follow.selected = true
10.50 +
10.51 +
10.52 /* actor wiring */
10.53
10.54 private val output_actor = actor {
10.55 loop {
10.56 react {
10.57 + case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
10.58 +
10.59 + case Render(body) => html_panel.render(body)
10.60 +
10.61 case cmd: Command =>
10.62 - Swing_Thread.now { Document_Model(view.getBuffer) } match {
10.63 + Swing_Thread.now {
10.64 + if (follow.selected) Document_Model(view.getBuffer) else None
10.65 + } match {
10.66 case None =>
10.67 - case Some(model) =>
10.68 - val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
10.69 - html_panel.render(body)
10.70 + case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
10.71 }
10.72
10.73 - case Session.Global_Settings => html_panel.init(Isabelle.font_size())
10.74 -
10.75 case bad => System.err.println("output_actor: ignoring bad message " + bad)
10.76 }
10.77 }
10.78 @@ -61,4 +97,10 @@
10.79 Isabelle.session.global_settings -= output_actor
10.80 super.removeNotify()
10.81 }
10.82 +
10.83 +
10.84 + /* init controls */
10.85 +
10.86 + controls.contents ++= List(update, follow)
10.87 + handle_update()
10.88 }
11.1 --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu May 20 07:36:50 2010 +0200
11.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu May 20 16:25:22 2010 +0200
11.3 @@ -33,7 +33,7 @@
11.4 loop {
11.5 react {
11.6 case result: Isabelle_Process.Result =>
11.7 - Swing_Thread.now { text_area.append(result.toString + "\n") }
11.8 + Swing_Thread.now { text_area.append(result.message.toString + "\n") }
11.9
11.10 case bad => System.err.println("raw_actor: ignoring bad message " + bad)
11.11 }