--- a/src/Tools/jEdit/plugin/actions.xml Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml Thu Dec 18 01:10:20 2008 +0100
@@ -16,10 +16,10 @@
</ACTION>
<ACTION NAME="Isabelle.activate">
<CODE>
- isabelle.jedit.Plugin$.MODULE$.plugin().activate(view);
+ isabelle.jedit.Plugin$.MODULE$.plugin().install(view);
</CODE>
<IS_SELECTED>
- return view.getBuffer().getMode().getName() == "isabelle";
+ return isabelle.jedit.Plugin$.MODULE$.plugin().is_active(view.getBuffer());
</IS_SELECTED>
</ACTION>
</ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/services.xml Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/plugin/services.xml Thu Dec 18 01:10:20 2008 +0100
@@ -1,7 +1,7 @@
<?xml version="1.0"?>
<!DOCTYPE SERVICES SYSTEM "services.dtd">
<SERVICES>
- <SERVICE CLASS="sidekick.SideKickParser" NAME="isabelle">
+ <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
new isabelle.prover.IsabelleSKParser();
</SERVICE>
<SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
--- a/src/Tools/jEdit/src/jedit/OutputDockable.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/OutputDockable.scala Thu Dec 18 01:10:20 2008 +0100
@@ -7,14 +7,7 @@
import org.gjt.sp.jedit.View
class OutputDockable(view : View, position : String) extends JPanel {
- {
- val textView = new JTextArea()
-
- setLayout(new GridLayout(1, 1))
- add(new JScrollPane(textView))
-
- textView.append("== Isabelle output ==\n")
-
- Plugin.plugin.prover.outputInfo.add( text => textView.append(text) )
- }
+
+ setLayout(new GridLayout(1, 1))
+ add(new JScrollPane(new JTextArea("No Prover running")))
}
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Dec 18 01:10:20 2008 +0100
@@ -1,25 +1,3 @@
-/*
- * ErrorOverview.java - Error overview component
- * :tabSize=8:indentSize=8:noTabs=false:
- * :folding=explicit:collapseFolds=1:
- *
- * Copyright (C) 2003 Slava Pestov
- *
- * This program is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
- */
-
package isabelle.jedit
import isabelle.prover.Command
@@ -33,14 +11,15 @@
import org.gjt.sp.jedit.buffer.JEditBuffer;
import org.gjt.sp.jedit._
-class PhaseOverviewPanel(textarea : JEditTextArea) extends JPanel(new BorderLayout) {
+class PhaseOverviewPanel(prover : isabelle.prover.Prover) extends JPanel(new BorderLayout) {
private val WIDTH = 10
private val HILITE_HEIGHT = 2
+ var textarea : JEditTextArea = null
- Plugin.plugin.prover.commandInfo.add(cc => {
- paintCommand(cc.command,textarea.getBuffer, getGraphics)
- })
+ val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
+ prover.commandInfo.add(cc => repaint_delay.delay_or_ignore())
+
setRequestFocusEnabled(false);
addMouseListener(new MouseAdapter {
@@ -97,9 +76,9 @@
super.paintComponent(gfx)
val buffer = textarea.getBuffer
-
- for(c <- Plugin.plugin.prover.document.commands)
+ for(c <- prover.document.commands)
paintCommand(c, buffer, gfx)
+
}
override def getPreferredSize : Dimension =
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Thu Dec 18 01:10:20 2008 +0100
@@ -2,7 +2,7 @@
import java.awt.Font
import java.io.{ FileInputStream, IOException }
-
+import javax.swing.JScrollPane
import isabelle.utils.EventSource
@@ -10,7 +10,11 @@
import isabelle.IsabelleSystem
-import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
+import scala.collection.mutable.HashMap
+
+import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View }
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.JEditTextArea
import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
object Plugin {
@@ -23,45 +27,68 @@
jEdit.setProperty(OPTION_PREFIX + name, value)
var plugin : Plugin = null
+ def prover(buffer : JEditBuffer) = plugin.prover_setup(buffer).get.prover
+ def prover_setup(buffer : JEditBuffer) = plugin.prover_setup(buffer).get
+
}
class Plugin extends EBPlugin {
import Plugin._
-
- val prover = new Prover()
- var theoryView : TheoryView = null
-
- var viewFont : Font = null
+
+ private val mapping = new HashMap[JEditBuffer, ProverSetup]
+
+ var viewFont : Font = null
val viewFontChanged = new EventSource[Font]
-
- private var _selectedState : Command = null
-
- val stateUpdate = new EventSource[Command]
-
- def selectedState = _selectedState
- def selectedState_=(newState : Command) {
- _selectedState = newState
- stateUpdate fire newState
+
+ def install(view : View) {
+ val buffer = view.getBuffer
+ mapping.get(buffer) match{
+ case None =>{
+ val prover_setup = new ProverSetup(buffer)
+ mapping.update(buffer, prover_setup)
+ prover_setup.activate(view)
+ }
+ case _ => System.err.println("Already installed plugin on Buffer")
+ }
}
-
- def activate(view : View) {
- val logic = property("logic")
- theoryView = new TheoryView(prover, view.getBuffer())
- prover.start(if (logic == null) logic else "HOL")
- val dir = view.getBuffer().getDirectory()
- prover.setDocument(theoryView,
- if (dir.startsWith(VFS_PREFIX)) dir.substring(VFS_PREFIX.length) else dir)
- TheoryView.activateTextArea(view.getTextArea())
+
+ def uninstall(view : View) {
+ val buffer = view.getBuffer
+ mapping.removeKey(buffer) match{
+ case None => System.err.println("No Plugin installed on this Buffer")
+ case Some(proversetup) =>
+ proversetup.deactivate
+ }
}
+
+ def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
+ def is_active (buffer : JEditBuffer) = mapping.get(buffer) match { case None => false case _ => true}
override def handleMessage(msg : EBMessage) = msg match {
case epu : EditPaneUpdate => epu.getWhat() match {
case EditPaneUpdate.BUFFER_CHANGED =>
- TheoryView.activateTextArea(epu.getEditPane().getTextArea())
-
+ mapping get epu.getEditPane.getBuffer match {
+ //only activate 'isabelle'-buffers!
+ case None =>
+ case Some(prover_setup) =>
+ prover_setup.theory_view.activate
+ val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("Isabelle_output")
+ if(dockable != null) {
+ val output_dockable = dockable.asInstanceOf[OutputDockable]
+ 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
+ }
+ }
+ }
case EditPaneUpdate.BUFFER_CHANGING =>
- TheoryView.deactivateTextArea(epu.getEditPane().getTextArea())
-
+ val buffer = epu.getEditPane.getBuffer
+ if(buffer != null) mapping get buffer match {
+ //only deactivate 'isabelle'-buffers!
+ case None =>
+ case Some(prover_setup) => prover_setup.theory_view.deactivate
+ }
case _ =>
}
@@ -73,7 +100,7 @@
val fontStream = new FileInputStream(path)
val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
viewFont = font.deriveFont(Font.PLAIN, size)
-
+
viewFontChanged.fire(viewFont)
}
catch {
@@ -83,7 +110,7 @@
override def start() {
plugin = this
-
+
if (property("font-path") != null && property("font-size") != null)
try {
setFont(property("font-path"), property("font-size").toFloat)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Dec 18 01:10:20 2008 +0100
@@ -0,0 +1,87 @@
+/*
+ * BufferExtension.scala
+ *
+ * To change this template, choose Tools | Template Manager
+ * and open the template in the editor.
+ */
+
+package isabelle.jedit
+
+import isabelle.utils.EventSource
+
+import isabelle.prover.{ Prover, Command }
+import org.w3c.dom.Document
+
+import isabelle.IsabelleSystem
+
+import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
+
+import javax.swing.{JTextArea, JScrollPane}
+
+class ProverSetup(buffer : JEditBuffer) {
+
+ val prover = new Prover()
+ var theory_view : TheoryView = null
+
+ private var _selectedState : Command = null
+
+ val stateUpdate = new EventSource[Command]
+
+ def selectedState = _selectedState
+ def selectedState_=(newState : Command) {
+ _selectedState = newState
+ stateUpdate fire newState
+ }
+
+ val output_text_view = new JTextArea("== Isabelle output ==\n")
+
+ def activate(view : View) {
+ val logic = Plugin.property("logic")
+ prover.start(if (logic == null) logic else "HOL")
+ val buffer = view.getBuffer
+ val dir = buffer.getDirectory()
+
+ theory_view = new TheoryView(view.getTextArea)
+ prover.setDocument(theory_view ,
+ if (dir.startsWith(Plugin.VFS_PREFIX)) dir.substring(Plugin.VFS_PREFIX.length) else dir)
+ theory_view.activate
+ prover.outputInfo.add( text => {
+ output_text_view.append(text)
+ val dockable = view.getDockableWindowManager.getDockable("Isabelle_output")
+ //link process output if dockable is active
+ if(dockable != null) {
+ val output_dockable = dockable.asInstanceOf[OutputDockable]
+ 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
+ }
+ }
+ })
+
+ //register for state-view
+ stateUpdate.add(state => {
+ val state_view = view.getDockableWindowManager.getDockable("Isabelle_state")
+ val state_panel = if(state_view != null) state_view.asInstanceOf[StateViewDockable].panel else null
+ if(state_panel != null){
+ if (state == null)
+ state_panel.setDocument(null : Document)
+ else
+ state_panel.setDocument(state.results_xml, UserAgent.baseURL)
+ }
+ })
+
+ //register for theory-view
+
+ // could also use this:
+ // prover.commandInfo.add(c => Plugin.theory_view.repaint(c.command))
+
+ }
+
+ def deactivate {
+ //TODO: clean up!
+ }
+
+}
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Thu Dec 18 01:10:20 2008 +0100
@@ -166,7 +166,7 @@
// TODO: register
- Plugin.plugin.prover.allInfo.add(add_result(_))
+ //Plugin.plugin.prover.allInfo.add(add_result(_))
}
//Concrete Implementations
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Thu Dec 18 01:10:20 2008 +0100
@@ -6,41 +6,31 @@
import isabelle.IsabelleSystem.getenv
-import org.w3c.dom.Document
-
import org.xhtmlrenderer.simple.XHTMLPanel
import org.xhtmlrenderer.context.AWTFontResolver
import org.gjt.sp.jedit.View
class StateViewDockable(view : View, position : String) extends JPanel {
- {
- val panel = new XHTMLPanel(new UserAgent())
- setLayout(new BorderLayout)
+ val panel = new XHTMLPanel(new UserAgent())
+ setLayout(new BorderLayout)
+
+ //Copy-paste-support
+ private val cp = new SelectionActions
+ cp.install(panel)
- //Copy-paste-support
- val cp = new SelectionActions
- cp.install(panel)
+ add(new JScrollPane(panel), BorderLayout.CENTER)
- add(new JScrollPane(panel), BorderLayout.CENTER)
-
- val fontResolver =
- panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
+ private val fontResolver =
+ panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
+ if (Plugin.plugin.viewFont != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+ Plugin.plugin.viewFontChanged.add(font => {
if (Plugin.plugin.viewFont != null)
fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
- Plugin.plugin.viewFontChanged.add(font => {
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
-
- panel.relayout()
- })
-
- Plugin.plugin.stateUpdate.add(state => {
- if (state == null)
- panel.setDocument(null : Document)
- else
- panel.setDocument(state.results_xml, UserAgent.baseURL)
- })
- }
+ panel.relayout()
+ })
+
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Dec 18 01:10:20 2008 +0100
@@ -18,7 +18,6 @@
import org.gjt.sp.jedit.syntax.SyntaxStyle
object TheoryView {
- val ISABELLE_THEORY_PROPERTY = "de.tum.in.isabelle.jedit.Theory";
def chooseColor(state : Command) : Color = {
if (state == null)
@@ -58,65 +57,44 @@
case _ => Color.white
}
}
-
- def withView(view : JEditTextArea, f : (TheoryView) => Unit) {
- if (view != null && view.getBuffer() != null)
- view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match {
- case null => null
- case view: TheoryView => f(view)
- case _ => null
- }
- }
-
- def activateTextArea(textArea : JEditTextArea) {
- withView(textArea, _.activate(textArea))
- }
-
- def deactivateTextArea(textArea : JEditTextArea) {
- withView(textArea, _.deactivate(textArea))
- }
}
-class TheoryView(prover : Prover, val buffer : JEditBuffer)
+class TheoryView (text_area : JEditTextArea)
extends TextAreaExtension with Text with BufferListener {
import TheoryView._
import Text.Changed
-
- var textArea : JEditTextArea = null;
- var col : Changed = null;
+
+ var col : Changed = null
+
+ val buffer = text_area.getBuffer
+ buffer.addBufferListener(this)
val colTimer = new Timer(300, new ActionListener() {
override def actionPerformed(e : ActionEvent) { commit() }
})
val changesSource = new EventSource[Changed]
-
- {
- buffer.addBufferListener(this)
- buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
+ val phase_overview = new PhaseOverviewPanel(Plugin.prover(buffer))
val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
- prover.commandInfo.add(_ => repaint_delay.delay_or_ignore())
- // could also use this:
- // prover.commandInfo.add(c => repaint(c.command))
+ Plugin.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
Plugin.plugin.viewFontChanged.add(font => updateFont())
-
+
colTimer.stop
colTimer.setRepeats(true)
- }
- def activate(area : JEditTextArea) {
- textArea = area
- textArea.addCaretListener(selectedStateController)
- textArea.addLeftOfScrollBar(new PhaseOverviewPanel(textArea))
- val painter = textArea.getPainter()
+ def activate() {
+ text_area.addCaretListener(selectedStateController)
+ phase_overview.textarea = text_area
+ text_area.addLeftOfScrollBar(phase_overview)
+ val painter = text_area.getPainter()
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
updateFont()
}
private def updateFont() {
- if (textArea != null) {
- val painter = textArea.getPainter()
+ if (text_area != null) {
+ val painter = text_area.getPainter()
if (Plugin.plugin.viewFont != null) {
painter.setStyles(painter.getStyles().map(style =>
new SyntaxStyle(style.getForegroundColor,
@@ -129,18 +107,18 @@
}
}
- def deactivate(area : JEditTextArea) {
- textArea.getPainter().removeExtension(this)
- textArea.removeCaretListener(selectedStateController)
- textArea = null
+ def deactivate() {
+ text_area.getPainter().removeExtension(this)
+ text_area.removeCaretListener(selectedStateController)
+ text_area.removeLeftOfScrollBar(phase_overview)
}
val selectedStateController = new CaretListener() {
override def caretUpdate(e : CaretEvent) {
- val cmd = prover.document.getNextCommandContaining(e.getDot())
+ val cmd = Plugin.prover(buffer).document.getNextCommandContaining(e.getDot())
if (cmd != null && cmd.start <= e.getDot() &&
- Plugin.plugin.selectedState != cmd)
- Plugin.plugin.selectedState = cmd
+ Plugin.prover_setup(buffer).selectedState != cmd)
+ Plugin.prover_setup(buffer).selectedState = cmd
}
}
@@ -159,28 +137,28 @@
def repaint(cmd : Command)
{
val ph = cmd.phase
- if (textArea != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
- var start = textArea.getLineOfOffset(toCurrent(cmd.start))
- var stop = textArea.getLineOfOffset(toCurrent(cmd.stop) - 1)
- textArea.invalidateLineRange(start, stop)
+ if (text_area != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
+ var start = text_area.getLineOfOffset(toCurrent(cmd.start))
+ var stop = text_area.getLineOfOffset(toCurrent(cmd.stop) - 1)
+ text_area.invalidateLineRange(start, stop)
- if (Plugin.plugin.selectedState == cmd)
- Plugin.plugin.selectedState = cmd // update State view
+ if (Plugin.prover_setup(buffer).selectedState == cmd)
+ Plugin.prover_setup(buffer).selectedState = cmd // update State view
}
}
def repaintAll()
{
- if (textArea != null)
- textArea.invalidateLineRange(textArea.getFirstPhysicalLine,
- textArea.getLastPhysicalLine)
+ if (text_area != null)
+ text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
+ text_area.getLastPhysicalLine)
}
def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){
- val fm = textArea.getPainter.getFontMetrics
- val startP = textArea.offsetToXY(begin)
- val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish)
- else { var p = textArea.offsetToXY(finish - 1)
+ val fm = text_area.getPainter.getFontMetrics
+ val startP = text_area.offsetToXY(begin)
+ val stopP = if (finish < buffer.getLength()) text_area.offsetToXY(finish)
+ else { var p = text_area.offsetToXY(finish - 1)
p.x = p.x + fm.charWidth(' ')
p }
@@ -194,9 +172,9 @@
override def paintValidLine(gfx : Graphics2D, screenLine : Int,
pl : Int, start : Int, end : Int, y : Int)
{
- val fm = textArea.getPainter.getFontMetrics
+ val fm = text_area.getPainter.getFontMetrics
var savedColor = gfx.getColor
- var e = prover.document.getNextCommandContaining(fromCurrent(start))
+ var e = Plugin.prover(buffer).document.getNextCommandContaining(fromCurrent(start))
//Encolor Phase
while (e != null && toCurrent(e.start) < end) {
@@ -217,7 +195,7 @@
}
def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
- def length = buffer.getLength()
+ override def length = buffer.getLength
def changes = changesSource
--- a/src/Tools/jEdit/src/prover/IsabelleSKParser.scala Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/prover/IsabelleSKParser.scala Thu Dec 18 01:10:20 2008 +0100
@@ -7,35 +7,31 @@
package isabelle.prover
-import isabelle.jedit.Plugin
+import isabelle.jedit.{Plugin}
import sidekick.{SideKickParser, SideKickParsedData, IAsset}
-import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.{Buffer, ServiceManager}
import javax.swing.tree.DefaultMutableTreeNode
import errorlist.DefaultErrorSource;
-class IsabelleSKParser() extends SideKickParser("isabelle") {
+class IsabelleSKParser extends SideKickParser("isabelle") {
override def parse(b : Buffer,
errorSource : DefaultErrorSource)
: SideKickParsedData = {
- if(Plugin.plugin == null || Plugin.plugin.theoryView == null
- || Plugin.plugin.theoryView.buffer == null
- || !Plugin.plugin.theoryView.buffer.equals(b))
- {
- val data = new SideKickParsedData("WARNING:")
- data.root.add(new DefaultMutableTreeNode("can only parse buffer which is activated via IsabellePlugin -> activate"))
- data
- } else{
- val plugin = Plugin.plugin
- val prover = plugin.prover
- val buffer = Plugin.plugin.theoryView.buffer.asInstanceOf[Buffer]
- val document = prover.document
- val data = new SideKickParsedData(buffer.getPath)
+ Plugin.plugin.prover_setup(b) match {
+ case None =>
+ val data = new SideKickParsedData("WARNING:")
+ data.root.add(new DefaultMutableTreeNode("can only parse buffer which is activated via IsabellePlugin -> activate"))
+ data
+ case Some(prover_setup) =>
+ val prover = prover_setup.prover
+ val document = prover.document
+ val data = new SideKickParsedData(b.getPath)
- for(command <- document.commands){
- data.root.add(command.root_node.swing_node)
- }
- data
+ for(command <- document.commands){
+ data.root.add(command.root_node.swing_node)
+ }
+ data
}
}