# HG changeset patch # User immler@in.tum.de # Date 1229559020 -3600 # Node ID f81cd75ae3312dc2942b6101e8ea0db7a03453d2 # Parent a67a4eaebcff5c2121e8068fc7f889e838b40ea6 restructured: independent provers in different buffers diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/plugin/actions.xml --- 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 @@


-			isabelle.jedit.Plugin$.MODULE$.plugin().activate(view);
+			isabelle.jedit.Plugin$.MODULE$.plugin().install(view);

- return view.getBuffer().getMode().getName() == "isabelle"; + return isabelle.jedit.Plugin$.MODULE$.plugin().is_active(view.getBuffer()); \ No newline at end of file diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/plugin/services.xml --- 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 @@ - + new isabelle.prover.IsabelleSKParser(); diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/OutputDockable.scala --- 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"))) } diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- 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 = diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/Plugin.scala --- 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) diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/ProverSetup.scala --- /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! + } + +} diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/ScrollerDockable.scala --- 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 diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/StateViewDockable.scala --- 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() + }) + } diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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 diff -r a67a4eaebcff -r f81cd75ae331 src/Tools/jEdit/src/prover/IsabelleSKParser.scala --- 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 } }