# HG changeset patch # User wenzelm # Date 1274365522 -7200 # Node ID f692d6178e4e3830ab0b759f45c3b39b0f52336c # Parent 8096a4c755ebed71a58debb1237a952361e961be# Parent 9421452afc29cb99390f11f0d0e5e6d5c2bbf052 merged diff -r 8096a4c755eb -r f692d6178e4e src/Pure/PIDE/command.scala --- 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 } diff -r 8096a4c755eb -r f692d6178e4e src/Pure/PIDE/document.scala --- 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) + } } } diff -r 8096a4c755eb -r f692d6178e4e src/Pure/System/gui_setup.scala --- 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) diff -r 8096a4c755eb -r f692d6178e4e src/Pure/System/isabelle_system.scala --- 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")) diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/document_view.scala --- 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 } } diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/html_panel.scala --- 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 = - { - """ - - - - - - - -""" - } - - 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 = + { + """ + + + + + + + +""" + } + + 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) } } diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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) diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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 diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- 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) diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/output_dockable.scala --- 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() } diff -r 8096a4c755eb -r f692d6178e4e src/Tools/jEdit/src/jedit/protocol_dockable.scala --- 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) }