original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
authorwenzelm
Sun Oct 19 16:51:55 2008 +0200 (2008-10-19 ago)
changeset 34318c13e168a8ae6
child 34319 eaac45c45348
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
src/Tools/jEdit/plugin/IsabellePlugin.ant
src/Tools/jEdit/plugin/IsabellePlugin.props
src/Tools/jEdit/plugin/actions.xml
src/Tools/jEdit/plugin/dockables.xml
src/Tools/jEdit/plugin/services.xml
src/Tools/jEdit/src/jedit/OptionPane.scala
src/Tools/jEdit/src/jedit/OutputDockable.scala
src/Tools/jEdit/src/jedit/Plugin.scala
src/Tools/jEdit/src/jedit/StateViewDockable.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/jedit/VFS.scala
src/Tools/jEdit/src/proofdocument/ProofDocument.scala
src/Tools/jEdit/src/proofdocument/Text.scala
src/Tools/jEdit/src/proofdocument/Token.scala
src/Tools/jEdit/src/proofdocument/tests/TestProofDocument.scala
src/Tools/jEdit/src/prover/Command.scala
src/Tools/jEdit/src/prover/CommandChangeInfo.scala
src/Tools/jEdit/src/prover/Document.scala
src/Tools/jEdit/src/prover/Prover.scala
src/Tools/jEdit/src/utils/EventSource.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/plugin/IsabellePlugin.ant	Sun Oct 19 16:51:55 2008 +0200
     1.3 @@ -0,0 +1,10 @@
     1.4 +<?xml version="1.0"?>
     1.5 +<project name="IsabellePlugin installer" default="install" basedir=".">
     1.6 +  <target name="install">
     1.7 +  	<copy file="services.xml" todir="bin" />
     1.8 +  	<copy file="dockables.xml" todir="bin" />
     1.9 +  	<copy file="actions.xml" todir="bin" />
    1.10 +  	<copy file="IsabellePlugin.props" todir="bin" />
    1.11 +    <jar destfile="IsabellePlugin.jar" basedir="bin" /> 
    1.12 +  </target>
    1.13 +</project>
    1.14 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/jEdit/plugin/IsabellePlugin.props	Sun Oct 19 16:51:55 2008 +0200
     2.3 @@ -0,0 +1,24 @@
     2.4 +# jEdit Properties
     2.5 +
     2.6 +plugin.isabelle.jedit.Plugin.activate=startup
     2.7 +plugin.isabelle.jedit.Plugin.name=IsabellePlugin
     2.8 +plugin.isabelle.jedit.Plugin.version=0.1
     2.9 +plugin.isabelle.jedit.Plugin.description=Isabelle/Isar integration into jEdit
    2.10 +plugin.isabelle.jedit.Plugin.option-pane=isabelle
    2.11 +
    2.12 +plugin.isabelle.jedit.Plugin.menu.label=Isabelle
    2.13 +plugin.isabelle.jedit.Plugin.menu=Isabelle.show-output Isabelle.show-state Isabelle.activate
    2.14 +
    2.15 +Isabelle.show-output.label=Show Output
    2.16 +Isabelle.show-state.label=Show State
    2.17 +Isabelle.activate.label=Activate current buffer
    2.18 +
    2.19 +Isabelle_output.title=Isabelle Output
    2.20 +Isabelle_state.title=Isabelle State
    2.21 +
    2.22 +options.isabelle.label=Isabelle
    2.23 +options.isabelle.code=new isabelle.jedit.OptionPane();
    2.24 +options.isabelle.font-path.title=Font Path
    2.25 +options.isabelle.font-size.title=Font Size
    2.26 +options.isabelle.font-size=14
    2.27 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/plugin/actions.xml	Sun Oct 19 16:51:55 2008 +0200
     3.3 @@ -0,0 +1,20 @@
     3.4 +<ACTIONS>
     3.5 +	<ACTION NAME="Isabelle.show-output">
     3.6 +		<CODE>
     3.7 +			wm.addDockableWindow("Isabelle_output");
     3.8 +		</CODE>
     3.9 +	</ACTION>
    3.10 +	<ACTION NAME="Isabelle.show-state">
    3.11 +		<CODE>
    3.12 +			wm.addDockableWindow("Isabelle_state");
    3.13 +		</CODE>
    3.14 +	</ACTION>
    3.15 +	<ACTION NAME="Isabelle.activate">
    3.16 +		<CODE>
    3.17 +			isabelle.jedit.Plugin$.MODULE$.plugin().activate(view);
    3.18 +		</CODE>
    3.19 +		<IS_SELECTED>
    3.20 +			return view.getBuffer().getMode().getName() == "isabelle";
    3.21 +		</IS_SELECTED>
    3.22 +	</ACTION>
    3.23 +</ACTIONS>
    3.24 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/plugin/dockables.xml	Sun Oct 19 16:51:55 2008 +0200
     4.3 @@ -0,0 +1,12 @@
     4.4 +<?xml version="1.0"?>
     4.5 +
     4.6 +<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
     4.7 +
     4.8 +<DOCKABLES>
     4.9 +	<DOCKABLE NAME="Isabelle_output">
    4.10 +		new isabelle.jedit.OutputDockable(view, position);
    4.11 +	</DOCKABLE>
    4.12 +	<DOCKABLE NAME="Isabelle_state">
    4.13 +		new isabelle.jedit.StateViewDockable(view, position);
    4.14 +	</DOCKABLE>
    4.15 +</DOCKABLES>
    4.16 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/jEdit/plugin/services.xml	Sun Oct 19 16:51:55 2008 +0200
     5.3 @@ -0,0 +1,7 @@
     5.4 +<?xml version="1.0"?>
     5.5 +<!DOCTYPE SERVICES SYSTEM "services.dtd">
     5.6 +<SERVICES>
     5.7 +	<SERVICE NAME="isa" CLASS="org.gjt.sp.jedit.io.VFS">
     5.8 +		new isabelle.jedit.VFS();
     5.9 +	</SERVICE>
    5.10 +</SERVICES>
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Sun Oct 19 16:51:55 2008 +0200
     6.3 @@ -0,0 +1,83 @@
     6.4 +package isabelle.jedit
     6.5 +
     6.6 +import java.lang.Integer
     6.7 +
     6.8 +import java.awt.BorderLayout
     6.9 +import java.awt.GridBagConstraints.HORIZONTAL
    6.10 +import java.awt.BorderLayout.{ WEST, CENTER, EAST }
    6.11 +import java.awt.event.{ ActionListener, ActionEvent }
    6.12 +import javax.swing.{ JTextField, JButton, JPanel, JLabel, JFileChooser, 
    6.13 +                     JSpinner, SwingUtilities, JComboBox }
    6.14 +
    6.15 +import isabelle.IsabelleSystem
    6.16 +
    6.17 +import org.gjt.sp.jedit.AbstractOptionPane
    6.18 +
    6.19 +class OptionPane extends AbstractOptionPane("isabelle") {
    6.20 +  import Plugin.property
    6.21 +  
    6.22 +  var pathName = new JTextField()
    6.23 +  var fontSize = new JSpinner()
    6.24 +  var logicName = new JComboBox()
    6.25 +    
    6.26 +  override def _init() {
    6.27 +    addComponent(property("font-path.title"), {
    6.28 +      val pickPath = new JButton("...")
    6.29 +      pickPath.addActionListener(new ActionListener() {
    6.30 +        override def actionPerformed(e : ActionEvent) {
    6.31 +          val chooser = new JFileChooser(pathName.getText())
    6.32 +          if (chooser.showOpenDialog(OptionPane.this) == JFileChooser.APPROVE_OPTION)
    6.33 +            pathName.setText(chooser.getSelectedFile().getAbsolutePath())
    6.34 +        } 
    6.35 +      })
    6.36 +
    6.37 +      pathName.setText(property("font-path"))
    6.38 +      
    6.39 +      val pathPanel = new JPanel(new BorderLayout())
    6.40 +      pathPanel.add(pathName, CENTER)
    6.41 +      pathPanel.add(pickPath, EAST)
    6.42 +      pathPanel
    6.43 +    }, HORIZONTAL)
    6.44 +
    6.45 +    addComponent(property("font-size.title"), {
    6.46 +      try {
    6.47 +        if (property("font-size") != null)
    6.48 +          fontSize.setValue(Integer.valueOf(property("font-size")))
    6.49 +      }
    6.50 +      catch {
    6.51 +        case e : NumberFormatException => 
    6.52 +          fontSize.setValue(14)
    6.53 +      }
    6.54 +      
    6.55 +      fontSize
    6.56 +    })
    6.57 +
    6.58 +    addComponent(property("logic.title"), {
    6.59 +      val logics : Array[Object] = 
    6.60 +        (IsabelleSystem.isabelle_tool("findlogics") _1).split("\\s").asInstanceOf[Array[Object]]
    6.61 +      for (name <- logics) {
    6.62 +        logicName.addItem(name)
    6.63 +        if (name == property("logic"))
    6.64 +          logicName.setSelectedItem(name)
    6.65 +      }
    6.66 +      
    6.67 +      logicName
    6.68 +    })
    6.69 +  }
    6.70 +    
    6.71 +  override def _save() {
    6.72 +    val size = fontSize.getValue()
    6.73 +    val name = pathName.getText()
    6.74 +    if (property("font-path") != name || property("font-size") != size.toString) {
    6.75 +      property("font-path", name)
    6.76 +      property("font-size", size.toString)
    6.77 +      SwingUtilities invokeLater new Runnable() {
    6.78 +        override def run() = 
    6.79 +          Plugin.plugin.setFont(name, size.asInstanceOf[Integer].intValue)
    6.80 +      }
    6.81 +    }
    6.82 +    
    6.83 +    val logic = logicName.getSelectedItem.asInstanceOf[String]
    6.84 +    property("logic", logic) 
    6.85 +  }
    6.86 +}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/jEdit/src/jedit/OutputDockable.scala	Sun Oct 19 16:51:55 2008 +0200
     7.3 @@ -0,0 +1,20 @@
     7.4 +package isabelle.jedit
     7.5 +
     7.6 +import java.awt.GridLayout
     7.7 +
     7.8 +import javax.swing.{ JPanel, JTextArea, JScrollPane }
     7.9 +
    7.10 +import org.gjt.sp.jedit.View
    7.11 +
    7.12 +class OutputDockable(view : View, position : String) extends JPanel {
    7.13 +  {
    7.14 +    val textView = new JTextArea()
    7.15 +    
    7.16 +    setLayout(new GridLayout(1, 1))
    7.17 +    add(new JScrollPane(textView))
    7.18 +    
    7.19 +    textView.append("== Isabelle output ==\n")
    7.20 +    
    7.21 +    Plugin.plugin.prover.outputInfo.add( text => textView.append(text) )
    7.22 +  }
    7.23 +}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Oct 19 16:51:55 2008 +0200
     8.3 @@ -0,0 +1,98 @@
     8.4 +package isabelle.jedit
     8.5 +
     8.6 +import java.awt.Font
     8.7 +import java.io.{ FileInputStream, IOException }
     8.8 +
     8.9 +
    8.10 +import isabelle.utils.EventSource
    8.11 +
    8.12 +import isabelle.prover.{ Prover, Command }
    8.13 +
    8.14 +import isabelle.IsabelleSystem
    8.15 +
    8.16 +import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
    8.17 +import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
    8.18 +
    8.19 +object Plugin {
    8.20 +  val NAME = "Isabelle"
    8.21 +  val OPTION_PREFIX = "options.isabelle."
    8.22 +  
    8.23 +  def property(name : String) = jEdit.getProperty(OPTION_PREFIX + name)
    8.24 +  def property(name : String, value : String) = 
    8.25 +    jEdit.setProperty(OPTION_PREFIX + name, value)
    8.26 +  
    8.27 +  var plugin : Plugin = null
    8.28 +}
    8.29 +
    8.30 +class Plugin extends EBPlugin {
    8.31 +  import Plugin._
    8.32 +  
    8.33 +  val prover = new Prover()
    8.34 +  var theoryView : TheoryView = null
    8.35 +  
    8.36 +  var viewFont : Font = null 
    8.37 +  val viewFontChanged = new EventSource[Font]
    8.38 +  
    8.39 +  private var _selectedState : Command = null
    8.40 +  
    8.41 +  val stateUpdate = new EventSource[Command]
    8.42 +  
    8.43 +  def selectedState = _selectedState
    8.44 +  def selectedState_=(newState : Command) {
    8.45 +    _selectedState = newState
    8.46 +    stateUpdate fire newState
    8.47 +  }
    8.48 +  
    8.49 +  def activate(view : View) {
    8.50 +    val logic = property("logic")
    8.51 +    theoryView = new TheoryView(prover, view.getBuffer())
    8.52 +    prover.start(if (logic == null) logic else "HOL")
    8.53 +    val dir = view.getBuffer().getDirectory()
    8.54 +    prover.setDocument(theoryView, 
    8.55 +                       if (dir.startsWith("isa:")) dir.substring(4) else dir)
    8.56 +    TheoryView.activateTextArea(view.getTextArea())
    8.57 +  }
    8.58 +  
    8.59 +  override def handleMessage(msg : EBMessage) = msg match {
    8.60 +    case epu : EditPaneUpdate => epu.getWhat() match {
    8.61 +      case EditPaneUpdate.BUFFER_CHANGED =>
    8.62 +        TheoryView.activateTextArea(epu.getEditPane().getTextArea())
    8.63 +
    8.64 +      case EditPaneUpdate.BUFFER_CHANGING =>
    8.65 +        TheoryView.deactivateTextArea(epu.getEditPane().getTextArea())
    8.66 +
    8.67 +      case _ =>
    8.68 +    }
    8.69 +      
    8.70 +    case _ =>
    8.71 +  }
    8.72 +
    8.73 +  def setFont(path : String, size : Float) {
    8.74 +    try {
    8.75 +      val fontStream = new FileInputStream(path)
    8.76 +      val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
    8.77 +      viewFont = font.deriveFont(Font.PLAIN, size)
    8.78 +      
    8.79 +      viewFontChanged.fire(viewFont)
    8.80 +    }
    8.81 +    catch {
    8.82 +      case e : IOException =>
    8.83 +    }
    8.84 +  }
    8.85 +  
    8.86 +  override def start() {
    8.87 +    plugin = this
    8.88 +
    8.89 +    if (property("font-path") != null && property("font-size") != null)
    8.90 +      try {
    8.91 +        setFont(property("font-path"), property("font-size").toFloat)
    8.92 +      }
    8.93 +      catch {
    8.94 +        case e : NumberFormatException =>
    8.95 +      }
    8.96 +  }
    8.97 +  
    8.98 +  override def stop() {
    8.99 +    // TODO: implement cleanup
   8.100 +  }
   8.101 +}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Sun Oct 19 16:51:55 2008 +0200
     9.3 @@ -0,0 +1,80 @@
     9.4 +package isabelle.jedit
     9.5 +
     9.6 +import java.io.{ ByteArrayInputStream, FileInputStream, InputStream }
     9.7 +
     9.8 +import java.awt.GridLayout
     9.9 +import javax.swing.{ JPanel, JTextArea, JScrollPane }
    9.10 +
    9.11 +import isabelle.IsabelleSystem.getenv
    9.12 +
    9.13 +import org.xml.sax.InputSource;
    9.14 +
    9.15 +import org.w3c.dom.Document
    9.16 +
    9.17 +import org.xhtmlrenderer.simple.XHTMLPanel
    9.18 +import org.xhtmlrenderer.context.AWTFontResolver
    9.19 +import org.xhtmlrenderer.swing.NaiveUserAgent
    9.20 +import org.xhtmlrenderer.resource.CSSResource
    9.21 +
    9.22 +import org.gjt.sp.jedit.View
    9.23 +
    9.24 +object StateViewDockable {
    9.25 +  val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
    9.26 +  val userStylesheet = 
    9.27 +    "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css";
    9.28 +  val stylesheet = """
    9.29 +
    9.30 +@import "isabelle.css";
    9.31 +
    9.32 +@import '""" + userStylesheet + """';
    9.33 +
    9.34 +messages, message {
    9.35 +  display: block;
    9.36 +  white-space: pre-wrap;
    9.37 +  font-family: Isabelle;
    9.38 +}
    9.39 +"""
    9.40 +}
    9.41 +
    9.42 +class UserAgent extends NaiveUserAgent {
    9.43 +  override def getCSSResource(uri : String) : CSSResource = {
    9.44 +    if (uri == StateViewDockable.baseURL + "style")
    9.45 +      new CSSResource(
    9.46 +        new ByteArrayInputStream(StateViewDockable.stylesheet.getBytes()))
    9.47 +    else {
    9.48 +      val stream = resolveAndOpenStream(uri)
    9.49 +      val resource = new CSSResource(stream)
    9.50 +      if (stream == null)
    9.51 +        resource.getResourceInputSource().setByteStream(
    9.52 +          new ByteArrayInputStream(new Array[Byte](0)))
    9.53 +      resource
    9.54 +    }
    9.55 +  }
    9.56 +}
    9.57 +
    9.58 +class StateViewDockable(view : View, position : String) extends JPanel {
    9.59 +  {
    9.60 +    val panel = new XHTMLPanel(new UserAgent())
    9.61 +    setLayout(new GridLayout(1, 1))
    9.62 +    add(new JScrollPane(panel))
    9.63 +    
    9.64 +    val fontResolver =
    9.65 +      panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
    9.66 +    if (Plugin.plugin.viewFont != null)
    9.67 +      fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
    9.68 +
    9.69 +    Plugin.plugin.viewFontChanged.add(font => {
    9.70 +      if (Plugin.plugin.viewFont != null)
    9.71 +        fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
    9.72 +      
    9.73 +      panel.relayout()
    9.74 +    })
    9.75 +    
    9.76 +    Plugin.plugin.stateUpdate.add(state => {
    9.77 +      if (state == null)
    9.78 +        panel.setDocument(null : Document)
    9.79 +      else
    9.80 +        panel.setDocument(state.document, StateViewDockable.baseURL)
    9.81 +    })
    9.82 +  }
    9.83 +}
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Oct 19 16:51:55 2008 +0200
    10.3 @@ -0,0 +1,244 @@
    10.4 +package isabelle.jedit
    10.5 +
    10.6 +import isabelle.utils.EventSource
    10.7 +
    10.8 +import isabelle.proofdocument.Text
    10.9 +
   10.10 +import isabelle.prover.{ Prover, Command, CommandChangeInfo }
   10.11 +import isabelle.prover.Command.Phase
   10.12 +
   10.13 +import javax.swing.Timer
   10.14 +import javax.swing.event.{ CaretListener, CaretEvent }
   10.15 +import java.awt.Graphics2D
   10.16 +import java.awt.event.{ ActionEvent, ActionListener }
   10.17 +import java.awt.Color;
   10.18 +
   10.19 +import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
   10.20 +import org.gjt.sp.jedit.textarea.{ TextArea, TextAreaExtension, TextAreaPainter }
   10.21 +import org.gjt.sp.jedit.syntax.SyntaxStyle
   10.22 +
   10.23 +object TheoryView {
   10.24 +  val ISABELLE_THEORY_PROPERTY = "de.tum.in.isabelle.jedit.Theory";
   10.25 +
   10.26 +  def chooseColor(state : Command) : Color = {
   10.27 +    if (state == null)
   10.28 +      Color.red
   10.29 +    else
   10.30 +      state.phase match {
   10.31 +        case Phase.UNPROCESSED => new Color(255, 255, 192)
   10.32 +        case Phase.FINISHED => new Color(192, 255, 192)
   10.33 +        case Phase.FAILED => new Color(255, 192, 192)
   10.34 +        case _ => Color.red
   10.35 +      }
   10.36 +  }
   10.37 +  
   10.38 +  def withView(view : TextArea, f : (TheoryView) => Unit) {
   10.39 +    if (view != null && view.getBuffer() != null)
   10.40 +      view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match {
   10.41 +        case null => null
   10.42 +        case view: TheoryView => f(view)
   10.43 +        case _ => null
   10.44 +      }
   10.45 +  }
   10.46 +	
   10.47 +  def activateTextArea(textArea : TextArea) {
   10.48 +    withView(textArea, _.activate(textArea))
   10.49 +  }	
   10.50 +	
   10.51 +  def deactivateTextArea(textArea : TextArea) {
   10.52 +    withView(textArea, _.deactivate(textArea))
   10.53 +  }
   10.54 +}
   10.55 +
   10.56 +class TheoryView(prover : Prover, buffer : JEditBuffer) 
   10.57 +    extends TextAreaExtension with Text with BufferListener {
   10.58 +  import TheoryView._
   10.59 +  import Text.Changed
   10.60 +  
   10.61 +  var textArea : TextArea = null;
   10.62 +  var col : Changed = null;
   10.63 +  
   10.64 +  val colTimer = new Timer(300, new ActionListener() {
   10.65 +    override def actionPerformed(e : ActionEvent) { commit() }
   10.66 +  })
   10.67 +  
   10.68 +  val changesSource = new EventSource[Changed]
   10.69 +
   10.70 +  {
   10.71 +    buffer.addBufferListener(this)
   10.72 +    buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
   10.73 +    
   10.74 +    prover.commandInfo.add(e => repaint(e.command))
   10.75 +    prover.commandInfo.add(e => repaintAll())
   10.76 +	
   10.77 +    Plugin.plugin.viewFontChanged.add(font => updateFont())
   10.78 +    
   10.79 +    colTimer.stop
   10.80 +    colTimer.setRepeats(true)
   10.81 +  }
   10.82 +
   10.83 +  def activate(area : TextArea) {
   10.84 +    textArea = area
   10.85 +    textArea.addCaretListener(selectedStateController)
   10.86 +    
   10.87 +    val painter = textArea.getPainter()
   10.88 +    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
   10.89 +    updateFont()
   10.90 +  }
   10.91 +  
   10.92 +  private def updateFont() {
   10.93 +    if (textArea != null) {
   10.94 +      val painter = textArea.getPainter()
   10.95 +      if (Plugin.plugin.viewFont != null) {
   10.96 +        painter.setStyles(painter.getStyles().map(style =>
   10.97 +          new SyntaxStyle(style.getForegroundColor, 
   10.98 +                          style.getBackgroundColor, 
   10.99 +                          Plugin.plugin.viewFont)
  10.100 +        ))
  10.101 +        painter.setFont(Plugin.plugin.viewFont)
  10.102 +        repaintAll()
  10.103 +      }
  10.104 +    }
  10.105 +  }
  10.106 +  
  10.107 +  def deactivate(area : TextArea) {
  10.108 +    textArea.getPainter().removeExtension(this)
  10.109 +    textArea.removeCaretListener(selectedStateController)
  10.110 +    textArea = null
  10.111 +  }
  10.112 +  
  10.113 +  val selectedStateController = new CaretListener() {
  10.114 +    override def caretUpdate(e : CaretEvent) {
  10.115 +      val cmd = prover.document.getNextCommandContaining(e.getDot())
  10.116 +      if (cmd != null && cmd.start <= e.getDot() && 
  10.117 +            Plugin.plugin.selectedState != cmd)
  10.118 +        Plugin.plugin.selectedState = cmd
  10.119 +    }
  10.120 +  }
  10.121 +
  10.122 +  private def fromCurrent(pos : Int) =
  10.123 +    if (col != null && col.start <= pos)
  10.124 +      if (pos < col.start + col.added) col.start
  10.125 +      else pos - col.added + col.removed
  10.126 +    else pos
  10.127 +  
  10.128 +  private def toCurrent(pos : Int) = 
  10.129 +    if (col != null && col.start <= pos)
  10.130 +      if (pos < col.start + col.removed) col.start
  10.131 +      else pos + col.added - col.removed
  10.132 +    else pos
  10.133 +  
  10.134 +  def repaint(cmd : Command)
  10.135 +  {
  10.136 +    var ph = cmd.phase
  10.137 +    if (textArea != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
  10.138 +      var start = textArea.getLineOfOffset(toCurrent(cmd.start))
  10.139 +      var stop = textArea.getLineOfOffset(toCurrent(cmd.stop) - 1)
  10.140 +      textArea.invalidateLineRange(start, stop)
  10.141 +      
  10.142 +      if (Plugin.plugin.selectedState == cmd)
  10.143 +        Plugin.plugin.selectedState = cmd // update State view 
  10.144 +    }
  10.145 +  }
  10.146 +  
  10.147 +  def repaintAll()
  10.148 +  {
  10.149 +    if (textArea != null)
  10.150 +      textArea.invalidateLineRange(textArea.getFirstPhysicalLine, 
  10.151 +                                   textArea.getLastPhysicalLine)
  10.152 +  }
  10.153 +  
  10.154 +  override def paintValidLine(gfx : Graphics2D, screenLine : Int,
  10.155 +                              pl : Int, start : Int, end : Int, y : Int)
  10.156 +  {	
  10.157 +    var fm = textArea.getPainter().getFontMetrics()
  10.158 +    var savedColor = gfx.getColor()
  10.159 +    var e = prover.document.getNextCommandContaining(fromCurrent(start))
  10.160 +    
  10.161 +    while (e != null && toCurrent(e.start) < end) {
  10.162 +      val begin = Math.max(start, toCurrent(e.start))
  10.163 +      val startP = textArea.offsetToXY(begin)
  10.164 +
  10.165 +      val finish = Math.min(end - 1, toCurrent(e.stop))
  10.166 +      val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish) 
  10.167 +                  else { var p = textArea.offsetToXY(finish - 1) 
  10.168 +                         p.x = p.x + fm.charWidth(' ') 
  10.169 +                         p }
  10.170 +			
  10.171 +      if (startP != null && stopP != null) {
  10.172 +        gfx.setColor(chooseColor(e))
  10.173 +        gfx.fillRect(startP.x, y, stopP.x - startP.x, fm.getHeight())
  10.174 +      }
  10.175 +      
  10.176 +      e = e.next
  10.177 +    }
  10.178 +    
  10.179 +    gfx.setColor(savedColor)
  10.180 +  }
  10.181 +	
  10.182 +  def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
  10.183 +  def length = buffer.getLength()
  10.184 +
  10.185 +  def changes = changesSource
  10.186 +
  10.187 +  private def commit() {
  10.188 +    if (col != null)
  10.189 +      changes.fire(col)
  10.190 +    col = null
  10.191 +    if (colTimer.isRunning())
  10.192 +      colTimer.stop()
  10.193 +  }	
  10.194 +	
  10.195 +  private def delayCommit() {
  10.196 +    if (colTimer.isRunning())
  10.197 +      colTimer.restart()
  10.198 +    else
  10.199 +      colTimer.start()
  10.200 +  }
  10.201 +	
  10.202 +  override def contentInserted(buffer : JEditBuffer, startLine : Int, 
  10.203 +                               offset : Int, numLines : Int, length : Int) { }
  10.204 +  override def contentRemoved(buffer : JEditBuffer, startLine : Int, 
  10.205 +                              offset : Int, numLines : Int, length : Int) { }
  10.206 +
  10.207 +  override def preContentInserted(buffer : JEditBuffer, startLine : Int,
  10.208 +			offset : Int, numLines : Int, length : Int) {
  10.209 +    if (col == null) 
  10.210 +      col = new Changed(offset, length, 0)
  10.211 +    else if (col.start <= offset && offset <= col.start + col.added) 
  10.212 +      col = new Changed(col.start, col.added + length, col.removed)
  10.213 +    else { 
  10.214 +      commit()
  10.215 +      col = new Changed(offset, length, 0) 
  10.216 +    }
  10.217 +    delayCommit()
  10.218 +  }	
  10.219 +  
  10.220 +  override def preContentRemoved(buffer : JEditBuffer, startLine : Int,
  10.221 +			start : Int, numLines : Int, removed : Int) {
  10.222 +    if (col == null)
  10.223 +      col = new Changed(start, 0, removed)
  10.224 +    else if (col.start > start + removed || start > col.start + col.added) { 
  10.225 +      commit()
  10.226 +      col = new Changed(start, 0, removed) 
  10.227 +    }
  10.228 +    else {
  10.229 +      val offset = start - col.start
  10.230 +      val diff = col.added - removed
  10.231 +      val (added, addRemoved) = 
  10.232 +        if (diff < offset) 
  10.233 +          (offset max 0, diff - (offset max 0))
  10.234 +        else 
  10.235 +          (diff - (offset min 0), offset min 0)
  10.236 +      
  10.237 +      col = new Changed(start min col.start, added, col.removed - addRemoved) 
  10.238 +    }
  10.239 +    delayCommit()
  10.240 +  }
  10.241 +
  10.242 +  override def bufferLoaded(buffer : JEditBuffer) { }
  10.243 +  override def foldHandlerChanged(buffer : JEditBuffer) { }
  10.244 +  override def foldLevelChanged(buffer : JEditBuffer, startLine : Int, 
  10.245 +                                endLine : Int) = { }
  10.246 +  override def transactionComplete(buffer : JEditBuffer) = { } 
  10.247 +}
  10.248 \ No newline at end of file
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/jEdit/src/jedit/VFS.scala	Sun Oct 19 16:51:55 2008 +0200
    11.3 @@ -0,0 +1,199 @@
    11.4 +package isabelle.jedit
    11.5 +
    11.6 +import java.io.InputStream
    11.7 +import java.io.OutputStream
    11.8 +import java.io.ByteArrayInputStream
    11.9 +import java.io.ByteArrayOutputStream
   11.10 +import java.io.InputStreamReader
   11.11 +
   11.12 +import java.awt.Component
   11.13 +
   11.14 +import isabelle.Symbol.Interpretation
   11.15 +
   11.16 +import org.gjt.sp.jedit.Buffer
   11.17 +import org.gjt.sp.jedit.View
   11.18 +import org.gjt.sp.jedit.io
   11.19 +import org.gjt.sp.jedit.io.VFSFile
   11.20 +import org.gjt.sp.jedit.io.VFSManager
   11.21 +
   11.22 +object VFS {
   11.23 +  val converter = new Interpretation()
   11.24 +  
   11.25 +  val BUFFER_SIZE = 1024
   11.26 +  
   11.27 +  def inputConverter(in : InputStream) = {
   11.28 +    val reader = new InputStreamReader(in, "UTF-8")
   11.29 +    val buffer = new StringBuffer()
   11.30 +    val array = new Array[Char](BUFFER_SIZE)
   11.31 +    
   11.32 +    var finished = false
   11.33 +    while (! finished) {
   11.34 +      val length = reader.read(array, 0, array.length)
   11.35 +      if (length == -1)
   11.36 +        finished = true
   11.37 +      else
   11.38 +        buffer.append(array, 0, length)
   11.39 +    }
   11.40 +    
   11.41 +    val str = converter.decode(buffer.toString())
   11.42 +    new ByteArrayInputStream(str.getBytes())
   11.43 +  }
   11.44 +  
   11.45 +  class OutputConverter(out : OutputStream) extends ByteArrayOutputStream {
   11.46 +    override def close() {
   11.47 +      out.write(converter.encode(new String(buf, 0, count)).getBytes())
   11.48 +      out.close()
   11.49 +    }
   11.50 +  }
   11.51 +  
   11.52 +  def mapFile(vfs : VFS, base : VFSFile) =
   11.53 +    if (base == null) null else new File(vfs, base)
   11.54 +  
   11.55 +  class File(vfs : VFS, base : VFSFile) extends VFSFile {
   11.56 +    override def getColor() = 
   11.57 +      base.getColor()
   11.58 +    
   11.59 +    override def getDeletePath() = 
   11.60 +      base.getDeletePath()
   11.61 +    
   11.62 +    override def getExtendedAttribute(name : String) =
   11.63 +      base.getExtendedAttribute(name)
   11.64 +
   11.65 +    override def getIcon(expanded : Boolean, openBuffer : Boolean) = 
   11.66 +      base.getIcon(expanded, openBuffer)
   11.67 +
   11.68 +    override def getLength() = 
   11.69 +      base.getLength()  
   11.70 +
   11.71 +    override def getName() =
   11.72 +      base.getName()
   11.73 +
   11.74 +    override def getPath() =
   11.75 +      "isa:" + base.getPath()
   11.76 +
   11.77 +    override def getSymlinkPath() =
   11.78 +      base.getSymlinkPath()
   11.79 +
   11.80 +    override def getType() =
   11.81 +      base.getType()
   11.82 +
   11.83 +    override def getVFS() =
   11.84 +      vfs
   11.85 +
   11.86 +    override def isBinary(session : Object) =
   11.87 +      base.isBinary(session)
   11.88 +
   11.89 +    override def isHidden() =
   11.90 +      base.isHidden()
   11.91 +
   11.92 +    override def isReadable() =
   11.93 +      base.isReadable()
   11.94 +
   11.95 +    override def isWriteable() =
   11.96 +      base.isWriteable()
   11.97 +
   11.98 +    override def setDeletePath(path : String) =
   11.99 +      base.setDeletePath(path)
  11.100 +    
  11.101 +    override def setHidden(hidden : Boolean) =
  11.102 +      base.setHidden(hidden)
  11.103 +      
  11.104 +    override def setLength(length : Long) =
  11.105 +      base.setLength(length)
  11.106 +      
  11.107 +    override def setName(name : String) =
  11.108 +      base.setName(name)
  11.109 +      
  11.110 +    override def setPath(path : String) =
  11.111 +      base.setPath(path)
  11.112 +      
  11.113 +    override def setReadable(readable : Boolean) =
  11.114 +      base.setReadable(readable)
  11.115 +      
  11.116 +    override def setWriteable(writeable : Boolean) =
  11.117 +      base.setWriteable(writeable)
  11.118 +      
  11.119 +    override def setSymlinkPath(symlinkPath : String) =
  11.120 +      base.setSymlinkPath(symlinkPath)
  11.121 +      
  11.122 +    override def setType(fType : Int) =
  11.123 +      base.setType(fType)
  11.124 +  } 
  11.125 +  
  11.126 +}
  11.127 +
  11.128 +/**
  11.129 + * The Isabelle virtual file system for jEdit.
  11.130 + * 
  11.131 + * This filesystem passes every operation on to FileVFS. Just the read and write
  11.132 + * operations are overwritten to convert the xsymbols to unicode on read and
  11.133 + * unicode to xsymbols on write.
  11.134 + * 
  11.135 + * @author Johannes Hölzl <hoelzl@in.tum.de>
  11.136 + */
  11.137 +class VFS extends io.VFS("isa", VFSManager.getVFSForProtocol("file").getCapabilities()) {
  11.138 +  private var baseVFS = VFSManager.getVFSForProtocol("file") 
  11.139 +
  11.140 +  private def cutPath(path : String) = 
  11.141 +    if (path.startsWith("isa:")) path.substring(4) else path
  11.142 +  
  11.143 +  override def createVFSSession(path : String, comp : Component) = 
  11.144 +    baseVFS.createVFSSession(cutPath(path), comp)
  11.145 +  
  11.146 +  override def getCapabilities() = 
  11.147 +    baseVFS.getCapabilities()
  11.148 +  
  11.149 +  override def getExtendedAttributes() = 
  11.150 +    baseVFS.getExtendedAttributes()
  11.151 +  
  11.152 +  override def getParentOfPath(path : String) = 
  11.153 +    "isa:" + baseVFS.getParentOfPath(cutPath(path))
  11.154 +  
  11.155 +  override def constructPath(parent : String, path : String) = 
  11.156 +    "isa:" + baseVFS.constructPath(cutPath(parent), path)
  11.157 +  
  11.158 +  override def getFileName(path : String) = 
  11.159 +    baseVFS.getFileName(path)
  11.160 +  
  11.161 +  override def getFileSeparator() = 
  11.162 +    baseVFS.getFileSeparator()
  11.163 +  
  11.164 +  override def getTwoStageSaveName(path : String) = 
  11.165 +    "isa:" + baseVFS.getTwoStageSaveName(cutPath(path))
  11.166 +  
  11.167 +  override def _canonPath(session : Object, path : String, comp : Component) =
  11.168 +    "isa:" + baseVFS._canonPath(session, cutPath(path), comp)
  11.169 +  
  11.170 +  override def _createInputStream(session : Object, path : String,
  11.171 +                                  ignoreErrors : Boolean, comp : Component) =
  11.172 +    VFS.inputConverter(baseVFS._createInputStream(session, cutPath(path), 
  11.173 +                                                  ignoreErrors, comp))
  11.174 +  
  11.175 +  override def _createOutputStream(session : Object, path : String,
  11.176 +                                   comp : Component) =
  11.177 +    new VFS.OutputConverter(baseVFS._createOutputStream(session, cutPath(path), comp))
  11.178 +  
  11.179 +  override def _delete(session : Object, path : String, comp : Component) =
  11.180 +    baseVFS._delete(session, cutPath(path), comp)
  11.181 +  
  11.182 +  override def _getFile(session : Object, path : String, comp : Component) =
  11.183 +    VFS.mapFile(this, baseVFS._getFile(session, cutPath(path), comp))
  11.184 +
  11.185 +  override def _listFiles(session : Object, path : String, comp :  Component) =
  11.186 +    (baseVFS._listFiles(session, cutPath(path), comp)
  11.187 +            .map(file => VFS.mapFile(this, file)))
  11.188 +
  11.189 +  override def _mkdir(session : Object, path : String, comp : Component) =
  11.190 +    baseVFS._mkdir(session, cutPath(path), comp)
  11.191 +
  11.192 +  override def _rename(session : Object, from : String, to : String,
  11.193 +                       comp : Component) =
  11.194 +    baseVFS._rename(session, cutPath(from), cutPath(to), comp)
  11.195 +
  11.196 +  override def _backup(session : Object, path : String, comp : Component) =
  11.197 +    baseVFS._backup(session, cutPath(path), comp);
  11.198 +
  11.199 +  override def _saveComplete(session : Object, buffer : Buffer, path : String,
  11.200 +                             comp : Component) =
  11.201 +    baseVFS._saveComplete(session, buffer, cutPath(path), comp)
  11.202 +}
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sun Oct 19 16:51:55 2008 +0200
    12.3 @@ -0,0 +1,236 @@
    12.4 +package isabelle.proofdocument
    12.5 +
    12.6 +import java.util.regex.Pattern
    12.7 +
    12.8 +import isabelle.utils.EventSource
    12.9 +
   12.10 +object ProofDocument {
   12.11 +  // Be carefully when changeing this regex. Not only must it handle the 
   12.12 +  // spurious end of a token but also:  
   12.13 +  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
   12.14 +  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
   12.15 +  
   12.16 +  val tokenPattern = 
   12.17 +    Pattern.compile(
   12.18 +      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
   12.19 +      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
   12.20 +      "(\\?'?|')[A-Za-z_0-9.]*|" + 
   12.21 +      "[A-Za-z_0-9.]+|" + 
   12.22 +      "[!#$%&*+-/<=>?@^_|~]+|" +
   12.23 +      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
   12.24 +      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
   12.25 +      "[()\\[\\]{}:;]", Pattern.MULTILINE)
   12.26 +
   12.27 +}
   12.28 +
   12.29 +abstract class ProofDocument[C](text : Text) {
   12.30 +  import ProofDocument._
   12.31 +  
   12.32 +  protected var firstToken : Token[C] = null
   12.33 +  protected var lastToken : Token[C] = null
   12.34 +  private var active = false 
   12.35 +  
   12.36 +  {
   12.37 +    text.changes.add(e => textChanged(e.start, e.added, e.removed))
   12.38 +  }
   12.39 +	
   12.40 +  def activate() : Unit =
   12.41 +    if (! active) {
   12.42 +      active = true
   12.43 +      textChanged(0, text.length, 0)
   12.44 +    }
   12.45 +  
   12.46 +  protected def tokens(start : Token[C], stop : Token[C]) = 
   12.47 +    new Iterator[Token[C]]() {
   12.48 +      var current = start
   12.49 +      def hasNext() = current != stop && current != null
   12.50 +      def next() = { val save = current ; current = current.next ; save }
   12.51 +    }
   12.52 +  
   12.53 +  protected def tokens(start : Token[C]) : Iterator[Token[C]] = 
   12.54 +    tokens(start, null)
   12.55 +  
   12.56 +  protected def tokens() : Iterator[Token[C]] = 
   12.57 +    tokens(firstToken, null)
   12.58 +
   12.59 +  private def checkStart(t : Token[C], P : (Int) => Boolean)
   12.60 +    = t != null && P(t.start)
   12.61 +
   12.62 +  private def checkStop(t : Token[C], P : (Int) => Boolean)
   12.63 +    = t != null && P(t.stop)
   12.64 +  
   12.65 +  private def scan(s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {
   12.66 +    var current = s
   12.67 +    while (current != null) {
   12.68 +      val next = current.next
   12.69 +      if (next == null || f(next))
   12.70 +        return current
   12.71 +      current = next
   12.72 +    }
   12.73 +    return null
   12.74 +  }
   12.75 +
   12.76 +  private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
   12.77 +    if (active == false)
   12.78 +      return
   12.79 +        
   12.80 +    var beforeChange = 
   12.81 +      if (checkStop(firstToken, _ < start)) scan(firstToken, _.stop >= start) 
   12.82 +      else null
   12.83 +    
   12.84 +    var firstRemoved = 
   12.85 +      if (beforeChange != null) beforeChange.next
   12.86 +      else if (checkStart(firstToken, _ <= start + removedLen)) firstToken
   12.87 +      else null 
   12.88 +
   12.89 +    var lastRemoved = scan(firstRemoved, _.start > start + removedLen)
   12.90 +
   12.91 +    var shiftToken = 
   12.92 +      if (lastRemoved != null) lastRemoved
   12.93 +      else if (checkStart(firstToken, _ > start)) firstToken
   12.94 +      else null
   12.95 +    
   12.96 +    while(shiftToken != null) {
   12.97 +      shiftToken.shift(addedLen - removedLen, start)
   12.98 +      shiftToken = shiftToken.next
   12.99 +    }
  12.100 +    
  12.101 +    // scan changed tokens until the end of the text or a matching token is
  12.102 +    // found which is beyond the changed area
  12.103 +    val matchStart = if (beforeChange == null) 0 else beforeChange.stop
  12.104 +    var firstAdded : Token[C] = null
  12.105 +    var lastAdded : Token[C] = null
  12.106 +
  12.107 +    val matcher = tokenPattern.matcher(text.content(matchStart, text.length))
  12.108 +    var finished = false
  12.109 +    var position = 0 
  12.110 +    while(matcher.find(position) && ! finished) {
  12.111 +      position = matcher.end()
  12.112 +			
  12.113 +      val newToken = new Token[C](matcher.start() + matchStart, 
  12.114 +                                  matcher.end() + matchStart,
  12.115 +                                  isStartKeyword(matcher.group()),
  12.116 +                                  matcher.end() - matcher.start() > 2 &&
  12.117 +                                  matcher.group().substring(0, 2) == "(*")
  12.118 +
  12.119 +      if (firstAdded == null)
  12.120 +        firstAdded = newToken
  12.121 +      else {
  12.122 +        newToken.previous = lastAdded
  12.123 +        lastAdded.next = newToken
  12.124 +      }
  12.125 +      lastAdded = newToken
  12.126 +      
  12.127 +      while(checkStop(lastRemoved, _ < newToken.stop) &&
  12.128 +              lastRemoved.next != null)	
  12.129 +        lastRemoved = lastRemoved.next
  12.130 +			
  12.131 +      if (newToken.stop >= start + addedLen && 
  12.132 +            checkStop(lastRemoved, _ == newToken.stop) )
  12.133 +        finished = true
  12.134 +    }
  12.135 +
  12.136 +    var afterChange = if (lastRemoved != null) lastRemoved.next else null
  12.137 +		
  12.138 +    // remove superflous first token-change
  12.139 +    if (firstAdded != null && firstAdded == firstRemoved && 
  12.140 +          firstAdded.stop < start) {
  12.141 +      beforeChange = firstRemoved
  12.142 +      if (lastRemoved == firstRemoved) {
  12.143 +        lastRemoved = null
  12.144 +        firstRemoved = null
  12.145 +      }
  12.146 +      else {
  12.147 +        firstRemoved = firstRemoved.next
  12.148 +        if (firstRemoved == null)
  12.149 +          System.err.println("ERROR")
  12.150 +        assert(firstRemoved != null)
  12.151 +      }
  12.152 +
  12.153 +      if (lastAdded == firstAdded) {
  12.154 +        lastAdded = null
  12.155 +        firstAdded = null
  12.156 +      }
  12.157 +      if (firstAdded != null)
  12.158 +        firstAdded = firstAdded.next
  12.159 +    }
  12.160 +    
  12.161 +    // remove superflous last token-change
  12.162 +    if (lastAdded != null && lastAdded == lastRemoved &&
  12.163 +          lastAdded.start > start + addedLen) {
  12.164 +      afterChange = lastRemoved
  12.165 +      if (firstRemoved == lastRemoved) {
  12.166 +        firstRemoved = null
  12.167 +        lastRemoved = null
  12.168 +      }
  12.169 +      else {
  12.170 +        lastRemoved = lastRemoved.previous
  12.171 +        if (lastRemoved == null)
  12.172 +          System.err.println("ERROR")
  12.173 +        assert(lastRemoved != null)
  12.174 +      }
  12.175 +      
  12.176 +      if (lastAdded == firstAdded) {
  12.177 +        lastAdded = null
  12.178 +        firstAdded = null
  12.179 +      }
  12.180 +      else
  12.181 +        lastAdded = lastAdded.previous
  12.182 +    }
  12.183 +    
  12.184 +    if (firstRemoved == null && firstAdded == null)
  12.185 +      return
  12.186 +    
  12.187 +    if (firstToken == null) {
  12.188 +      firstToken = firstAdded
  12.189 +      lastToken = lastAdded
  12.190 +    }
  12.191 +    else {
  12.192 +      // cut removed tokens out of list
  12.193 +      if (firstRemoved != null)
  12.194 +        firstRemoved.previous = null
  12.195 +      if (lastRemoved != null)
  12.196 +        lastRemoved.next = null
  12.197 +      
  12.198 +      if (firstToken == firstRemoved)
  12.199 +        if (firstAdded != null)
  12.200 +          firstToken = firstAdded
  12.201 +        else
  12.202 +          firstToken = afterChange
  12.203 +      
  12.204 +      if (lastToken == lastRemoved)
  12.205 +        if (lastAdded != null)
  12.206 +          lastToken = lastAdded
  12.207 +        else
  12.208 +          lastToken = beforeChange
  12.209 +      
  12.210 +      // insert new tokens into list
  12.211 +      if (firstAdded != null) {
  12.212 +        firstAdded.previous = beforeChange
  12.213 +        if (beforeChange != null)
  12.214 +          beforeChange.next = firstAdded
  12.215 +        else
  12.216 +          firstToken = firstAdded
  12.217 +      }
  12.218 +      else if (beforeChange != null)
  12.219 +        beforeChange.next = afterChange
  12.220 +      
  12.221 +      if (lastAdded != null) {
  12.222 +        lastAdded.next = afterChange
  12.223 +        if (afterChange != null)
  12.224 +          afterChange.previous = lastAdded
  12.225 +        else
  12.226 +          lastToken = lastAdded
  12.227 +      }
  12.228 +      else if (afterChange != null)
  12.229 +        afterChange.previous = beforeChange
  12.230 +    }
  12.231 +    
  12.232 +    tokenChanged(beforeChange, afterChange, firstRemoved)
  12.233 +  }
  12.234 +  
  12.235 +  protected def isStartKeyword(str : String) : Boolean;
  12.236 +  
  12.237 +  protected def tokenChanged(start : Token[C], stop : Token[C], 
  12.238 +                             removed : Token[C]) 
  12.239 +}
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Sun Oct 19 16:51:55 2008 +0200
    13.3 @@ -0,0 +1,14 @@
    13.4 +package isabelle.proofdocument
    13.5 +
    13.6 +import isabelle.utils.EventSource
    13.7 +
    13.8 +object Text {
    13.9 +  class Changed(val start : Int, val added : Int, val removed : Int) { }
   13.10 +}
   13.11 +
   13.12 +trait Text {
   13.13 +  def content(start : Int, stop : Int) : String
   13.14 +  def length : Int
   13.15 +  
   13.16 +  def changes : EventSource[Text.Changed]
   13.17 +}
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Sun Oct 19 16:51:55 2008 +0200
    14.3 @@ -0,0 +1,31 @@
    14.4 +package isabelle.proofdocument
    14.5 +
    14.6 +class Token[C](var start : Int, var stop : Int, val isCommandStart : Boolean,
    14.7 +               val isComment : Boolean) {
    14.8 +  var next : Token[C] = null
    14.9 +  var previous : Token[C] = null
   14.10 +  var command : C = null.asInstanceOf[C]
   14.11 +  
   14.12 +  def length = stop - start
   14.13 +
   14.14 +  def shift(offset : Int, bottomClamp : Int) {
   14.15 +    start = bottomClamp max (start + offset)
   14.16 +    stop = bottomClamp max (stop + offset)
   14.17 +  }
   14.18 +  
   14.19 +  override def hashCode() : Int = (31 + start) * 31 + stop
   14.20 +
   14.21 +  override def equals(obj : Any) : Boolean = {
   14.22 +    if (super.equals(obj))
   14.23 +      return true;
   14.24 +    
   14.25 +    if (null == obj)
   14.26 +      return false;
   14.27 +    
   14.28 +    obj match {
   14.29 +      case other: Token[_] => 
   14.30 +        (start == other.start) && (stop == other.stop)
   14.31 +      case other: Any => false  
   14.32 +    }
   14.33 +  }
   14.34 +}
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Tools/jEdit/src/proofdocument/tests/TestProofDocument.scala	Sun Oct 19 16:51:55 2008 +0200
    15.3 @@ -0,0 +1,139 @@
    15.4 +package isabelle.proofdocument.tests
    15.5 +
    15.6 +import org.testng.annotations._
    15.7 +import org.testng.Assert._
    15.8 +  
    15.9 +import isabelle.proofdocument._
   15.10 +import isabelle.utils.EventSource
   15.11 +
   15.12 +class TextMockup() extends Text {
   15.13 +  var content = ""
   15.14 +  val changes = new EventSource[Text.Changed]
   15.15 +
   15.16 +  def content(start : Int, stop : Int) = content.substring(start, stop)
   15.17 +  def length = content.length
   15.18 +  
   15.19 +  def change(start : Int, added : String, removed : Int) {
   15.20 +    content = content.substring(0, start) + added + content.substring(start + removed)
   15.21 +    changes.fire(new Text.Changed(start, added.length, removed))
   15.22 +  }
   15.23 +} 
   15.24 +
   15.25 +class ProofDocumentTest(text : Text) extends ProofDocument[String](text) {
   15.26 +  var start : Token[String] = null
   15.27 +  var stop : Token[String] = null
   15.28 +  var removed : Token[String] = null
   15.29 +
   15.30 +  def isStartKeyword(s : String) : Boolean = false
   15.31 +  
   15.32 +  def tokenChanged(start_ : Token[String], stop_ : Token[String], 
   15.33 +                   removed_ : Token[String]) {
   15.34 +    start = start_
   15.35 +    stop = stop_
   15.36 +    removed = removed_
   15.37 +  }
   15.38 +  
   15.39 +  override def tokens = super.tokens
   15.40 +  override def tokens(s : Token[String]) = super.tokens(s)
   15.41 +  override def tokens(s : Token[String], e : Token[String]) = super.tokens(s, e)
   15.42 +  
   15.43 +  def first = firstToken
   15.44 +  def last = lastToken
   15.45 +  
   15.46 +  def checkLinks(first : Token[String], last : Token[String]) {
   15.47 +    var iter = first
   15.48 +    var prev : Token[String] = null
   15.49 +    
   15.50 +    while(iter != null) {
   15.51 +      assert(iter.previous == prev)
   15.52 +      prev = iter
   15.53 +      iter = iter.next
   15.54 +    }
   15.55 +    if (last != null)
   15.56 +      assert(prev == last)
   15.57 +  }
   15.58 +}
   15.59 +
   15.60 +class TestProofDocument {
   15.61 +  private def ranges(ts : Iterator[Token[String]]) =
   15.62 +    (for (t <- ts) yield (t.start, t.stop)).toList
   15.63 +  
   15.64 +  @Test
   15.65 +  def testParsing() {
   15.66 +    def check(tokens : String*) = {
   15.67 +      var content = ""
   15.68 +      var structure = Nil : List[(Int, Int)]
   15.69 +    
   15.70 +      for(tok <- tokens) {
   15.71 +        if (tok != " ")
   15.72 +          structure = (content.length, content.length + tok.length) :: structure
   15.73 +        content = content + tok
   15.74 +      }
   15.75 +      
   15.76 +      val text = new TextMockup()
   15.77 +      val document = new ProofDocumentTest(text)
   15.78 +      text.change(0, content, 0)
   15.79 +      document.checkLinks(document.first, document.last)
   15.80 +      assertEquals(ranges(document.tokens), structure.reverse)
   15.81 +    }
   15.82 +  
   15.83 +    check("lemma", " " , "fixes", " ", "A", " ", ":", ":", " ", "'a", " ", 
   15.84 +          "shows", "\"True\"", " ", "using", "`A = A`", "by", "(", "auto", " ", 
   15.85 +          "simp", " ", "add", ":", "refl", ")")
   15.86 +  }
   15.87 +  
   15.88 +  @Test
   15.89 +  def testChanging() {
   15.90 +    val text = new TextMockup()
   15.91 +    val document = new ProofDocumentTest(text)
   15.92 +
   15.93 +    def compare(start : Int, add : String, remove : Int) {
   15.94 +      val oldDocument = ranges(document.tokens)
   15.95 +      text.change(start, add, remove)
   15.96 +      document.checkLinks(document.first, document.last)
   15.97 +      document.checkLinks(document.removed, null)
   15.98 +      
   15.99 +      val offset = remove - add.length
  15.100 +      val before = if (document.start == null) Nil 
  15.101 +                   else ranges(document.tokens(document.first, document.start.next))
  15.102 +      val after = (for(t <- document.tokens(document.stop)) 
  15.103 +                     yield (t.start + offset, t.stop + offset)).toList
  15.104 +      val removed = ranges(document.tokens(document.removed))
  15.105 +      assertEquals((before ++ removed ++ after).length, oldDocument.length, 
  15.106 +                   "Mismatch on token count")
  15.107 +      assertEquals(before, oldDocument.take(before.length),
  15.108 +                   "Tokens before changed part")
  15.109 +      assertEquals(after, oldDocument.drop(before.length + removed.length),
  15.110 +                   "Tokens before changed part")
  15.111 +    
  15.112 +      val newText = new TextMockup()
  15.113 +      val newDocument = new ProofDocumentTest(newText)
  15.114 +      newText.change(0, text.content, 0)
  15.115 +      newDocument.checkLinks(newDocument.first, newDocument.last)
  15.116 +
  15.117 +      assertEquals(ranges(document.tokens), ranges(newDocument.tokens),
  15.118 +                   "Mismatch on entirely reparsed document")
  15.119 +    }
  15.120 +  
  15.121 +    val s = """lemma fixes a :: nat assumes T: \"A\" shows \"B ==> A\" using `A` by auto"""
  15.122 +    compare(0, s, text.content.length)
  15.123 +    compare(0, "(*", 0)
  15.124 +    compare(text.content.length, "*)", 0)
  15.125 +    compare(0, "", 2)
  15.126 +    compare(1, "", 7)
  15.127 +    
  15.128 +    compare(0, "test :: 12 34", text.content.length)
  15.129 +    compare(6, "", 1)
  15.130 +    compare(6, ":", 0)
  15.131 +    compare(8, "56", 2)
  15.132 +    compare(2, "", 4)
  15.133 +    
  15.134 +    compare(0, "test  :: 12 34", text.content.length)
  15.135 +    compare(5, "test 1 2", 0)
  15.136 +    compare(4, " test 2 3", 0)
  15.137 +
  15.138 +    compare(0, "theory Scratch\nimports Main\nbegin\n\nlemma test_x: fixes X :: nat shows \"∃ X. X > 0\" by auto\n\nend", text.content.length)
  15.139 +    compare(72, "", 11)
  15.140 +    compare(71, "", 1)
  15.141 +  }
  15.142 +}
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Oct 19 16:51:55 2008 +0200
    16.3 @@ -0,0 +1,65 @@
    16.4 +package isabelle.prover
    16.5 +
    16.6 +import isabelle.proofdocument.Token
    16.7 +import isabelle.{ YXML, XML }
    16.8 +
    16.9 +object Command {
   16.10 +  object Phase extends Enumeration {
   16.11 +    val UNPROCESSED = Value("UNPROCESSED")
   16.12 +    val FINISHED = Value("FINISHED")
   16.13 +    val REMOVE = Value("REMOVE")
   16.14 +    val REMOVED = Value("REMOVED")
   16.15 +    val FAILED = Value("FAILED")
   16.16 +  }
   16.17 +
   16.18 +  private var nextId : Long = 0
   16.19 +  def generateId : Long = {
   16.20 +    nextId = nextId + 1
   16.21 +    return nextId
   16.22 +  }
   16.23 +  
   16.24 +  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
   16.25 +}
   16.26 +
   16.27 +class Command(val first : Token[Command], val last : Token[Command]) {
   16.28 +  import Command._
   16.29 +  
   16.30 +  {
   16.31 +    var t = first
   16.32 +    while(t != null) {
   16.33 +      t.command = this
   16.34 +      t = if (t == last) null else t.next
   16.35 +    }
   16.36 +  }
   16.37 +  
   16.38 +  val id : Long = generateId
   16.39 +  var phase = Phase.UNPROCESSED
   16.40 +	
   16.41 +  var results = Nil : List[XML.Tree]
   16.42 +  
   16.43 +  def idString = java.lang.Long.toString(id, 36)
   16.44 +  def document = XML.document(results match {
   16.45 +                                case Nil => XML.Elem("message", List(), List())
   16.46 +                                case List(elem) => elem
   16.47 +                                case _ => 
   16.48 +                                  XML.Elem("messages", List(), List(results.first,
   16.49 +                                                                    results.last))
   16.50 +                              }, "style")
   16.51 +  def addResult(tree : XML.Tree) {
   16.52 +    results = results ::: List(tree)
   16.53 +  }
   16.54 +
   16.55 +  def next = if (last.next != null) last.next.command else null
   16.56 +  def previous = if (first.previous != null) first.previous.command else null
   16.57 +
   16.58 +  def start = first start
   16.59 +  def stop = last stop
   16.60 +  
   16.61 +  def properStart = start
   16.62 +  def properStop = {
   16.63 +    var i = last
   16.64 +    while (i != first && i.isComment)
   16.65 +      i = i.previous
   16.66 +    i.stop
   16.67 +  }  	
   16.68 +}
   16.69 \ No newline at end of file
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Tools/jEdit/src/prover/CommandChangeInfo.scala	Sun Oct 19 16:51:55 2008 +0200
    17.3 @@ -0,0 +1,3 @@
    17.4 +package isabelle.prover
    17.5 +
    17.6 +class CommandChangeInfo(val command : Command)
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Tools/jEdit/src/prover/Document.scala	Sun Oct 19 16:51:55 2008 +0200
    18.3 @@ -0,0 +1,152 @@
    18.4 +package isabelle.prover
    18.5 +
    18.6 +import isabelle.proofdocument.{ ProofDocument, Token, Text }
    18.7 +
    18.8 +import isabelle.utils.EventSource
    18.9 +
   18.10 +object Document {
   18.11 +  class StructureChange(val beforeChange : Command,
   18.12 +                        val addedCommands : List[Command],
   18.13 +                        val removedCommands : List[Command])
   18.14 +}
   18.15 +
   18.16 +class Document(text : Text, prover : Prover) extends ProofDocument[Command](text) 
   18.17 +{ 
   18.18 +  val structuralChanges = new EventSource[Document.StructureChange]() 
   18.19 +  
   18.20 +  def isStartKeyword(s : String) = prover.commandKeywords.contains(s) 
   18.21 +  
   18.22 +  def commands() = new Iterator[Command] {
   18.23 +    var current = firstToken
   18.24 +    def hasNext() = current != null
   18.25 +    def next() = { try {val s = current.command ; current = s.last.next ; s}
   18.26 +    catch { case error : NullPointerException => 
   18.27 +      System.err.println("NPE!")
   18.28 +      throw error
   18.29 +    } 
   18.30 +    }
   18.31 +  }
   18.32 +
   18.33 +  def getContent(cmd : Command) = text.content(cmd.properStart, cmd.properStop)
   18.34 +
   18.35 +  def getNextCommandContaining(pos : Int) : Command = {
   18.36 +    for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
   18.37 +    return null
   18.38 +  }
   18.39 +  
   18.40 +  override def tokenChanged(start : Token[Command], stop : Token[Command], 
   18.41 +                            removed : Token[Command]) {
   18.42 +    var removedCommands : List[Command] = Nil
   18.43 +    var first : Command = null
   18.44 +    var last : Command = null
   18.45 +    
   18.46 +    for(t <- tokens(removed)) {
   18.47 +      if (first == null)
   18.48 +        first = t.command
   18.49 +      if (t.command != last)
   18.50 +        removedCommands = t.command :: removedCommands
   18.51 +      last = t.command
   18.52 +    }
   18.53 +
   18.54 +    var before : Command = null
   18.55 +    if (! removedCommands.isEmpty) {
   18.56 +      if (first.first == removed) {
   18.57 +        if (start == null)
   18.58 +          before = null
   18.59 +        else
   18.60 +          before = start.command
   18.61 +      }
   18.62 +      else
   18.63 +        before = first.previous
   18.64 +    }
   18.65 +    
   18.66 +    var addedCommands : List[Command] = Nil
   18.67 +    var scan : Token[Command] = null
   18.68 +    if (start != null) {
   18.69 +      val next = start.next
   18.70 +      if (first != null && first.first != removed) {
   18.71 +        scan = first.first
   18.72 +        if (before == null)
   18.73 +          before = first.previous
   18.74 +      }
   18.75 +      else if (next != null && next != stop) {
   18.76 +        if (next.isCommandStart) {
   18.77 +          before = start.command
   18.78 +          scan = next
   18.79 +        }
   18.80 +        else if (first == null || first.first == removed) {
   18.81 +          first = start.command
   18.82 +          removedCommands = first :: removedCommands
   18.83 +          scan = first.first
   18.84 +          if (before == null)
   18.85 +            before = first.previous
   18.86 +        }
   18.87 +        else {
   18.88 +          scan = first.first
   18.89 +          if (before == null)
   18.90 +            before = first.previous
   18.91 +        }
   18.92 +      }
   18.93 +    }
   18.94 +    else
   18.95 +      scan = firstToken
   18.96 +    
   18.97 +    var stopScan : Token[Command] = null
   18.98 +    if (stop != null) {
   18.99 +      if (stop == stop.command.first)
  18.100 +        stopScan = stop
  18.101 +      else
  18.102 +        stopScan = stop.command.last.next
  18.103 +    }
  18.104 +    else if (last != null)
  18.105 +      stopScan = last.last.next
  18.106 +    else
  18.107 +      stopScan = null
  18.108 +		
  18.109 +    var cmdStart : Token[Command] = null
  18.110 +    var cmdStop : Token[Command] = null
  18.111 +    var overrun = false
  18.112 +    var finished = false
  18.113 +    while (scan != null && !finished) {
  18.114 +      if (scan == stopScan)	{
  18.115 +        if (scan.isCommandStart)
  18.116 +          finished = true
  18.117 +        else
  18.118 +          overrun = true
  18.119 +      }
  18.120 +      
  18.121 +      if (scan.isCommandStart && cmdStart != null && !finished) {
  18.122 +        if (! overrun) {
  18.123 +          addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
  18.124 +          cmdStart = scan
  18.125 +          cmdStop = scan
  18.126 +        }
  18.127 +        else
  18.128 +          finished = true
  18.129 +      }
  18.130 +      else if (! finished) {
  18.131 +        if (cmdStart == null)
  18.132 +          cmdStart = scan
  18.133 +        cmdStop = scan
  18.134 +      }
  18.135 +      if (overrun && !finished) {
  18.136 +        if (scan.command != last)
  18.137 +          removedCommands = scan.command :: removedCommands
  18.138 +        last = scan.command
  18.139 +      }
  18.140 +      
  18.141 +      if (!finished)
  18.142 +        scan = scan.next
  18.143 +    }
  18.144 +    
  18.145 +    if (cmdStart != null)
  18.146 +      addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
  18.147 +    
  18.148 +    // relink commands
  18.149 +    addedCommands = addedCommands.reverse
  18.150 +    removedCommands = removedCommands.reverse
  18.151 +    
  18.152 +    structuralChanges.fire(new Document.StructureChange(before, addedCommands, 
  18.153 +                                                        removedCommands))
  18.154 +  }
  18.155 +}
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Oct 19 16:51:55 2008 +0200
    19.3 @@ -0,0 +1,185 @@
    19.4 +package isabelle.prover
    19.5 +
    19.6 +import scala.collection.mutable.{ HashMap, HashSet }
    19.7 +
    19.8 +import java.util.Properties
    19.9 +
   19.10 +import javax.swing.SwingUtilities
   19.11 +
   19.12 +import isabelle.proofdocument.{ ProofDocument, Text }
   19.13 +import isabelle.IsabelleProcess.Result
   19.14 +import isabelle.YXML.parse_failsafe
   19.15 +import isabelle.XML.{ Elem, Tree }
   19.16 +import isabelle.Symbol.Interpretation
   19.17 +import isabelle.IsabelleSyntax.{ encode_properties, encode_string }
   19.18 +
   19.19 +import isabelle.utils.EventSource
   19.20 +
   19.21 +import Command.Phase
   19.22 +
   19.23 +class Prover() {
   19.24 +  val converter = new Interpretation()
   19.25 +
   19.26 +  private var _logic = "HOL"
   19.27 +  private var process = null : IsabelleProcess
   19.28 +  private var commands = new HashMap[String, Command]
   19.29 +  
   19.30 +  val commandKeywords = new HashSet[String]
   19.31 +  private var initialized = false
   19.32 +    
   19.33 +  val activated = new EventSource[Unit]
   19.34 +  val commandInfo = new EventSource[CommandChangeInfo]
   19.35 +  val outputInfo = new EventSource[String]
   19.36 +  var document = null : Document
   19.37 +  
   19.38 +  var workerThread = new Thread("isabelle.Prover: worker") {
   19.39 +    override def run() : Unit = {
   19.40 +      while (true) {
   19.41 +        val r = process.get_result
   19.42 +        
   19.43 +        val id = if (r.props != null) r.props.getProperty("id") else null
   19.44 +        val st = if (id != null) commands.getOrElse(id, null) else null
   19.45 +        
   19.46 +        if (r.kind == IsabelleProcess.Kind.EXIT)
   19.47 +          return
   19.48 +        else if (r.kind == IsabelleProcess.Kind.STDOUT 
   19.49 +                 || r.kind == IsabelleProcess.Kind.STDIN)
   19.50 +          inUIThread(() => outputInfo.fire(r.result))
   19.51 +        else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
   19.52 +          initialized = true
   19.53 +          inUIThread(() => 
   19.54 +            if (document != null) {
   19.55 +              document.activate()
   19.56 +              activated.fire(())
   19.57 +            }
   19.58 +          )
   19.59 +        }
   19.60 +        else {
   19.61 +          val tree = parse_failsafe(converter.decode(r.result))
   19.62 +          tree match {
   19.63 +            case Elem("message", _, List(Elem("command_decl", List(("name", name), 
   19.64 +                                                                   ("kind", _)), _))) =>
   19.65 +              commandKeywords.addEntry(name)
   19.66 +            case _ =>
   19.67 +              if (st != null)
   19.68 +                handleResult(st, r, tree)
   19.69 +          }
   19.70 +        }
   19.71 +        
   19.72 +      }
   19.73 +    }
   19.74 +  }
   19.75 +  
   19.76 +  def handleResult(st : Command, r : Result, tree : XML.Tree) {
   19.77 +    def fireChange() = 
   19.78 +      inUIThread(() => commandInfo.fire(new CommandChangeInfo(st)))
   19.79 +    
   19.80 +    r.kind match {
   19.81 +      case IsabelleProcess.Kind.ERROR => 
   19.82 +        if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
   19.83 +          st.phase = Phase.FAILED
   19.84 +        st.addResult(tree)
   19.85 +        fireChange()
   19.86 +        
   19.87 +      case IsabelleProcess.Kind.WRITELN =>
   19.88 +        st.addResult(tree)
   19.89 +        fireChange()
   19.90 +        
   19.91 +      case IsabelleProcess.Kind.PRIORITY =>
   19.92 +        st.addResult(tree)
   19.93 +        fireChange()
   19.94 +              
   19.95 +      case IsabelleProcess.Kind.WARNING =>
   19.96 +        st.addResult(tree)
   19.97 +        fireChange()
   19.98 +              
   19.99 +      case IsabelleProcess.Kind.STATUS =>
  19.100 +        val state = tree match { case Elem("message", _, 
  19.101 +                                           Elem (name, _, _) :: _) => name
  19.102 +                                 case _ => null }
  19.103 +        if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
  19.104 +          state match {
  19.105 +            case "finished" => 
  19.106 +              st.phase = Phase.FINISHED
  19.107 +              fireChange()
  19.108 +              
  19.109 +            case "unprocessed" => 
  19.110 +              st.phase = Phase.UNPROCESSED
  19.111 +              fireChange()
  19.112 +                    
  19.113 +            case "failed" => 
  19.114 +              st.phase = Phase.FAILED
  19.115 +              fireChange()
  19.116 +                    
  19.117 +            case "removed" =>
  19.118 +              commands.removeKey(st.idString)
  19.119 +              st.phase = Phase.REMOVED
  19.120 +              fireChange()
  19.121 +              
  19.122 +            case _ =>
  19.123 +          }
  19.124 +        }
  19.125 +      case _ =>
  19.126 +    }
  19.127 +  }
  19.128 +  
  19.129 +  def logic = _logic
  19.130 +  
  19.131 +  def start(logic : String) {
  19.132 +    if (logic != null)
  19.133 +      _logic = logic
  19.134 +    process = new IsabelleProcess("-m", "xsymbols", _logic)
  19.135 +    workerThread.start
  19.136 +  }
  19.137 +
  19.138 +  def stop() {
  19.139 +    process.kill
  19.140 +  }
  19.141 +  
  19.142 +  private def inUIThread(runnable : () => Unit) {
  19.143 +    SwingUtilities invokeAndWait new Runnable() {
  19.144 +      override def run() { runnable() }
  19.145 +    }
  19.146 +  }
  19.147 +  
  19.148 +  def setDocument(text : Text, path : String) {
  19.149 +    this.document = new Document(text, this)
  19.150 +    process.ML("ThyLoad.add_path " + encode_string(path))
  19.151 +
  19.152 +    document.structuralChanges.add(changes => {
  19.153 +      for (cmd <- changes.removedCommands) remove(cmd)
  19.154 +      for (cmd <- changes.addedCommands) send(cmd)
  19.155 +    })
  19.156 +    if (initialized) {
  19.157 +      document.activate()
  19.158 +      activated.fire(())
  19.159 +    }
  19.160 +  }
  19.161 +  
  19.162 +  private def send(cmd : Command) {
  19.163 +    commands.put(cmd.idString, cmd)
  19.164 +    
  19.165 +    val props = new Properties()
  19.166 +    props.setProperty("id", cmd.idString)
  19.167 +    props.setProperty("offset", "1")
  19.168 +
  19.169 +    val content = converter.encode(document.getContent(cmd))
  19.170 +    process.output_sync("Isar.command " 
  19.171 +                        + encode_properties(props)
  19.172 +                        + " "
  19.173 +                        + encode_string(content))
  19.174 +    
  19.175 +    process.output_sync("Isar.insert "
  19.176 +                        + encode_string(if (cmd.previous == null) "" 
  19.177 +                                        else cmd.previous.idString)
  19.178 +                        + " "
  19.179 +                        + encode_string(cmd.idString))
  19.180 +    
  19.181 +    cmd.phase = Phase.UNPROCESSED
  19.182 +  }
  19.183 +  
  19.184 +  def remove(cmd : Command) {
  19.185 +    cmd.phase = Phase.REMOVE
  19.186 +    process.output_sync("Isar.remove " + encode_string(cmd.idString))
  19.187 +  }
  19.188 +}
  19.189 \ No newline at end of file
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Tools/jEdit/src/utils/EventSource.scala	Sun Oct 19 16:51:55 2008 +0200
    20.3 @@ -0,0 +1,12 @@
    20.4 +package isabelle.utils
    20.5 +
    20.6 +import scala.collection.mutable.HashSet
    20.7 +
    20.8 +class EventSource[Event] {
    20.9 +  private val handlers = new HashSet[(Event) => Unit]()
   20.10 +
   20.11 +  def add(handler : (Event) => Unit) { handlers += handler }
   20.12 +  def remove(handler : (Event) => Unit) { handlers -= handler }
   20.13 +	
   20.14 +  def fire(event : Event) { for(h <- handlers) h(event) }
   20.15 +}
   20.16 \ No newline at end of file