1.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Dec 29 20:36:34 2008 +0100
1.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Dec 29 20:43:04 2008 +0100
1.3 @@ -24,7 +24,7 @@
1.4 var textarea : JEditTextArea = null
1.5
1.6 val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
1.7 - prover.commandInfo.add(cc => repaint_delay.delay_or_ignore())
1.8 + prover.command_info += (_ => repaint_delay.delay_or_ignore())
1.9
1.10 setRequestFocusEnabled(false);
1.11
2.1 --- a/src/Tools/jEdit/src/jedit/Plugin.scala Mon Dec 29 20:36:34 2008 +0100
2.2 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala Mon Dec 29 20:43:04 2008 +0100
2.3 @@ -14,7 +14,6 @@
2.4
2.5 import scala.collection.mutable.HashMap
2.6
2.7 -import isabelle.utils.EventSource
2.8 import isabelle.prover.{Prover, Command}
2.9 import isabelle.{IsabelleSystem, Symbol}
2.10
2.11 @@ -55,17 +54,12 @@
2.12 // Isabelle font
2.13
2.14 var font: Font = null
2.15 - val font_changed = new EventSource[Font]
2.16 + val font_changed = new EventBus[Font]
2.17
2.18 def set_font(path: String, size: Float) {
2.19 - try {
2.20 - font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
2.21 - deriveFont(Font.PLAIN, size)
2.22 - font_changed.fire(font)
2.23 - }
2.24 - catch {
2.25 - case e: IOException =>
2.26 - }
2.27 + font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
2.28 + deriveFont(Font.PLAIN, size)
2.29 + font_changed.event(font)
2.30 }
2.31
2.32
3.1 --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Dec 29 20:36:34 2008 +0100
3.2 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Dec 29 20:43:04 2008 +0100
3.3 @@ -7,7 +7,6 @@
3.4 package isabelle.jedit
3.5
3.6
3.7 -import isabelle.utils.EventSource
3.8 import isabelle.prover.{Prover, Command}
3.9 import isabelle.renderer.UserAgent
3.10
3.11 @@ -21,34 +20,30 @@
3.12 import javax.swing.{JTextArea, JScrollPane}
3.13
3.14
3.15 -class ProverSetup(buffer : JEditBuffer) {
3.16 +class ProverSetup(buffer: JEditBuffer)
3.17 +{
3.18 + val prover = new Prover(Isabelle.system, Isabelle.symbols)
3.19 + var theory_view: TheoryView = null
3.20
3.21 - val prover = new Prover(Isabelle.system, Isabelle.symbols)
3.22 - var theory_view : TheoryView = null
3.23 -
3.24 - private var _selectedState : Command = null
3.25 + val state_update = new EventBus[Command]
3.26
3.27 - val stateUpdate = new EventSource[Command]
3.28 + private var _selected_state: Command = null
3.29 + def selected_state = _selected_state
3.30 + def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
3.31
3.32 - def selectedState = _selectedState
3.33 - def selectedState_=(newState : Command) {
3.34 - _selectedState = newState
3.35 - stateUpdate fire newState
3.36 - }
3.37 + val output_text_view = new JTextArea
3.38
3.39 - val output_text_view = new JTextArea("== Isabelle output ==\n")
3.40 -
3.41 - def activate(view : View) {
3.42 - val logic = Isabelle.property("logic")
3.43 - prover.start(if (logic == null) logic else "HOL") // FIXME avoid hardwired logic
3.44 + def activate(view: View) {
3.45 + prover.start(Isabelle.property("logic"))
3.46 val buffer = view.getBuffer
3.47 - val dir = buffer.getDirectory()
3.48 + val dir = buffer.getDirectory
3.49
3.50 theory_view = new TheoryView(view.getTextArea)
3.51 - prover.setDocument(theory_view ,
3.52 - if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
3.53 + prover.set_document(theory_view,
3.54 + if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
3.55 theory_view.activate
3.56 - prover.outputInfo.add( text => {
3.57 + prover.output_info += (text =>
3.58 + {
3.59 output_text_view.append(text)
3.60 val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
3.61 //link process output if dockable is active
3.62 @@ -61,19 +56,21 @@
3.63 }
3.64 }
3.65 })
3.66 -
3.67 +
3.68 //register for state-view
3.69 - stateUpdate.add(state => {
3.70 + state_update += (state => {
3.71 val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
3.72 - val state_panel = if(state_view != null) state_view.asInstanceOf[StateViewDockable].panel else null
3.73 - if(state_panel != null){
3.74 + val state_panel =
3.75 + if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
3.76 + else null
3.77 + if (state_panel != null){
3.78 if (state == null)
3.79 - state_panel.setDocument(null : Document)
3.80 + state_panel.setDocument(null: Document)
3.81 else
3.82 state_panel.setDocument(state.results_xml, UserAgent.baseURL)
3.83 }
3.84 })
3.85 -
3.86 +
3.87 //register for theory-view
3.88
3.89 // could also use this:
4.1 --- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Dec 29 20:36:34 2008 +0100
4.2 +++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Dec 29 20:43:04 2008 +0100
4.3 @@ -8,8 +8,6 @@
4.4
4.5
4.6 import isabelle.IsabelleProcess.Result
4.7 -import isabelle.YXML.parse_failsafe
4.8 -import isabelle.utils.EventSource
4.9 import isabelle.renderer.UserAgent
4.10
4.11
4.12 @@ -225,12 +223,12 @@
4.13 if (Isabelle.plugin.font != null)
4.14 fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
4.15
4.16 - Isabelle.plugin.font_changed.add(font => {
4.17 + Isabelle.plugin.font_changed += (font => {
4.18 if (Isabelle.plugin.font != null)
4.19 fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
4.20 panel.relayout()
4.21 })
4.22 - val tree = parse_failsafe(Isabelle.symbols.decode(r.result))
4.23 + val tree = YXML.parse_failsafe(Isabelle.symbols.decode(r.result))
4.24 val document = XML.document(tree)
4.25 panel.setDocument(document, UserAgent.baseURL)
4.26 val sa = new SelectionActions
5.1 --- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 29 20:36:34 2008 +0100
5.2 +++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 29 20:43:04 2008 +0100
5.3 @@ -66,7 +66,7 @@
5.4 if (Isabelle.plugin.font != null)
5.5 fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
5.6
5.7 - Isabelle.plugin.font_changed.add(font => {
5.8 + Isabelle.plugin.font_changed += (font => {
5.9 if (Isabelle.plugin.font != null)
5.10 fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
5.11
6.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 29 20:36:34 2008 +0100
6.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 29 20:43:04 2008 +0100
6.3 @@ -9,7 +9,6 @@
6.4 package isabelle.jedit
6.5
6.6
6.7 -import isabelle.utils.EventSource
6.8 import isabelle.proofdocument.Text
6.9 import isabelle.prover.{Prover, Command}
6.10 import isabelle.prover.Command.Phase
6.11 @@ -86,13 +85,13 @@
6.12 col_timer.setRepeats(true)
6.13
6.14
6.15 - private val changes_source = new EventSource[Text.Changed]
6.16 + private val changes_bus = new EventBus[Text.Changed]
6.17 private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
6.18
6.19
6.20 /* activation */
6.21
6.22 - Isabelle.plugin.font_changed.add(font => update_font())
6.23 + Isabelle.plugin.font_changed += (_ => update_font())
6.24
6.25 private def update_font() = {
6.26 if (text_area != null) {
6.27 @@ -111,8 +110,8 @@
6.28 override def caretUpdate(e: CaretEvent) = {
6.29 val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
6.30 if (cmd != null && cmd.start <= e.getDot &&
6.31 - Isabelle.prover_setup(buffer).selectedState != cmd)
6.32 - Isabelle.prover_setup(buffer).selectedState = cmd
6.33 + Isabelle.prover_setup(buffer).selected_state != cmd)
6.34 + Isabelle.prover_setup(buffer).selected_state = cmd
6.35 }
6.36 }
6.37
6.38 @@ -134,7 +133,7 @@
6.39 /* painting */
6.40
6.41 val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
6.42 - Isabelle.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
6.43 + Isabelle.prover(buffer).command_info += (_ => repaint_delay.delay_or_ignore())
6.44
6.45 private def from_current(pos: Int) =
6.46 if (col != null && col.start <= pos)
6.47 @@ -156,8 +155,8 @@
6.48 val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
6.49 text_area.invalidateLineRange(start, stop)
6.50
6.51 - if (Isabelle.prover_setup(buffer).selectedState == cmd)
6.52 - Isabelle.prover_setup(buffer).selectedState = cmd // update State view
6.53 + if (Isabelle.prover_setup(buffer).selected_state == cmd)
6.54 + Isabelle.prover_setup(buffer).selected_state = cmd // update State view
6.55 }
6.56 }
6.57
6.58 @@ -223,7 +222,7 @@
6.59
6.60 def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
6.61 def length = buffer.getLength
6.62 - def changes = changes_source
6.63 + def changes = changes_bus
6.64
6.65
6.66
6.67 @@ -231,7 +230,7 @@
6.68
6.69 private def commit() {
6.70 if (col != null)
6.71 - changes.fire(col)
6.72 + changes.event(col)
6.73 col = null
6.74 if (col_timer.isRunning())
6.75 col_timer.stop()
7.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Dec 29 20:36:34 2008 +0100
7.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Dec 29 20:43:04 2008 +0100
7.3 @@ -8,7 +8,6 @@
7.4
7.5 import java.util.regex.Pattern
7.6
7.7 -import isabelle.utils.EventSource
7.8
7.9 object ProofDocument {
7.10 // Be carefully when changeing this regex. Not only must it handle the
7.11 @@ -36,15 +35,14 @@
7.12 protected var lastToken : Token[C] = null
7.13 private var active = false
7.14
7.15 - {
7.16 - text.changes.add(e => textChanged(e.start, e.added, e.removed))
7.17 - }
7.18 + text.changes += (e => textChanged(e.start, e.added, e.removed))
7.19
7.20 - def activate() : Unit =
7.21 - if (! active) {
7.22 + def activate() {
7.23 + if (!active) {
7.24 active = true
7.25 textChanged(0, text.length, 0)
7.26 }
7.27 + }
7.28
7.29 protected def tokens(start : Token[C], stop : Token[C]) =
7.30 new Iterator[Token[C]]() {
7.31 @@ -224,7 +222,7 @@
7.32 tokenChanged(beforeChange, afterChange, firstRemoved)
7.33 }
7.34
7.35 - protected def isStartKeyword(str : String) : Boolean;
7.36 + protected def isStartKeyword(str: String): Boolean
7.37
7.38 protected def tokenChanged(start : Token[C], stop : Token[C],
7.39 removed : Token[C])
8.1 --- a/src/Tools/jEdit/src/proofdocument/Text.scala Mon Dec 29 20:36:34 2008 +0100
8.2 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala Mon Dec 29 20:43:04 2008 +0100
8.3 @@ -6,15 +6,13 @@
8.4
8.5 package isabelle.proofdocument
8.6
8.7 -import isabelle.utils.EventSource
8.8
8.9 object Text {
8.10 - class Changed(val start : Int, val added : Int, val removed : Int)
8.11 + class Changed(val start: Int, val added: Int, val removed: Int)
8.12 }
8.13
8.14 trait Text {
8.15 - def content(start : Int, stop : Int) : String
8.16 - def length : Int
8.17 -
8.18 - def changes : EventSource[Text.Changed]
8.19 + def content(start: Int, stop: Int): String
8.20 + def length: Int
8.21 + def changes: EventBus[Text.Changed]
8.22 }
9.1 --- a/src/Tools/jEdit/src/prover/Document.scala Mon Dec 29 20:36:34 2008 +0100
9.2 +++ b/src/Tools/jEdit/src/prover/Document.scala Mon Dec 29 20:43:04 2008 +0100
9.3 @@ -6,9 +6,8 @@
9.4
9.5 package isabelle.prover
9.6
9.7 -import isabelle.proofdocument.{ ProofDocument, Token, Text }
9.8 +import isabelle.proofdocument.{ProofDocument, Token, Text}
9.9
9.10 -import isabelle.utils.EventSource
9.11
9.12 object Document {
9.13 class StructureChange(val beforeChange : Command,
9.14 @@ -16,20 +15,21 @@
9.15 val removedCommands : List[Command])
9.16 }
9.17
9.18 +
9.19 class Document(text : Text, val prover : Prover) extends ProofDocument[Command](text)
9.20 -{
9.21 - val structuralChanges = new EventSource[Document.StructureChange]()
9.22 -
9.23 +{
9.24 + val structural_changes = new EventBus[Document.StructureChange]
9.25 +
9.26 def isStartKeyword(s : String) = prover.command_decls.contains(s)
9.27 -
9.28 +
9.29 def commands() = new Iterator[Command] {
9.30 var current = firstToken
9.31 def hasNext() = current != null
9.32 def next() = { try {val s = current.command ; current = s.last.next ; s}
9.33 - catch { case error : NullPointerException =>
9.34 + catch { case error : NullPointerException =>
9.35 System.err.println("NPE!")
9.36 throw error
9.37 - }
9.38 + }
9.39 }
9.40 }
9.41
9.42 @@ -39,13 +39,13 @@
9.43 for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
9.44 return null
9.45 }
9.46 -
9.47 - override def tokenChanged(start : Token[Command], stop : Token[Command],
9.48 +
9.49 + override def tokenChanged(start : Token[Command], stop : Token[Command],
9.50 removed : Token[Command]) {
9.51 var removedCommands : List[Command] = Nil
9.52 var first : Command = null
9.53 var last : Command = null
9.54 -
9.55 +
9.56 for(t <- tokens(removed)) {
9.57 if (first == null)
9.58 first = t.command
9.59 @@ -65,7 +65,7 @@
9.60 else
9.61 before = first.previous
9.62 }
9.63 -
9.64 +
9.65 var addedCommands : List[Command] = Nil
9.66 var scan : Token[Command] = null
9.67 if (start != null) {
9.68 @@ -96,7 +96,7 @@
9.69 }
9.70 else
9.71 scan = firstToken
9.72 -
9.73 +
9.74 var stopScan : Token[Command] = null
9.75 if (stop != null) {
9.76 if (stop == stop.command.first)
9.77 @@ -108,19 +108,19 @@
9.78 stopScan = last.last.next
9.79 else
9.80 stopScan = null
9.81 -
9.82 +
9.83 var cmdStart : Token[Command] = null
9.84 var cmdStop : Token[Command] = null
9.85 var overrun = false
9.86 var finished = false
9.87 while (scan != null && !finished) {
9.88 - if (scan == stopScan) {
9.89 + if (scan == stopScan) {
9.90 if (scan.kind.equals(Token.Kind.COMMAND_START))
9.91 finished = true
9.92 else
9.93 overrun = true
9.94 }
9.95 -
9.96 +
9.97 if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
9.98 if (! overrun) {
9.99 addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
9.100 @@ -140,19 +140,19 @@
9.101 removedCommands = scan.command :: removedCommands
9.102 last = scan.command
9.103 }
9.104 -
9.105 +
9.106 if (!finished)
9.107 scan = scan.next
9.108 }
9.109 -
9.110 +
9.111 if (cmdStart != null)
9.112 addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
9.113 -
9.114 +
9.115 // relink commands
9.116 addedCommands = addedCommands.reverse
9.117 removedCommands = removedCommands.reverse
9.118 -
9.119 - structuralChanges.fire(new Document.StructureChange(before, addedCommands,
9.120 - removedCommands))
9.121 +
9.122 + structural_changes.event(
9.123 + new Document.StructureChange(before, addedCommands, removedCommands))
9.124 }
9.125 }
10.1 --- a/src/Tools/jEdit/src/prover/Prover.scala Mon Dec 29 20:36:34 2008 +0100
10.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Dec 29 20:43:04 2008 +0100
10.3 @@ -10,15 +10,12 @@
10.4
10.5
10.6 import java.util.Properties
10.7 -import javax.swing.SwingUtilities
10.8
10.9 import scala.collection.mutable.{HashMap, HashSet}
10.10
10.11 +import org.gjt.sp.util.Log
10.12 +
10.13 import isabelle.proofdocument.{ProofDocument, Text, Token}
10.14 -import isabelle.{Symbol, IsabelleSyntax}
10.15 -import isabelle.utils.EventSource
10.16 -
10.17 -import Command.Phase
10.18
10.19
10.20 class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation)
10.21 @@ -31,39 +28,32 @@
10.22 val keyword_decls = new HashSet[String]
10.23 private var initialized = false
10.24
10.25 - val activated = new EventSource[Unit]
10.26 - val commandInfo = new EventSource[Command]
10.27 - val outputInfo = new EventSource[String]
10.28 + val activated = new EventBus[Unit]
10.29 + val command_info = new EventBus[Command]
10.30 + val output_info = new EventBus[String]
10.31 var document: Document = null
10.32
10.33
10.34 - def swing(body: => Unit) =
10.35 - SwingUtilities.invokeAndWait(new Runnable { def run = body })
10.36 -
10.37 - def swing_async(body: => Unit) =
10.38 - SwingUtilities.invokeLater(new Runnable { def run = body })
10.39 -
10.40 -
10.41 - def fireChange(c: Command) = swing { commandInfo.fire(c) }
10.42 + def command_change(c: Command) = Swing.now { command_info.event(c) }
10.43
10.44 private def handle_result(r: IsabelleProcess.Result) = {
10.45 val id = if (r.props != null) r.props.getProperty(Markup.ID) else null
10.46 val st = if (id != null) commands.getOrElse(id, null) else null
10.47
10.48 if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
10.49 - swing { outputInfo.fire(r.result) }
10.50 + Swing.now { output_info.event(r.result) }
10.51 else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
10.52 initialized = true
10.53 - swing {
10.54 + Swing.now {
10.55 if (document != null) {
10.56 document.activate()
10.57 - activated.fire(())
10.58 + activated.event(())
10.59 }
10.60 }
10.61 }
10.62 else {
10.63 val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
10.64 - if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)) {
10.65 + if (st == null || (st.phase != Command.Phase.REMOVED && st.phase != Command.Phase.REMOVE)) {
10.66 r.kind match {
10.67
10.68 case IsabelleProcess.Kind.STATUS =>
10.69 @@ -75,24 +65,24 @@
10.70 //{{{
10.71 // command status
10.72 case XML.Elem(Markup.FINISHED, _, _) =>
10.73 - st.phase = Phase.FINISHED
10.74 - fireChange(st)
10.75 + st.phase = Command.Phase.FINISHED
10.76 + command_change(st)
10.77 case XML.Elem(Markup.UNPROCESSED, _, _) =>
10.78 - st.phase = Phase.UNPROCESSED
10.79 - fireChange(st)
10.80 + st.phase = Command.Phase.UNPROCESSED
10.81 + command_change(st)
10.82 case XML.Elem(Markup.FAILED, _, _) =>
10.83 - st.phase = Phase.FAILED
10.84 - fireChange(st)
10.85 + st.phase = Command.Phase.FAILED
10.86 + command_change(st)
10.87 case XML.Elem(Markup.DISPOSED, _, _) =>
10.88 document.prover.commands.removeKey(st.id)
10.89 - st.phase = Phase.REMOVED
10.90 - fireChange(st)
10.91 + st.phase = Command.Phase.REMOVED
10.92 + command_change(st)
10.93
10.94 // command and keyword declarations
10.95 - case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, _)), _) =>
10.96 - command_decls.addEntry(name)
10.97 - case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) =>
10.98 - keyword_decls.addEntry(name)
10.99 + case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) =>
10.100 + command_decls += name
10.101 + case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
10.102 + keyword_decls += name
10.103
10.104 // other markup
10.105 case XML.Elem(kind,
10.106 @@ -117,15 +107,15 @@
10.107 //}}}
10.108
10.109 case IsabelleProcess.Kind.ERROR if st != null =>
10.110 - if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
10.111 - st.phase = Phase.FAILED
10.112 + if (st.phase != Command.Phase.REMOVED && st.phase != Command.Phase.REMOVE)
10.113 + st.phase = Command.Phase.FAILED
10.114 st.add_result(tree)
10.115 - fireChange(st)
10.116 + command_change(st)
10.117
10.118 case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
10.119 | IsabelleProcess.Kind.WARNING if st != null =>
10.120 st.add_result(tree)
10.121 - fireChange(st)
10.122 + command_change(st)
10.123
10.124 case _ =>
10.125 }
10.126 @@ -135,8 +125,12 @@
10.127
10.128
10.129 def start(logic: String) {
10.130 - val results = new EventBus[IsabelleProcess.Result] + handle_result
10.131 if (logic != null) _logic = logic
10.132 +
10.133 + val results = new EventBus[IsabelleProcess.Result]
10.134 + results += handle_result
10.135 + results.logger = Log.log(Log.ERROR, null, _)
10.136 +
10.137 process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
10.138 }
10.139
10.140 @@ -144,22 +138,22 @@
10.141 process.kill
10.142 }
10.143
10.144 - def setDocument(text: Text, path: String) {
10.145 + def set_document(text: Text, path: String) {
10.146 this.document = new Document(text, this)
10.147 process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
10.148
10.149 - document.structuralChanges.add(changes => {
10.150 + document.structural_changes += (changes => {
10.151 for (cmd <- changes.removedCommands) remove(cmd)
10.152 for (cmd <- changes.addedCommands) send(cmd)
10.153 })
10.154 if (initialized) {
10.155 document.activate()
10.156 - activated.fire(())
10.157 + activated.event(())
10.158 }
10.159 }
10.160
10.161 private def send(cmd: Command) {
10.162 - cmd.phase = Phase.UNPROCESSED
10.163 + cmd.phase = Command.Phase.UNPROCESSED
10.164 commands.put(cmd.id, cmd)
10.165
10.166 val props = new Properties
10.167 @@ -172,7 +166,7 @@
10.168 }
10.169
10.170 def remove(cmd: Command) {
10.171 - cmd.phase = Phase.REMOVE
10.172 + cmd.phase = Command.Phase.REMOVE
10.173 process.remove_command(cmd.id)
10.174 }
10.175 }