--- a/src/Pure/PIDE/command.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu May 27 13:13:30 2010 +0200
@@ -13,6 +13,9 @@
import scala.collection.mutable
+case class Command_Set(set: Set[Command])
+
+
object Command
{
object Status extends Enumeration
@@ -29,10 +32,10 @@
command_id: Option[String], offset: Option[Int])
}
-
class Command(
val id: Isar_Document.Command_ID,
- val span: Thy_Syntax.Span)
+ val span: Thy_Syntax.Span,
+ val static_parent: Option[Command] = None)
extends Session.Entity
{
/* classification */
@@ -42,7 +45,9 @@
def is_malformed: Boolean = !is_command && !is_ignored
def name: String = if (is_command) span.head.content else ""
- override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
+ override def toString =
+ if (is_command) name + "(" + id + ")"
+ else if (is_ignored) "<ignored>" else "<malformed>"
/* source text */
@@ -59,15 +64,17 @@
@volatile protected var state = new State(this)
def current_state: State = state
- private case class Consume(session: Session, message: XML.Tree)
+ private case class Consume(message: XML.Tree, forward: Command => Unit)
private case object Assign
private val accumulator = actor {
var assigned = false
loop {
react {
- case Consume(session: Session, message: XML.Tree) if !assigned =>
- state = state.+(session, message)
+ case Consume(message, forward) if !assigned =>
+ val old_state = state
+ state = old_state + message
+ if (!(state eq old_state)) forward(static_parent getOrElse this)
case Assign =>
assigned = true // single assignment
@@ -78,11 +85,14 @@
}
}
- def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+ def consume(message: XML.Tree, forward: Command => Unit)
+ {
+ accumulator ! Consume(message, forward)
+ }
def assign_state(state_id: Isar_Document.State_ID): Command =
{
- val cmd = new Command(state_id, span)
+ val cmd = new Command(state_id, span, Some(this))
accumulator !? Assign
cmd.state = current_state
cmd
--- a/src/Pure/PIDE/state.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Pure/PIDE/state.scala Thu May 27 13:13:30 2010 +0200
@@ -70,50 +70,45 @@
/* message dispatch */
- def + (session: Session, message: XML.Tree): State =
- {
- val changed: State =
- message match {
- case XML.Elem(Markup.STATUS, _, elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(kind, atts, body) =>
- atts match {
- case Position.Range(begin, end) =>
- if (kind == Markup.ML_TYPING) {
- val info = Pretty.string_of(body, margin = 40)
- state.add_markup(
- command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+ def + (message: XML.Tree): State =
+ message match {
+ case XML.Elem(Markup.STATUS, _, elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
+ case XML.Elem(kind, atts, body) =>
+ atts match {
+ case Position.Range(begin, end) =>
+ if (kind == Markup.ML_TYPING) {
+ val info = Pretty.string_of(body, margin = 40)
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+ }
+ else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+ state.add_markup(command.markup_node(
+ begin - 1, end - 1,
+ Command.RefInfo(
+ Position.get_file(atts),
+ Position.get_line(atts),
+ Position.get_id(atts),
+ Position.get_offset(atts))))
+ case _ => state
}
- else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
- state.add_markup(command.markup_node(
- begin - 1, end - 1,
- Command.RefInfo(
- Position.get_file(atts),
- Position.get_line(atts),
- Position.get_id(atts),
- Position.get_offset(atts))))
- case _ => state
- }
- }
- else {
- state.add_markup(
- command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
- }
- case _ => state
- }
- case _ =>
- System.err.println("ignored status report: " + elem)
- state
- })
- case _ => add_result(message)
- }
- if (!(this eq changed)) session.command_change.event(command)
- changed
- }
+ }
+ else {
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
+ }
+ case _ => state
+ }
+ case _ =>
+ System.err.println("ignored status report: " + elem)
+ state
+ })
+ case _ => add_result(message)
+ }
}
--- a/src/Pure/System/isabelle_process.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu May 27 13:13:30 2010 +0200
@@ -161,7 +161,7 @@
if (proc == 0) error("Cannot kill Isabelle: no process")
else {
try_close()
- Thread.sleep(500)
+ Thread.sleep(500) // FIXME property!?
put_result(Kind.SIGNAL, "KILL")
proc.destroy
proc = null
@@ -391,7 +391,7 @@
new Thread("isabelle: exit") {
override def run() = {
val rc = proc.waitFor()
- Thread.sleep(300)
+ Thread.sleep(300) // FIXME property!?
put_result(Kind.SYSTEM, "Exit thread terminated")
put_result(Kind.EXIT, rc.toString)
rm_fifo()
--- a/src/Pure/System/isabelle_system.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu May 27 13:13:30 2010 +0200
@@ -215,12 +215,12 @@
catch { case _: IOException => None }
if (pid.isDefined) {
var running = true
- var count = 10
+ var count = 10 // FIXME property!?
while (running && count > 0) {
if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
running = false
else {
- Thread.sleep(100)
+ Thread.sleep(100) // FIXME property!?
if (!strict) count -= 1
}
}
--- a/src/Pure/System/session.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Pure/System/session.scala Thu May 27 13:13:30 2010 +0200
@@ -25,7 +25,7 @@
trait Entity
{
val id: Entity_ID
- def consume(session: Session, message: XML.Tree): Unit
+ def consume(message: XML.Tree, forward: Command => Unit): Unit
}
}
@@ -37,9 +37,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]
+ val commands_changed = new Event_Bus[Command_Set]
/* unique ids */
@@ -66,7 +64,7 @@
private case object Stop
private case class Begin_Document(path: String)
- private val session_actor = actor {
+ private lazy val session_actor = actor {
var prover: Isabelle_Process with Isar_Document = null
@@ -118,7 +116,7 @@
case None => None
case Some(id) => lookup_entity(id)
}
- if (target.isDefined) target.get.consume(this, result.message)
+ if (target.isDefined) target.get.consume(result.message, indicate_command_change)
else if (result.kind == Isabelle_Process.Kind.STATUS) {
// global status message
result.body match {
@@ -239,6 +237,52 @@
}
+
+ /** buffered command changes -- delay_first discipline **/
+
+ private lazy val command_change_buffer = actor {
+ import scala.compat.Platform.currentTime
+
+ var changed: Set[Command] = Set()
+ var flush_time: Option[Long] = None
+
+ def flush_timeout: Long =
+ flush_time match {
+ case None => 5000L
+ case Some(time) => (time - currentTime) max 0
+ }
+
+ def flush()
+ {
+ if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
+ changed = Set()
+ flush_time = None
+ }
+
+ def invoke()
+ {
+ val now = currentTime
+ flush_time match {
+ case None => flush_time = Some(now + 100) // FIXME output_delay property
+ case Some(time) => if (now >= time) flush()
+ }
+ }
+
+ loop {
+ reactWithin(flush_timeout) {
+ case command: Command => changed += command; invoke()
+ case TIMEOUT => flush()
+ case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def indicate_command_change(command: Command)
+ {
+ command_change_buffer ! command
+ }
+
+
/* main methods */
def start(timeout: Int, args: List[String]): Option[String] =
--- a/src/Tools/jEdit/src/jedit/document_model.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu May 27 13:13:30 2010 +0200
@@ -95,7 +95,7 @@
private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
- private val edits_delay = Swing_Thread.delay_last(300) {
+ private val edits_delay = Swing_Thread.delay_last(300) { // FIXME input_delay property
if (!edits_buffer.isEmpty) {
val new_change = current_change().edit(session, edits_buffer.toList)
edits_buffer.clear
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu May 27 13:13:30 2010 +0200
@@ -69,7 +69,7 @@
}
-class Document_View(model: Document_Model, text_area: TextArea)
+class Document_View(val model: Document_Model, text_area: TextArea)
{
private val session = model.session
@@ -79,38 +79,22 @@
@volatile private var document = model.recent_document()
- /* buffer of changed commands -- owned by Swing thread */
-
- @volatile private var changed_commands: Set[Command] = Set()
+ /* commands_changed_actor */
- private val changed_delay = Swing_Thread.delay_first(100) {
- if (!changed_commands.isEmpty) {
- document = model.recent_document()
- for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
- update_syntax(cmd)
- invalidate_line(cmd)
- overview.repaint()
- }
- changed_commands = Set()
- }
- }
-
-
- /* command change actor */
-
- private case object Exit
-
- private val command_change_actor = actor {
+ private val commands_changed_actor = actor {
loop {
react {
- case command: Command => // FIXME rough filtering according to document family!?
+ case Command_Set(changed) =>
Swing_Thread.now {
- changed_commands += command
- changed_delay()
+ document = model.recent_document()
+ // FIXME cover doc states as well!!?
+ for (command <- changed if document.commands.contains(command)) {
+ update_syntax(command)
+ invalidate_line(command)
+ overview.repaint()
+ }
}
- case Exit => reply(()); exit()
-
case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
}
}
@@ -153,24 +137,23 @@
}
- /* caret_listener */
+ /* caret handling */
- private var _selected_command: Command = null
- private def selected_command = _selected_command
- private def selected_command_=(cmd: Command)
- {
- _selected_command = cmd
- session.results.event(cmd)
- }
+ def selected_command: Option[Command] =
+ document.command_at(text_area.getCaretPosition) match {
+ case Some((command, _)) => Some(command)
+ case None => None
+ }
private val caret_listener = new CaretListener
{
+ private var last_selected_command: Option[Command] = None
override def caretUpdate(e: CaretEvent)
{
- document.command_at(e.getDot) match {
- case Some((command, command_start)) if (selected_command != command) =>
- selected_command = command
- case _ =>
+ val selected = selected_command
+ if (selected != last_selected_command) {
+ last_selected_command = selected
+ if (selected.isDefined) session.indicate_command_change(selected.get)
}
}
}
@@ -179,6 +162,7 @@
/* (re)painting */
private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
+ // FIXME update_delay property
private def update_syntax(cmd: Command)
{
@@ -192,9 +176,6 @@
{
val (start, stop) = model.lines_of_command(document, cmd)
text_area.invalidateLineRange(start, stop)
-
- if (selected_command == cmd)
- session.results.event(cmd)
}
private def invalidate_all() =
@@ -289,13 +270,12 @@
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
- session.command_change += command_change_actor
+ session.commands_changed += commands_changed_actor
}
private def deactivate()
{
- session.command_change -= command_change_actor
- command_change_actor !? Exit
+ session.commands_changed -= commands_changed_actor
text_area.removeLeftOfScrollBar(overview)
text_area.removeCaretListener(caret_listener)
text_area.getPainter.removeExtension(text_area_extension)
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 27 08:02:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 27 13:13:30 2010 +0200
@@ -22,74 +22,61 @@
class Output_Dockable(view: View, position: String) extends Dockable(view, position)
{
+ Swing_Thread.assert()
+
val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
add(html_panel, BorderLayout.CENTER)
- /* controls */
-
- private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
- zoom.tooltip = "Zoom factor for basic font size"
-
- private val update = new Button("Update") {
- reactions += { case ButtonClicked(_) => handle_update() }
- }
- update.tooltip =
- "<html>Update display according to the<br>state of command at caret position</html>"
-
- private val tracing = new CheckBox("Tracing") {
- reactions += { case ButtonClicked(_) => handle_update() }
- }
- tracing.tooltip =
- "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
+ /* component state -- owned by Swing thread */
- private val debug = new CheckBox("Debug") {
- reactions += { case ButtonClicked(_) => handle_update() }
- }
- debug.tooltip =
- "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
+ private var zoom_factor = 100
+ private var show_debug = false
+ private var show_tracing = false
+ private var follow_caret = true
+ private var current_command: Option[Command] = None
- private val follow = new CheckBox("Follow")
- follow.selected = true
- follow.tooltip =
- "<html>Indicate automatic update following<br>caret movement or state changes</html>"
- private def filtered_results(document: Document, cmd: Command): List[XML.Tree] =
+ private def handle_resize()
{
- val show_tracing = tracing.selected
- val show_debug = debug.selected
- document.current_state(cmd).results filter {
- case XML.Elem(Markup.TRACING, _, _) => show_tracing
- case XML.Elem(Markup.DEBUG, _, _) => show_debug
- case _ => true
+ Swing_Thread.now {
+ html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
}
}
- private case class Render(body: List[XML.Tree])
+ private def handle_caret()
+ {
+ Swing_Thread.now {
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) => current_command = doc_view.selected_command
+ case None =>
+ }
+ }
+ }
- private def handle_update()
+ private def handle_update(restriction: Option[Set[Command]] = None)
{
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, _)) =>
- main_actor ! Render(filtered_results(document, cmd))
- case None =>
+ if (follow_caret) handle_caret()
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ current_command match {
+ case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
+ val document = doc_view.model.recent_document
+ val filtered_results =
+ document.current_state(cmd).results filter {
+ case XML.Elem(Markup.TRACING, _, _) => show_tracing
+ case XML.Elem(Markup.DEBUG, _, _) => show_debug
+ case _ => true
+ }
+ html_panel.render(filtered_results)
+ case _ =>
}
case None =>
}
}
}
- private var zoom_factor = 100
-
- private def handle_resize() =
- Swing_Thread.now {
- html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
- }
-
/* main actor */
@@ -97,17 +84,7 @@
loop {
react {
case Session.Global_Settings => handle_resize()
- case Render(body) => html_panel.render(body)
-
- case cmd: Command =>
- Swing_Thread.now {
- if (follow.selected) Document_Model(view.getBuffer) else None
- } match {
- case None =>
- case Some(model) =>
- html_panel.render(filtered_results(model.recent_document, cmd))
- }
-
+ case Command_Set(changed) => handle_update(Some(changed))
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}
}
@@ -115,13 +92,13 @@
override def init()
{
- Isabelle.session.results += main_actor
+ Isabelle.session.commands_changed += main_actor
Isabelle.session.global_settings += main_actor
}
override def exit()
{
- Isabelle.session.results -= main_actor
+ Isabelle.session.commands_changed -= main_actor
Isabelle.session.global_settings -= main_actor
}
@@ -129,14 +106,42 @@
/* resize */
addComponentListener(new ComponentAdapter {
- val delay = Swing_Thread.delay_last(500) { handle_resize() }
+ val delay = Swing_Thread.delay_last(500) { handle_resize() } // FIXME update_delay property
override def componentResized(e: ComponentEvent) { delay() }
})
- /* init controls */
+ /* controls */
+
+ private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+ zoom.tooltip = "Zoom factor for basic font size"
+
+ private val debug = new CheckBox("Debug") {
+ reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
+ }
+ debug.selected = show_debug
+ debug.tooltip =
+ "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
- val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow)
+ private val tracing = new CheckBox("Tracing") {
+ reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
+ }
+ tracing.selected = show_tracing
+ tracing.tooltip =
+ "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
+
+ private val auto_update = new CheckBox("Auto update") {
+ reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
+ }
+ auto_update.selected = follow_caret
+ auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
+
+ private val update = new Button("Update") {
+ reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
+ }
+ update.tooltip = "<html>Update display according to the command at cursor position</html>"
+
+ val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
add(controls.peer, BorderLayout.NORTH)
handle_update()