# HG changeset patch
# User wenzelm
# Date 1230579784 -3600
# Node ID 14367c0715e8533fb74916824e4385c8b49f899c
# Parent  4900605ebd0c7c7c81a9de190c0ab7a489a3d0fe
replaced EventSource by EventBus;
misc tuning;

diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- 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);
 
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/jedit/Plugin.scala
--- 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)
   }
 
 
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- 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:
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- 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
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- 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)
 
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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()
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- 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]) 
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/proofdocument/Text.scala
--- 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]
 }
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/prover/Document.scala
--- 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))
   }
 }
diff -r 4900605ebd0c -r 14367c0715e8 src/Tools/jEdit/src/prover/Prover.scala
--- 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)
   }
 }