--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Dec 29 20:43:04 2008 +0100
@@ -24,7 +24,7 @@
var textarea : JEditTextArea = null
val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
- prover.commandInfo.add(cc => repaint_delay.delay_or_ignore())
+ prover.command_info += (_ => repaint_delay.delay_or_ignore())
setRequestFocusEnabled(false);
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Mon Dec 29 20:43:04 2008 +0100
@@ -14,7 +14,6 @@
import scala.collection.mutable.HashMap
-import isabelle.utils.EventSource
import isabelle.prover.{Prover, Command}
import isabelle.{IsabelleSystem, Symbol}
@@ -55,17 +54,12 @@
// Isabelle font
var font: Font = null
- val font_changed = new EventSource[Font]
+ val font_changed = new EventBus[Font]
def set_font(path: String, size: Float) {
- try {
- font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
- deriveFont(Font.PLAIN, size)
- font_changed.fire(font)
- }
- catch {
- case e: IOException =>
- }
+ font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
+ deriveFont(Font.PLAIN, size)
+ font_changed.event(font)
}
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Dec 29 20:43:04 2008 +0100
@@ -7,7 +7,6 @@
package isabelle.jedit
-import isabelle.utils.EventSource
import isabelle.prover.{Prover, Command}
import isabelle.renderer.UserAgent
@@ -21,34 +20,30 @@
import javax.swing.{JTextArea, JScrollPane}
-class ProverSetup(buffer : JEditBuffer) {
-
+class ProverSetup(buffer: JEditBuffer)
+{
val prover = new Prover(Isabelle.system, Isabelle.symbols)
- var theory_view : TheoryView = null
-
- private var _selectedState : Command = null
+ var theory_view: TheoryView = null
- val stateUpdate = new EventSource[Command]
+ val state_update = new EventBus[Command]
- def selectedState = _selectedState
- def selectedState_=(newState : Command) {
- _selectedState = newState
- stateUpdate fire newState
- }
+ private var _selected_state: Command = null
+ def selected_state = _selected_state
+ def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
- val output_text_view = new JTextArea("== Isabelle output ==\n")
-
- def activate(view : View) {
- val logic = Isabelle.property("logic")
- prover.start(if (logic == null) logic else "HOL") // FIXME avoid hardwired logic
+ val output_text_view = new JTextArea
+
+ def activate(view: View) {
+ prover.start(Isabelle.property("logic"))
val buffer = view.getBuffer
- val dir = buffer.getDirectory()
+ val dir = buffer.getDirectory
theory_view = new TheoryView(view.getTextArea)
- prover.setDocument(theory_view ,
- if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
+ prover.set_document(theory_view,
+ if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
theory_view.activate
- prover.outputInfo.add( text => {
+ prover.output_info += (text =>
+ {
output_text_view.append(text)
val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
//link process output if dockable is active
@@ -61,19 +56,21 @@
}
}
})
-
+
//register for state-view
- stateUpdate.add(state => {
+ state_update += (state => {
val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
- val state_panel = if(state_view != null) state_view.asInstanceOf[StateViewDockable].panel else null
- if(state_panel != null){
+ val state_panel =
+ if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
+ else null
+ if (state_panel != null){
if (state == null)
- state_panel.setDocument(null : Document)
+ state_panel.setDocument(null: Document)
else
state_panel.setDocument(state.results_xml, UserAgent.baseURL)
}
})
-
+
//register for theory-view
// could also use this:
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Dec 29 20:43:04 2008 +0100
@@ -8,8 +8,6 @@
import isabelle.IsabelleProcess.Result
-import isabelle.YXML.parse_failsafe
-import isabelle.utils.EventSource
import isabelle.renderer.UserAgent
@@ -225,12 +223,12 @@
if (Isabelle.plugin.font != null)
fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
- Isabelle.plugin.font_changed.add(font => {
+ Isabelle.plugin.font_changed += (font => {
if (Isabelle.plugin.font != null)
fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
panel.relayout()
})
- val tree = parse_failsafe(Isabelle.symbols.decode(r.result))
+ val tree = YXML.parse_failsafe(Isabelle.symbols.decode(r.result))
val document = XML.document(tree)
panel.setDocument(document, UserAgent.baseURL)
val sa = new SelectionActions
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 29 20:43:04 2008 +0100
@@ -66,7 +66,7 @@
if (Isabelle.plugin.font != null)
fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
- Isabelle.plugin.font_changed.add(font => {
+ Isabelle.plugin.font_changed += (font => {
if (Isabelle.plugin.font != null)
fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 29 20:43:04 2008 +0100
@@ -9,7 +9,6 @@
package isabelle.jedit
-import isabelle.utils.EventSource
import isabelle.proofdocument.Text
import isabelle.prover.{Prover, Command}
import isabelle.prover.Command.Phase
@@ -86,13 +85,13 @@
col_timer.setRepeats(true)
- private val changes_source = new EventSource[Text.Changed]
+ private val changes_bus = new EventBus[Text.Changed]
private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
/* activation */
- Isabelle.plugin.font_changed.add(font => update_font())
+ Isabelle.plugin.font_changed += (_ => update_font())
private def update_font() = {
if (text_area != null) {
@@ -111,8 +110,8 @@
override def caretUpdate(e: CaretEvent) = {
val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
if (cmd != null && cmd.start <= e.getDot &&
- Isabelle.prover_setup(buffer).selectedState != cmd)
- Isabelle.prover_setup(buffer).selectedState = cmd
+ Isabelle.prover_setup(buffer).selected_state != cmd)
+ Isabelle.prover_setup(buffer).selected_state = cmd
}
}
@@ -134,7 +133,7 @@
/* painting */
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
- Isabelle.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
+ Isabelle.prover(buffer).command_info += (_ => repaint_delay.delay_or_ignore())
private def from_current(pos: Int) =
if (col != null && col.start <= pos)
@@ -156,8 +155,8 @@
val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
text_area.invalidateLineRange(start, stop)
- if (Isabelle.prover_setup(buffer).selectedState == cmd)
- Isabelle.prover_setup(buffer).selectedState = cmd // update State view
+ if (Isabelle.prover_setup(buffer).selected_state == cmd)
+ Isabelle.prover_setup(buffer).selected_state = cmd // update State view
}
}
@@ -223,7 +222,7 @@
def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
def length = buffer.getLength
- def changes = changes_source
+ def changes = changes_bus
@@ -231,7 +230,7 @@
private def commit() {
if (col != null)
- changes.fire(col)
+ changes.event(col)
col = null
if (col_timer.isRunning())
col_timer.stop()
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Dec 29 20:43:04 2008 +0100
@@ -8,7 +8,6 @@
import java.util.regex.Pattern
-import isabelle.utils.EventSource
object ProofDocument {
// Be carefully when changeing this regex. Not only must it handle the
@@ -36,15 +35,14 @@
protected var lastToken : Token[C] = null
private var active = false
- {
- text.changes.add(e => textChanged(e.start, e.added, e.removed))
- }
+ text.changes += (e => textChanged(e.start, e.added, e.removed))
- def activate() : Unit =
- if (! active) {
+ def activate() {
+ if (!active) {
active = true
textChanged(0, text.length, 0)
}
+ }
protected def tokens(start : Token[C], stop : Token[C]) =
new Iterator[Token[C]]() {
@@ -224,7 +222,7 @@
tokenChanged(beforeChange, afterChange, firstRemoved)
}
- protected def isStartKeyword(str : String) : Boolean;
+ protected def isStartKeyword(str: String): Boolean
protected def tokenChanged(start : Token[C], stop : Token[C],
removed : Token[C])
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Mon Dec 29 20:43:04 2008 +0100
@@ -6,15 +6,13 @@
package isabelle.proofdocument
-import isabelle.utils.EventSource
object Text {
- class Changed(val start : Int, val added : Int, val removed : Int)
+ class Changed(val start: Int, val added: Int, val removed: Int)
}
trait Text {
- def content(start : Int, stop : Int) : String
- def length : Int
-
- def changes : EventSource[Text.Changed]
+ def content(start: Int, stop: Int): String
+ def length: Int
+ def changes: EventBus[Text.Changed]
}
--- a/src/Tools/jEdit/src/prover/Document.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Mon Dec 29 20:43:04 2008 +0100
@@ -6,9 +6,8 @@
package isabelle.prover
-import isabelle.proofdocument.{ ProofDocument, Token, Text }
+import isabelle.proofdocument.{ProofDocument, Token, Text}
-import isabelle.utils.EventSource
object Document {
class StructureChange(val beforeChange : Command,
@@ -16,20 +15,21 @@
val removedCommands : List[Command])
}
+
class Document(text : Text, val prover : Prover) extends ProofDocument[Command](text)
-{
- val structuralChanges = new EventSource[Document.StructureChange]()
-
+{
+ val structural_changes = new EventBus[Document.StructureChange]
+
def isStartKeyword(s : String) = prover.command_decls.contains(s)
-
+
def commands() = new Iterator[Command] {
var current = firstToken
def hasNext() = current != null
def next() = { try {val s = current.command ; current = s.last.next ; s}
- catch { case error : NullPointerException =>
+ catch { case error : NullPointerException =>
System.err.println("NPE!")
throw error
- }
+ }
}
}
@@ -39,13 +39,13 @@
for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
return null
}
-
- override def tokenChanged(start : Token[Command], stop : Token[Command],
+
+ override def tokenChanged(start : Token[Command], stop : Token[Command],
removed : Token[Command]) {
var removedCommands : List[Command] = Nil
var first : Command = null
var last : Command = null
-
+
for(t <- tokens(removed)) {
if (first == null)
first = t.command
@@ -65,7 +65,7 @@
else
before = first.previous
}
-
+
var addedCommands : List[Command] = Nil
var scan : Token[Command] = null
if (start != null) {
@@ -96,7 +96,7 @@
}
else
scan = firstToken
-
+
var stopScan : Token[Command] = null
if (stop != null) {
if (stop == stop.command.first)
@@ -108,19 +108,19 @@
stopScan = last.last.next
else
stopScan = null
-
+
var cmdStart : Token[Command] = null
var cmdStop : Token[Command] = null
var overrun = false
var finished = false
while (scan != null && !finished) {
- if (scan == stopScan) {
+ if (scan == stopScan) {
if (scan.kind.equals(Token.Kind.COMMAND_START))
finished = true
else
overrun = true
}
-
+
if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
if (! overrun) {
addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
@@ -140,19 +140,19 @@
removedCommands = scan.command :: removedCommands
last = scan.command
}
-
+
if (!finished)
scan = scan.next
}
-
+
if (cmdStart != null)
addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
-
+
// relink commands
addedCommands = addedCommands.reverse
removedCommands = removedCommands.reverse
-
- structuralChanges.fire(new Document.StructureChange(before, addedCommands,
- removedCommands))
+
+ structural_changes.event(
+ new Document.StructureChange(before, addedCommands, removedCommands))
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Mon Dec 29 20:36:34 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Dec 29 20:43:04 2008 +0100
@@ -10,15 +10,12 @@
import java.util.Properties
-import javax.swing.SwingUtilities
import scala.collection.mutable.{HashMap, HashSet}
+import org.gjt.sp.util.Log
+
import isabelle.proofdocument.{ProofDocument, Text, Token}
-import isabelle.{Symbol, IsabelleSyntax}
-import isabelle.utils.EventSource
-
-import Command.Phase
class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation)
@@ -31,39 +28,32 @@
val keyword_decls = new HashSet[String]
private var initialized = false
- val activated = new EventSource[Unit]
- val commandInfo = new EventSource[Command]
- val outputInfo = new EventSource[String]
+ val activated = new EventBus[Unit]
+ val command_info = new EventBus[Command]
+ val output_info = new EventBus[String]
var document: Document = null
- def swing(body: => Unit) =
- SwingUtilities.invokeAndWait(new Runnable { def run = body })
-
- def swing_async(body: => Unit) =
- SwingUtilities.invokeLater(new Runnable { def run = body })
-
-
- def fireChange(c: Command) = swing { commandInfo.fire(c) }
+ def command_change(c: Command) = Swing.now { command_info.event(c) }
private def handle_result(r: IsabelleProcess.Result) = {
val id = if (r.props != null) r.props.getProperty(Markup.ID) else null
val st = if (id != null) commands.getOrElse(id, null) else null
if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
- swing { outputInfo.fire(r.result) }
+ Swing.now { output_info.event(r.result) }
else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
initialized = true
- swing {
+ Swing.now {
if (document != null) {
document.activate()
- activated.fire(())
+ activated.event(())
}
}
}
else {
val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
- if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)) {
+ if (st == null || (st.phase != Command.Phase.REMOVED && st.phase != Command.Phase.REMOVE)) {
r.kind match {
case IsabelleProcess.Kind.STATUS =>
@@ -75,24 +65,24 @@
//{{{
// command status
case XML.Elem(Markup.FINISHED, _, _) =>
- st.phase = Phase.FINISHED
- fireChange(st)
+ st.phase = Command.Phase.FINISHED
+ command_change(st)
case XML.Elem(Markup.UNPROCESSED, _, _) =>
- st.phase = Phase.UNPROCESSED
- fireChange(st)
+ st.phase = Command.Phase.UNPROCESSED
+ command_change(st)
case XML.Elem(Markup.FAILED, _, _) =>
- st.phase = Phase.FAILED
- fireChange(st)
+ st.phase = Command.Phase.FAILED
+ command_change(st)
case XML.Elem(Markup.DISPOSED, _, _) =>
document.prover.commands.removeKey(st.id)
- st.phase = Phase.REMOVED
- fireChange(st)
+ st.phase = Command.Phase.REMOVED
+ command_change(st)
// command and keyword declarations
- case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, _)), _) =>
- command_decls.addEntry(name)
- case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) =>
- keyword_decls.addEntry(name)
+ case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) =>
+ command_decls += name
+ case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+ keyword_decls += name
// other markup
case XML.Elem(kind,
@@ -117,15 +107,15 @@
//}}}
case IsabelleProcess.Kind.ERROR if st != null =>
- if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
- st.phase = Phase.FAILED
+ if (st.phase != Command.Phase.REMOVED && st.phase != Command.Phase.REMOVE)
+ st.phase = Command.Phase.FAILED
st.add_result(tree)
- fireChange(st)
+ command_change(st)
case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
| IsabelleProcess.Kind.WARNING if st != null =>
st.add_result(tree)
- fireChange(st)
+ command_change(st)
case _ =>
}
@@ -135,8 +125,12 @@
def start(logic: String) {
- val results = new EventBus[IsabelleProcess.Result] + handle_result
if (logic != null) _logic = logic
+
+ val results = new EventBus[IsabelleProcess.Result]
+ results += handle_result
+ results.logger = Log.log(Log.ERROR, null, _)
+
process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
}
@@ -144,22 +138,22 @@
process.kill
}
- def setDocument(text: Text, path: String) {
+ def set_document(text: Text, path: String) {
this.document = new Document(text, this)
process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
- document.structuralChanges.add(changes => {
+ document.structural_changes += (changes => {
for (cmd <- changes.removedCommands) remove(cmd)
for (cmd <- changes.addedCommands) send(cmd)
})
if (initialized) {
document.activate()
- activated.fire(())
+ activated.event(())
}
}
private def send(cmd: Command) {
- cmd.phase = Phase.UNPROCESSED
+ cmd.phase = Command.Phase.UNPROCESSED
commands.put(cmd.id, cmd)
val props = new Properties
@@ -172,7 +166,7 @@
}
def remove(cmd: Command) {
- cmd.phase = Phase.REMOVE
+ cmd.phase = Command.Phase.REMOVE
process.remove_command(cmd.id)
}
}