--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Sun Feb 01 12:21:07 2009 +0100
@@ -22,7 +22,7 @@
/* parsing */
private var stopped = false
- override def stop () = { stopped = true }
+ override def stop() = { stopped = true }
def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = {
stopped = false
@@ -30,7 +30,7 @@
val data = new SideKickParsedData(buffer.getName)
val prover_setup = Isabelle.plugin.prover_setup(buffer)
- if(prover_setup.isDefined){
+ if (prover_setup.isDefined) {
val document = prover_setup.get.prover.document
val commands = document.commands
while (!stopped && commands.hasNext) {
@@ -54,7 +54,7 @@
override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
val buffer = pane.getBuffer
val ps = Isabelle.prover_setup(buffer)
- if(ps.isDefined) {
+ if (ps.isDefined) {
val completions = ps.get.prover.completions
def before_caret(i : Int) = buffer.getText(0 max caret - i, i)
def next_nonfitting(s : String) : String = {
@@ -64,9 +64,9 @@
}
def suggestions(i : Int) : (Set[String], String)= {
val text = before_caret(i)
- if(!text.matches("\\s") && i < 30){
+ if (!text.matches("\\s") && i < 30) {
val larger_results = suggestions(i + 1)
- if(larger_results._1.size > 0) larger_results
+ if (larger_results._1.size > 0) larger_results
else (completions.range(text, next_nonfitting(text)), text)
} else (Set[String](), text)
@@ -76,10 +76,10 @@
val descriptions = new java.util.LinkedList[String]
// compute suggestions
val (suggs, text) = suggestions(1)
- for(s <- suggs) {
+ for (s <- suggs) {
val decoded = Isabelle.symbols.decode(s)
list.add(decoded)
- if(decoded != s) descriptions.add(s) else descriptions.add(null)
+ if (decoded != s) descriptions.add(s) else descriptions.add(null)
}
return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
} else return null
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala Sun Feb 01 12:21:07 2009 +0100
@@ -44,7 +44,7 @@
addComponent(Isabelle.Property("font-size.title"), {
try {
if (Isabelle.Property("font-size") != null)
- fontSize.setValue(Integer.valueOf(Isabelle.Property("font-size")))
+ fontSize.setValue(Isabelle.Property("font-size").toInt)
}
catch {
case e : NumberFormatException =>
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sun Feb 01 12:21:07 2009 +0100
@@ -31,7 +31,7 @@
addMouseListener(new MouseAdapter {
override def mousePressed(evt : MouseEvent) {
val line = yToLine(evt.getY)
- if(line >= 0 && line < textarea.getLineCount())
+ if (line >= 0 && line < textarea.getLineCount())
textarea.setCaretPosition(textarea.getLineStartOffset(line))
}
})
@@ -52,7 +52,7 @@
val buffer = textarea.getBuffer
val lineCount = buffer.getLineCount
val line = yToLine(evt.getY())
- if(line >= 0 && line < textarea.getLineCount)
+ if (line >= 0 && line < textarea.getLineCount)
{
"TODO: Tooltip"
} else ""
@@ -71,7 +71,7 @@
gfx.setColor(light)
gfx.fillRect(0, y, getWidth - 1, 1 max height)
- if(height > 2){
+ if (height > 2) {
gfx.setColor(dark)
gfx.drawRect(0, y, getWidth - 1, height)
}
@@ -82,7 +82,7 @@
super.paintComponent(gfx)
val buffer = textarea.getBuffer
- for(c <- prover.document.commands)
+ for (c <- prover.document.commands)
paintCommand(c, buffer, gfx)
}
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Sun Feb 01 12:21:07 2009 +0100
@@ -12,7 +12,7 @@
import java.awt.Font
import javax.swing.JScrollPane
-import scala.collection.mutable.HashMap
+import scala.collection.mutable
import isabelle.prover.{Prover, Command}
import isabelle.IsabelleSystem
@@ -39,6 +39,12 @@
var system: IsabelleSystem = null
def symbols = system.symbols
+ // settings
+ def default_logic = {
+ val logic = Isabelle.Property("logic")
+ if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
+ }
+
// plugin instance
var plugin: Plugin = null
@@ -69,7 +75,7 @@
// mapping buffer <-> prover
- private val mapping = new HashMap[JEditBuffer, ProverSetup]
+ private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
private def install(view: View) {
val buffer = view.getBuffer
@@ -100,9 +106,9 @@
case Some(prover_setup) =>
prover_setup.theory_view.activate
val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
- if(dockable != null) {
+ if (dockable != null) {
val output_dockable = dockable.asInstanceOf[OutputDockable]
- if(output_dockable.getComponent(0) != prover_setup.output_text_view ) {
+ if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
output_dockable.asInstanceOf[OutputDockable].removeAll
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
output_dockable.revalidate
@@ -111,7 +117,7 @@
}
case EditPaneUpdate.BUFFER_CHANGING =>
val buffer = epu.getEditPane.getBuffer
- if(buffer != null) mapping get buffer match {
+ if (buffer != null) mapping get buffer match {
//only deactivate 'isabelle'-buffers!
case None =>
case Some(prover_setup) => prover_setup.theory_view.deactivate
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Sun Feb 01 12:21:07 2009 +0100
@@ -22,7 +22,7 @@
class ProverSetup(buffer: JEditBuffer)
{
- val prover = new Prover(Isabelle.system)
+ var prover: Prover = null
var theory_view: TheoryView = null
val state_update = new EventBus[Command]
@@ -34,7 +34,8 @@
val output_text_view = new JTextArea
def activate(view: View) {
- prover.start(Isabelle.Property("logic"))
+ prover = new Prover(Isabelle.system, Isabelle.default_logic)
+
val buffer = view.getBuffer
val dir = buffer.getDirectory
@@ -49,9 +50,9 @@
output_text_view.append(text)
val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
//link process output if dockable is active
- if(dockable != null) {
+ if (dockable != null) {
val output_dockable = dockable.asInstanceOf[OutputDockable]
- if(output_dockable.getComponent(0) != output_text_view ) {
+ if (output_dockable.getComponent(0) != output_text_view ) {
output_dockable.asInstanceOf[OutputDockable].removeAll
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
output_dockable.revalidate
@@ -65,7 +66,7 @@
val state_panel =
if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
else null
- if (state_panel != null){
+ if (state_panel != null) {
if (state == null)
state_panel.setDocument(null: Document)
else
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Sun Feb 01 12:21:07 2009 +0100
@@ -11,7 +11,7 @@
import isabelle.renderer.UserAgent
-import scala.collection.mutable.{ArrayBuffer, HashMap}
+import scala.collection.mutable
import java.awt.{BorderLayout, Adjustable, Dimension}
import java.awt.event.{ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent}
@@ -60,7 +60,7 @@
//panel has to be displayable before calculating preferred size!
add(panel)
// recalculate preferred size after resizing the message_view
- if(panel.getPreferredSize.getWidth.toInt != getWidth){
+ if (panel.getPreferredSize.getWidth.toInt != getWidth) {
cache.renderer.relayout (panel, getWidth)
}
val width = panel.getPreferredSize.getWidth.toInt
@@ -76,12 +76,12 @@
removeAll()
//calculate offset in pixel
val panel = place_message(no, 0)
- val pixeloffset = if(panel != null) panel.getHeight*offset/100 else 0
+ val pixeloffset = if (panel != null) panel.getHeight*offset/100 else 0
var n = no
var y:Int = getHeight + pixeloffset
- while (y >= 0 && n >= 0){
+ while (y >= 0 && n >= 0) {
val panel = place_message (n, y)
- if(panel != null) {
+ if (panel != null) {
panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder)
y = y - panel.getHeight
}
@@ -132,9 +132,9 @@
// do not show every new message, wait a certain amount of time
val message_ind_timer : Timer = new Timer(250, new ActionListener {
// this method is called to indicate a new message
- override def actionPerformed(e:ActionEvent){
+ override def actionPerformed(e:ActionEvent) {
//fire scroll-event if necessary and wanted
- if(message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
+ if (message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
vscroll.setValue(buffer.size*subunits - 1)
}
infopanel.setIndicator(false)
@@ -147,15 +147,15 @@
infopanel.setIndicator(true)
infopanel.setText(buffer.size.toString)
- if (! message_ind_timer.isRunning()){
- if(infopanel.isAutoScroll){
+ if (!message_ind_timer.isRunning()) {
+ if (infopanel.isAutoScroll) {
vscroll.setValue(buffer.size*subunits - 1)
}
message_ind_timer.setRepeats(false)
message_ind_timer.start()
}
- if(message_panel.no == -1) {
+ if (message_panel.no == -1) {
message_panel.no = 0
message_panel.revalidate
}
@@ -164,7 +164,7 @@
override def adjustmentValueChanged (e : AdjustmentEvent) = {
//event-handling has to be so general (without UNIT_INCR,...)
// because all events could be sent as TRACK e.g. on my mac
- if (e.getSource == vscroll){
+ if (e.getSource == vscroll) {
message_panel.no = e.getValue / subunits
message_panel.offset = 100 - 100 * (e.getValue % subunits) / subunits
message_panel.revalidate
@@ -179,12 +179,12 @@
//Concrete Implementations
//containing the unrendered messages
-class MessageBuffer extends HashMap[Int,Result] with Unrendered[Result]{
+class MessageBuffer extends mutable.HashMap[Int,Result] with Unrendered[Result]{
override def addUnrendered (id: Int, m: Result) {
update(id, m)
}
- override def getUnrendered (id: Int): Option[Result] = {
- if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
+ override def getUnrendered(id: Int): Option[Result] = {
+ if (id < size && id >= 0 && apply(id) != null) Some (apply(id))
else None
}
override def size = super.size
@@ -192,11 +192,11 @@
//containing the rendered messages
class PanelCache (buffer: Unrendered[Result], val renderer: Renderer[Result, XHTMLPanel])
- extends HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
+ extends mutable.HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
override def getRendered (id: Int): Option[XHTMLPanel] = {
//get message from buffer and render it if necessary
- if(!isDefinedAt(id)){
+ if (!isDefinedAt(id)) {
buffer.getUnrendered(id) match {
case Some (message) =>
update (id, renderer.render (message))
@@ -204,7 +204,7 @@
}
}
val result = try {
- Some (apply(id))
+ Some(apply(id))
} catch {
case _ => {
None
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala Sun Feb 01 12:21:07 2009 +0100
@@ -32,7 +32,7 @@
}
override def keyPressed(e: KeyEvent) {
- if(e.getKeyCode == KeyEvent.VK_ENTER) {
+ if (e.getKeyCode == KeyEvent.VK_ENTER) {
copyaction
e.consume
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Feb 01 12:21:07 2009 +0100
@@ -148,8 +148,7 @@
def repaint(cmd: Command) =
{
- val status = cmd.status
- if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) {
+ if (text_area != null) {
val start = text_area.getLineOfOffset(to_current(cmd.start))
val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
text_area.invalidateLineRange(start, stop)
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Feb 01 12:21:07 2009 +0100
@@ -37,7 +37,7 @@
}
-class ProofDocument(text: Text, prover: Prover)
+class ProofDocument(text: Text, is_command_keyword: String => Boolean)
{
private var active = false
def activate() {
@@ -103,7 +103,7 @@
while (matcher.find(position) && !finished) {
position = matcher.end
val kind =
- if (prover.is_command_keyword(matcher.group))
+ if (is_command_keyword(matcher.group))
Token.Kind.COMMAND_START
else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
Token.Kind.COMMENT
--- a/src/Tools/jEdit/src/prover/Command.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Sun Feb 01 12:21:07 2009 +0100
@@ -11,7 +11,7 @@
import javax.swing.text.Position
import javax.swing.tree.DefaultMutableTreeNode
-import scala.collection.mutable.ListBuffer
+import scala.collection.mutable
import isabelle.proofdocument.{Text, Token, ProofDocument}
import isabelle.jedit.{Isabelle, Plugin}
@@ -24,8 +24,6 @@
object Status extends Enumeration {
val UNPROCESSED = Value("UNPROCESSED")
val FINISHED = Value("FINISHED")
- val REMOVE = Value("REMOVE")
- val REMOVED = Value("REMOVED")
val FAILED = Value("FAILED")
}
}
@@ -34,7 +32,10 @@
class Command(text: Text, val first: Token, val last: Token)
{
val id = Isabelle.plugin.id()
-
+
+
+ /* content */
+
{
var t = first
while (t != null) {
@@ -43,37 +44,6 @@
}
}
-
- /* command status */
-
- private var _status = Command.Status.UNPROCESSED
- def status = _status
- def status_=(st: Command.Status.Value) = {
- if (st == Command.Status.UNPROCESSED) {
- // delete markup
- for (child <- root_node.children) {
- child.children = Nil
- }
- }
- _status = st
- }
-
-
- /* accumulated results */
-
- private val results = new ListBuffer[XML.Tree]
- def add_result(tree: XML.Tree) { results += tree }
-
- def result_document = XML.document(
- results.toList match {
- case Nil => XML.Elem("message", Nil, Nil)
- case List(elem) => elem
- case elems => XML.Elem("messages", Nil, List(elems.first, elems.last)) // FIXME all elems!?
- }, "style")
-
-
- /* content */
-
override def toString = name
val name = text.content(first.start, first.stop)
@@ -94,7 +64,40 @@
}
- /* markup tree */
+ /* command status */
+
+ var state_id: IsarDocument.State_ID = null
+
+ private var _status = Command.Status.UNPROCESSED
+ def status = _status
+ def status_=(st: Command.Status.Value) {
+ if (st == Command.Status.UNPROCESSED) {
+ // delete markup
+ for (child <- root_node.children) {
+ child.children = Nil
+ }
+ }
+ _status = st
+ }
+
+
+ /* results */
+
+ private val results = new mutable.ListBuffer[XML.Tree]
+ private val state_results = new mutable.ListBuffer[XML.Tree]
+ def add_result(running: Boolean, tree: XML.Tree) {
+ (if (running) state_results else results) += tree
+ }
+
+ def result_document = XML.document(
+ results.toList ::: state_results.toList match {
+ case Nil => XML.Elem("message", Nil, Nil)
+ case List(elem) => elem
+ case elems => XML.Elem("messages", Nil, elems)
+ }, "style")
+
+
+ /* markup */
val root_node =
new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Feb 01 12:21:07 2009 +0100
@@ -23,7 +23,7 @@
override def getShortString : String = node.short
override def getLongString : String = node.long
override def getName : String = node.name
- override def setName (name : String) = ()
+ override def setName(name : String) = ()
override def setStart(start : Position) = ()
override def getStart : Position = node.base.start + node.start
override def setEnd(end : Position) = ()
@@ -48,7 +48,7 @@
def children = children_cell
def children_= (cs : List[MarkupNode]) = {
swing_node.removeAllChildren
- for(c <- cs) swing_node add c.swing_node
+ for (c <- cs) swing_node add c.swing_node
children_cell = cs
}
@@ -62,7 +62,7 @@
private def remove(nodes : List[MarkupNode]) {
children_cell = children diff nodes
- for(node <- nodes) try {
+ for (node <- nodes) try {
swing_node remove node.swing_node
} catch { case e : IllegalArgumentException =>
System.err.println(e.toString)
@@ -72,23 +72,23 @@
def dfs : List[MarkupNode] = {
var all = Nil : List[MarkupNode]
- for(child <- children)
+ for (child <- children)
all = child.dfs ::: all
all = this :: all
all
}
def insert(new_child : MarkupNode) : Unit = {
- if(new_child fitting_into this){
- for(child <- children){
- if(new_child fitting_into child)
+ if (new_child fitting_into this) {
+ for (child <- children) {
+ if (new_child fitting_into child)
child insert new_child
}
- if(new_child orphan){
+ if (new_child orphan) {
// new_child did not fit into children of this
// -> insert new_child between this and its children
- for(child <- children){
- if(child fitting_into new_child) {
+ for (child <- children) {
+ if (child fitting_into new_child) {
new_child add child
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Feb 01 12:21:07 2009 +0100
@@ -1,5 +1,5 @@
/*
- * Higher-level prover communication
+ * Higher-level prover communication: interactive document model
*
* @author Johannes Hölzl, TU Munich
* @author Fabian Immler, TU Munich
@@ -9,40 +9,57 @@
package isabelle.prover
-import scala.collection.mutable.{HashMap, HashSet}
+import scala.collection.mutable
import scala.collection.immutable.{TreeSet}
import org.gjt.sp.util.Log
+import isabelle.jedit.Isabelle
import isabelle.proofdocument.{ProofDocument, Text, Token}
import isabelle.IsarDocument
-class Prover(isabelle_system: IsabelleSystem)
+class Prover(isabelle_system: IsabelleSystem, logic: String)
{
- private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
+ /* prover process */
+
private var process: Isar = null
- private val commands = new HashMap[IsarDocument.Command_ID, Command]
+ {
+ val results = new EventBus[IsabelleProcess.Result] + handle_result
+ results.logger = Log.log(Log.ERROR, null, _)
+ process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
+ }
+
+ def stop() { process.kill }
+
+ /* document state information */
+ private val states = new mutable.HashMap[IsarDocument.State_ID, Command]
+ private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
+ private val document0 = Isabelle.plugin.id()
+ private val document_versions = new mutable.HashSet[IsarDocument.Document_ID] + document0
+
+ private var initialized = false
+
+
/* outer syntax keywords */
val decl_info = new EventBus[(String, String)]
- private val keyword_decls = new HashSet[String] {
+ private val keyword_decls = new mutable.HashSet[String] {
override def +=(name: String) = {
decl_info.event(name, OuterKeyword.MINOR)
super.+=(name)
}
}
- private val command_decls = new HashMap[String, String] {
+ private val command_decls = new mutable.HashMap[String, String] {
override def +=(entry: (String, String)) = {
decl_info.event(entry)
super.+=(entry)
}
}
- def is_command_keyword(s: String): Boolean = command_decls.contains(s)
/* completions */
@@ -51,9 +68,9 @@
def completions = _completions
/* // TODO: ask Makarius to make Interpretation.symbols public (here: read-only as 'symbol_map')
val map = isabelle.jedit.Isabelle.symbols.symbol_map
- for(xsymb <- map.keys) {
+ for (xsymb <- map.keys) {
_completions += xsymb
- if(map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
+ if (map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
}
*/
decl_info += (k_v => _completions += k_v._1)
@@ -61,8 +78,6 @@
/* event handling */
- private var initialized = false
-
val activated = new EventBus[Unit]
val command_info = new EventBus[Command]
val output_info = new EventBus[String]
@@ -71,15 +86,20 @@
def command_change(c: Command) = Swing.now { command_info.event(c) }
- private def handle_result(r: IsabelleProcess.Result)
+ private def handle_result(result: IsabelleProcess.Result)
{
- val (id, st) = r.props.find(p => p._1 == Markup.ID) match
- { case None => (null, null)
- case Some((_, i)) => (i, commands.getOrElse(i, null)) }
+ val (running, command) =
+ result.props.find(p => p._1 == Markup.ID) match {
+ case None => (false, null)
+ case Some((_, id)) =>
+ if (commands.contains(id)) (false, commands(id))
+ else if (states.contains(id)) (true, states(id))
+ else (false, null)
+ }
- if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
- Swing.now { output_info.event(r.result) }
- else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
+ if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN)
+ Swing.now { output_info.event(result.result) }
+ else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !?
initialized = true
Swing.now {
if (document != null) {
@@ -89,97 +109,90 @@
}
}
else {
- if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
- r.kind match {
+ result.kind match {
+
+ case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
+ | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR
+ if command != null =>
+ if (result.kind == IsabelleProcess.Kind.ERROR)
+ command.status = Command.Status.FAILED
+ command.add_result(running, process.parse_message(result))
+ command_change(command)
- case IsabelleProcess.Kind.STATUS =>
- //{{{ handle all kinds of status messages here
- val tree = process.parse_message(r)
- tree match {
- case XML.Elem(Markup.MESSAGE, _, elems) =>
- for (elem <- elems) {
- elem match {
- //{{{
- // command status
- case XML.Elem(Markup.FINISHED, _, _) =>
- st.status = Command.Status.FINISHED
- command_change(st)
- case XML.Elem(Markup.UNPROCESSED, _, _) =>
- st.status = Command.Status.UNPROCESSED
- command_change(st)
- case XML.Elem(Markup.FAILED, _, _) =>
- st.status = Command.Status.FAILED
- command_change(st)
- case XML.Elem(Markup.DISPOSED, _, _) =>
- commands.removeKey(st.id)
- st.status = Command.Status.REMOVED
- command_change(st)
-
- // command and keyword declarations
- case XML.Elem(Markup.COMMAND_DECL,
- (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
- command_decls += (name -> kind)
- case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
- keyword_decls += name
+ case IsabelleProcess.Kind.STATUS =>
+ //{{{ handle all kinds of status messages here
+ process.parse_message(result) match {
+ case XML.Elem(Markup.MESSAGE, _, elems) =>
+ for (elem <- elems) {
+ elem match {
+ //{{{
+ // command and keyword declarations
+ case XML.Elem(Markup.COMMAND_DECL,
+ (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+ command_decls += (name -> kind)
+ case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+ keyword_decls += name
- // other markup
- case XML.Elem(kind,
- (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
- (Markup.ID, markup_id) :: _, _) =>
- val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
- val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
+ // document edits
+ case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
+ if document_versions.contains(doc_id) =>
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+ <- edits
+ if (commands.contains(cmd_id))
+ } {
+ val cmd = commands(cmd_id)
+ if (cmd.state_id != null) states -= cmd.state_id
+ states(cmd_id) = cmd
+ cmd.state_id = state_id
+ cmd.status = Command.Status.UNPROCESSED
+ command_change(cmd)
+ }
- val command =
- // outer syntax: no id in props
- if (st == null) commands.getOrElse(markup_id, null)
- // inner syntax: id from props
- else st
- command.root_node.insert(command.node_from(kind, begin, end))
+ // command status
+ case XML.Elem(Markup.UNPROCESSED, _, _)
+ if command != null =>
+ command.status = Command.Status.UNPROCESSED
+ command_change(command)
+ case XML.Elem(Markup.FINISHED, _, _)
+ if command != null =>
+ command.status = Command.Status.FINISHED
+ command_change(command)
+ case XML.Elem(Markup.FAILED, _, _)
+ if command != null =>
+ command.status = Command.Status.FAILED
+ command_change(command)
- case _ =>
- //}}}
- }
+ // other markup
+ case XML.Elem(kind,
+ (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
+ (Markup.ID, markup_id) :: _, _) =>
+ val begin = offset.toInt - 1
+ val end = end_offset.toInt - 1
+
+ val cmd = // FIXME proper command version!? running!?
+ // outer syntax: no id in props
+ if (command == null) commands.getOrElse(markup_id, null)
+ // inner syntax: id from props
+ else command
+ if (cmd != null)
+ cmd.root_node.insert(cmd.node_from(kind, begin, end))
+
+ case _ =>
+ //}}}
}
- case _ =>
- }
- //}}}
+ }
+ case _ =>
+ }
+ //}}}
- case IsabelleProcess.Kind.ERROR if st != null =>
- val tree = process.parse_message(r)
- if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)
- st.status = Command.Status.FAILED
- st.add_result(tree)
- command_change(st)
-
- case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
- | IsabelleProcess.Kind.WARNING if st != null =>
- val tree = process.parse_message(r)
- st.add_result(tree)
- command_change(st)
-
- case _ =>
- }
+ case _ =>
}
}
}
-
- def start(logic: String) {
- 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)
- }
-
- def stop() {
- process.kill
- }
-
def set_document(text: Text, path: String) {
- this.document = new ProofDocument(text, this)
+ this.document = new ProofDocument(text, command_decls.contains(_))
process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
document.structural_changes += (changes => {
@@ -202,7 +215,8 @@
}
def remove(cmd: Command) {
- cmd.status = Command.Status.REMOVE
+ commands -= cmd.id
+ if (cmd.state_id != null) states -= cmd.state_id
process.remove_command(cmd.id)
}
}
--- a/src/Tools/jEdit/src/utils/Delay.scala Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/utils/Delay.scala Sun Feb 01 12:21:07 2009 +0100
@@ -12,14 +12,14 @@
class Delay(amount : Int, action : () => Unit) {
val timer : Timer = new Timer(amount, new ActionListener {
- override def actionPerformed(e:ActionEvent){
- action ()
+ override def actionPerformed(e:ActionEvent) {
+ action()
}
})
// if called very often, action is executed at most once
// in amount milliseconds
- def delay_or_ignore () = {
- if (! timer.isRunning()){
+ def delay_or_ignore() = {
+ if (!timer.isRunning()) {
timer.setRepeats(false)
timer.start()
}