# HG changeset patch # User wenzelm # Date 1274958810 -7200 # Node ID 56e1b6976d0e2b43d531206eca005b363c83dec6 # Parent 8d231d3efcde7e0bdfe2c1d4f303bee8e9278acb# Parent 10ef4da1c314673919d05286a240615b505f394f merged diff -r 8d231d3efcde -r 56e1b6976d0e src/Pure/PIDE/command.scala --- 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) "" else "" + override def toString = + if (is_command) name + "(" + id + ")" + else if (is_ignored) "" else "" /* 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 diff -r 8d231d3efcde -r 56e1b6976d0e src/Pure/PIDE/state.scala --- 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) + } } diff -r 8d231d3efcde -r 56e1b6976d0e src/Pure/System/isabelle_process.scala --- 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() diff -r 8d231d3efcde -r 56e1b6976d0e src/Pure/System/isabelle_system.scala --- 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 } } diff -r 8d231d3efcde -r 56e1b6976d0e src/Pure/System/session.scala --- 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] = diff -r 8d231d3efcde -r 56e1b6976d0e src/Tools/jEdit/src/jedit/document_model.scala --- 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 diff -r 8d231d3efcde -r 56e1b6976d0e src/Tools/jEdit/src/jedit/document_view.scala --- 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) diff -r 8d231d3efcde -r 56e1b6976d0e src/Tools/jEdit/src/jedit/output_dockable.scala --- 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 = - "Update display according to the
state of command at caret position" - - private val tracing = new CheckBox("Tracing") { - reactions += { case ButtonClicked(_) => handle_update() } - } - tracing.tooltip = - "Indicate output of tracing messages
(also needs to be enabled on the prover side)" + /* component state -- owned by Swing thread */ - private val debug = new CheckBox("Debug") { - reactions += { case ButtonClicked(_) => handle_update() } - } - debug.tooltip = - "Indicate output of debug messages
(also needs to be enabled on the prover side)" + 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 = - "Indicate automatic update following
caret movement or state changes" - 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 = + "Indicate output of debug messages
(also needs to be enabled on the prover side)" - 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 = + "Indicate output of tracing messages
(also needs to be enabled on the prover side)" + + 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 = "Indicate automatic update following cursor movement" + + private val update = new Button("Update") { + reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } + } + update.tooltip = "Update display according to the command at cursor position" + + val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) add(controls.peer, BorderLayout.NORTH) handle_update()