--- a/src/Tools/jEdit/dist-template/properties/jedit.props Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Tue Dec 08 16:30:20 2009 +0100
@@ -170,9 +170,9 @@
encodingDetectors=BOM XML-PI buffer-local-property
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
-isabelle-browser.dock-position=bottom
-isabelle-output.dock-position=bottom
-isabelle-state.dock-position=bottom
+isabelle-history.dock-position=bottom
+isabelle-raw-output.dock-position=bottom
+isabelle-results.dock-position=bottom
isabelle.activate.shortcut=CS+ENTER
mode.isabelle.sidekick.showStatusWindow.label=true
sidekick-tree.dock-position=right
--- a/src/Tools/jEdit/plugin/Isabelle.props Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Tue Dec 08 16:30:20 2009 +0100
@@ -6,12 +6,11 @@
plugin.isabelle.jedit.Plugin.name=Isabelle
plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
plugin.isabelle.jedit.Plugin.version=0.0.1
-plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
+plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing
#system parameters
plugin.isabelle.jedit.Plugin.activate=defer
plugin.isabelle.jedit.Plugin.usePluginHome=false
-plugin.isabelle.jedit.Plugin.jars=
#dependencies
plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
@@ -23,23 +22,23 @@
#options
plugin.isabelle.jedit.Plugin.option-pane=isabelle
options.isabelle.label=Isabelle
-options.isabelle.code=new isabelle.jedit.OptionPane();
+options.isabelle.code=new isabelle.jedit.Isabelle_Options();
options.isabelle.logic.title=Logic
options.isabelle.font-size.title=Font Size
options.isabelle.font-size=14
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-state isabelle.show-output isabelle.show-browser
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-results isabelle.show-raw-output isabelle.show-history
isabelle.activate.label=Activate current buffer
-isabelle.show-state.label=Show State
-isabelle.show-output.label=Show Output
-isabelle.show-browser.label=Show Version-Browser
+isabelle.show-results.label=Show Results
+isabelle.show-raw-output.label=Show Raw Output
+isabelle.show-history.label=Show History
#dockables
-isabelle-output.title=Isabelle Output
-isabelle-state.title=Isabelle State
-isabelle-browser.title=Isabelle Browse-Version
+isabelle-results.title=Results
+isabelle-raw-output.title=Raw Output
+isabelle-history.title=History
#SideKick
sidekick.parser.isabelle.label=Isabelle
--- a/src/Tools/jEdit/plugin/actions.xml Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml Tue Dec 08 16:30:20 2009 +0100
@@ -1,19 +1,7 @@
+<?xml version="1.0"?>
+<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
+
<ACTIONS>
- <ACTION NAME="isabelle.show-output">
- <CODE>
- wm.addDockableWindow("isabelle-output");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.show-state">
- <CODE>
- wm.addDockableWindow("isabelle-state");
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.show-browser">
- <CODE>
- wm.addDockableWindow("isabelle-browser");
- </CODE>
- </ACTION>
<ACTION NAME="isabelle.activate">
<CODE>
isabelle.jedit.Isabelle.plugin().switch_active(view);
@@ -22,4 +10,19 @@
return isabelle.jedit.Isabelle.plugin().is_active(view.getBuffer());
</IS_SELECTED>
</ACTION>
+ <ACTION NAME="isabelle.show-results">
+ <CODE>
+ wm.addDockableWindow("isabelle-results");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.show-raw-output">
+ <CODE>
+ wm.addDockableWindow("isabelle-raw-output");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.show-history">
+ <CODE>
+ wm.addDockableWindow("isabelle-history");
+ </CODE>
+ </ACTION>
</ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/dockables.xml Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml Tue Dec 08 16:30:20 2009 +0100
@@ -1,15 +1,14 @@
<?xml version="1.0"?>
-
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
- <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
- new isabelle.jedit.OutputDockable(view, position);
+ <DOCKABLE NAME="isabelle-results" MOVABLE="TRUE">
+ new isabelle.jedit.Results_Dockable(view, position).peer();
</DOCKABLE>
- <DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
- new isabelle.jedit.StateViewDockable(view, position);
+ <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+ new isabelle.jedit.Raw_Output_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-browser" MOVABLE="TRUE">
- new isabelle.jedit.BrowseVersionDockable(view, position).peer();
+ <DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
+ new isabelle.jedit.History_Dockable(view, position).peer();
</DOCKABLE>
</DOCKABLES>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/services.xml Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/services.xml Tue Dec 08 16:30:20 2009 +0100
@@ -1,13 +1,14 @@
<?xml version="1.0"?>
<!DOCTYPE SERVICES SYSTEM "services.dtd">
+
<SERVICES>
<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
new isabelle.jedit.Isabelle_Encoding();
</SERVICE>
<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.IsabelleSideKickParser();
+ new isabelle.jedit.Isabelle_Sidekick();
</SERVICE>
<SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
- new isabelle.jedit.IsabelleHyperlinkSource();
+ new isabelle.jedit.Isabelle_Hyperlinks();
</SERVICE>
</SERVICES>
--- a/src/Tools/jEdit/src/jedit/browse_version_dockable.scala Tue Dec 08 14:49:01 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-/*
- * Dockable window for navigating through the document-versions
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-import isabelle.proofdocument.Change
-
-import java.awt.Dimension
-import scala.swing.{ListView, FlowPanel}
-import scala.swing.event.ListSelectionChanged
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
-
-class BrowseVersionDockable(view: View, position: String) extends FlowPanel
-{
- if (position == DockableWindowManager.FLOATING)
- preferredSize = new Dimension(500, 250)
-
- def prover_setup(): Option[ProverSetup] = Isabelle.prover_setup(view.getBuffer)
- def get_versions() =
- prover_setup() match {
- case None => Nil
- case Some(setup) => setup.theory_view.changes
- }
-
- val list = new ListView[Change]
- list.fixedCellWidth = 500
- list.listData = get_versions()
- contents += list
-
- listenTo(list.selection)
- reactions += {
- case ListSelectionChanged(source, range, false) =>
- prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
- }
-
- prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
-}
--- a/src/Tools/jEdit/src/jedit/document_overview.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_overview.scala Tue Dec 08 16:30:20 2009 +0100
@@ -6,8 +6,8 @@
package isabelle.jedit
-import isabelle.prover.{Prover, Command}
-import isabelle.proofdocument.ProofDocument
+
+import isabelle.proofdocument.{Command, Proof_Document, Prover, Theory_View}
import javax.swing.{JPanel, ToolTipManager}
import java.awt.event.{MouseAdapter, MouseEvent}
@@ -21,7 +21,7 @@
class Document_Overview(
prover: Prover,
text_area: JEditTextArea,
- to_current: (ProofDocument, Int) => Int)
+ to_current: (Proof_Document, Int) => Int)
extends JPanel(new BorderLayout)
{
private val WIDTH = 10
@@ -67,7 +67,7 @@
val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
val y = line_to_y(line1)
val height = HEIGHT * (line2 - line1)
- gfx.setColor(TheoryView.choose_color(command, doc))
+ gfx.setColor(Theory_View.choose_color(command, doc))
gfx.fillRect(0, y, getWidth - 1, height)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/history_dockable.scala Tue Dec 08 16:30:20 2009 +0100
@@ -0,0 +1,44 @@
+/*
+ * Dockable window for navigating through the document history
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.Change
+
+import java.awt.Dimension
+import scala.swing.{ListView, FlowPanel}
+import scala.swing.event.ListSelectionChanged
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class History_Dockable(view: View, position: String) extends FlowPanel
+{
+ if (position == DockableWindowManager.FLOATING)
+ preferredSize = new Dimension(500, 250)
+
+ def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
+ def get_versions() =
+ prover_setup() match {
+ case None => Nil
+ case Some(setup) => setup.theory_view.changes
+ }
+
+ val list = new ListView[Change]
+ list.fixedCellWidth = 500
+ list.listData = get_versions()
+ contents += list
+
+ listenTo(list.selection)
+ reactions += {
+ case ListSelectionChanged(source, range, false) =>
+ prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
+ }
+
+ prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
+}
--- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Tue Dec 08 16:30:20 2009 +0100
@@ -6,6 +6,7 @@
package isabelle.jedit
+
import org.gjt.sp.jedit.io.Encoding
import org.gjt.sp.jedit.buffer.JEditBuffer
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 08 16:30:20 2009 +0100
@@ -6,6 +6,7 @@
package isabelle.jedit
+
import java.io.File
import gatchan.jedit.hyperlinks.Hyperlink
@@ -17,10 +18,10 @@
import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.TextUtilities
-import isabelle.prover.Command
+import isabelle.proofdocument.Command
-class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
+private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
extends AbstractHyperlink(start, end, line, "")
{
override def click(view: View) {
@@ -28,21 +29,22 @@
}
}
-class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
+class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
extends AbstractHyperlink(start, end, line, "")
{
override def click(view: View) = {
Isabelle.system.source_file(ref_file) match {
- case None => System.err.println("Could not find source file " + ref_file)
+ case None => System.err.println("Could not find source file " + ref_file) // FIXME ??
case Some(file) =>
jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
}
}
}
-class IsabelleHyperlinkSource extends HyperlinkSource
+class Isabelle_Hyperlinks extends HyperlinkSource
{
- def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
+ def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
+ {
val prover = Isabelle.prover_setup(buffer).map(_.prover)
val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
if (prover.isEmpty || theory_view_opt.isEmpty) null
@@ -61,11 +63,11 @@
val end = theory_view.to_current(document, command_start + ref.stop)
ref.info match {
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
- new ExternalHyperlink(begin, end, line, ref_file, ref_line)
+ new External_Hyperlink(begin, end, line, ref_file, ref_line)
case Command.RefInfo(_, _, Some(id), Some(offset)) =>
prover.get.command(id) match {
case Some(ref_cmd) =>
- new InternalHyperlink(begin, end, line,
+ new Internal_Hyperlink(begin, end, line,
theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
case None => null
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue Dec 08 16:30:20 2009 +0100
@@ -0,0 +1,44 @@
+/*
+ * Editor pane for plugin options
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import javax.swing.{JComboBox, JSpinner}
+
+import org.gjt.sp.jedit.AbstractOptionPane
+
+
+class Isabelle_Options extends AbstractOptionPane("isabelle")
+{
+ private val logic_name = new JComboBox()
+ private val font_size = new JSpinner()
+
+ override def _init()
+ {
+ addComponent(Isabelle.Property("logic.title"), {
+ for (name <- Isabelle.system.find_logics()) {
+ logic_name.addItem(name)
+ if (name == Isabelle.Property("logic"))
+ logic_name.setSelectedItem(name)
+ }
+ logic_name
+ })
+ addComponent(Isabelle.Property("font-size.title"), {
+ font_size.setValue(Isabelle.Int_Property("font-size"))
+ font_size
+ })
+ }
+
+ override def _save()
+ {
+ val logic = logic_name.getSelectedItem.asInstanceOf[String]
+ Isabelle.Property("logic") = logic
+
+ val size = font_size.getValue().asInstanceOf[Int]
+ Isabelle.Int_Property("font-size") = size
+ }
+}
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 08 16:30:20 2009 +0100
@@ -7,6 +7,7 @@
package isabelle.jedit
+
import scala.collection.Set
import scala.collection.immutable.TreeSet
@@ -18,11 +19,10 @@
import errorlist.DefaultErrorSource
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
-import isabelle.prover.{Command, Markup_Node}
-import isabelle.proofdocument.ProofDocument
+import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
-class IsabelleSideKickParser extends SideKickParser("isabelle")
+class Isabelle_Sidekick extends SideKickParser("isabelle")
{
/* parsing */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Dec 08 16:30:20 2009 +0100
@@ -0,0 +1,153 @@
+/*
+ * include isabelle's command- and keyword-declarations
+ * live in jEdits syntax-highlighting
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.Prover
+import isabelle.Markup
+
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.syntax.{Token => JToken,
+ TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
+
+import java.awt.Color
+import java.awt.Font
+import javax.swing.text.Segment;
+
+
+object Isabelle_Token_Marker
+{
+ /* line context */
+
+ private val rule_set = new ParserRuleSet("isabelle", "MAIN")
+ private class LineContext(val line: Int, prev: LineContext)
+ extends TokenMarker.LineContext(rule_set, prev)
+
+
+ /* mapping to jEdit token types */
+ // TODO: as properties or CSS style sheet
+
+ private val choose_byte: Map[String, Byte] =
+ {
+ import JToken._
+ Map[String, Byte](
+ // logical entities
+ Markup.TCLASS -> LABEL,
+ Markup.TYCON -> LABEL,
+ Markup.FIXED_DECL -> LABEL,
+ Markup.FIXED -> LABEL,
+ Markup.CONST_DECL -> LABEL,
+ Markup.CONST -> LABEL,
+ Markup.FACT_DECL -> LABEL,
+ Markup.FACT -> LABEL,
+ Markup.DYNAMIC_FACT -> LABEL,
+ Markup.LOCAL_FACT_DECL -> LABEL,
+ Markup.LOCAL_FACT -> LABEL,
+ // inner syntax
+ Markup.TFREE -> LITERAL2,
+ Markup.FREE -> LITERAL2,
+ Markup.TVAR -> LITERAL3,
+ Markup.SKOLEM -> LITERAL3,
+ Markup.BOUND -> LITERAL3,
+ Markup.VAR -> LITERAL3,
+ Markup.NUM -> DIGIT,
+ Markup.FLOAT -> DIGIT,
+ Markup.XNUM -> DIGIT,
+ Markup.XSTR -> LITERAL4,
+ Markup.LITERAL -> LITERAL4,
+ Markup.INNER_COMMENT -> COMMENT1,
+ Markup.SORT -> FUNCTION,
+ Markup.TYP -> FUNCTION,
+ Markup.TERM -> FUNCTION,
+ Markup.PROP -> FUNCTION,
+ Markup.ATTRIBUTE -> FUNCTION,
+ Markup.METHOD -> FUNCTION,
+ // ML syntax
+ Markup.ML_KEYWORD -> KEYWORD2,
+ Markup.ML_IDENT -> NULL,
+ Markup.ML_TVAR -> LITERAL3,
+ Markup.ML_NUMERAL -> DIGIT,
+ Markup.ML_CHAR -> LITERAL1,
+ Markup.ML_STRING -> LITERAL1,
+ Markup.ML_COMMENT -> COMMENT1,
+ Markup.ML_MALFORMED -> INVALID,
+ // embedded source text
+ Markup.ML_SOURCE -> COMMENT4,
+ Markup.DOC_SOURCE -> COMMENT4,
+ Markup.ANTIQ -> COMMENT4,
+ Markup.ML_ANTIQ -> COMMENT4,
+ Markup.DOC_ANTIQ -> COMMENT4,
+ // outer syntax
+ Markup.IDENT -> NULL,
+ Markup.COMMAND -> OPERATOR,
+ Markup.KEYWORD -> KEYWORD4,
+ Markup.VERBATIM -> COMMENT3,
+ Markup.COMMENT -> COMMENT1,
+ Markup.CONTROL -> COMMENT3,
+ Markup.MALFORMED -> INVALID,
+ Markup.STRING -> LITERAL3,
+ Markup.ALTSTRING -> LITERAL1
+ ).withDefaultValue(NULL)
+ }
+
+ def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
+ styles(choose_byte(kind)).getForegroundColor
+}
+
+
+class Isabelle_Token_Marker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
+{
+ override def markTokens(prev: TokenMarker.LineContext,
+ handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
+ {
+ val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
+ val line = if (prev == null) 0 else previous.line + 1
+ val context = new Isabelle_Token_Marker.LineContext(line, previous)
+ val start = buffer.getLineStartOffset(line)
+ val stop = start + line_segment.count
+
+ val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+ val document = theory_view.current_document()
+ def to: Int => Int = theory_view.to_current(document, _)
+ def from: Int => Int = theory_view.from_current(document, _)
+
+ var next_x = start
+ var cmd = document.command_at(from(start))
+ while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
+ val command = cmd.get
+ for {
+ markup <- command.highlight(document).flatten
+ command_start = command.start(document)
+ abs_start = to(command_start + markup.start)
+ abs_stop = to(command_start + markup.stop)
+ if (abs_stop > start)
+ if (abs_start < stop)
+ byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
+ token_start = (abs_start - start) max 0
+ token_length =
+ (abs_stop - abs_start) -
+ ((start - abs_start) max 0) -
+ ((abs_stop - stop) max 0)
+ } {
+ if (start + token_start > next_x)
+ handler.handleToken(line_segment, 1,
+ next_x - start, start + token_start - next_x, context)
+ handler.handleToken(line_segment, byte,
+ token_start, token_length, context)
+ next_x = start + token_start + token_length
+ }
+ cmd = document.commands.next(command)
+ }
+ if (next_x < stop)
+ handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+
+ handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
+ handler.setLineContext(context)
+ return context
+ }
+}
--- a/src/Tools/jEdit/src/jedit/option_pane.scala Tue Dec 08 14:49:01 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-/*
- * Editor pane for plugin options
- *
- * @author Johannes Hölzl, TU Munich
- */
-
-package isabelle.jedit
-
-import javax.swing.{JComboBox, JSpinner}
-
-import org.gjt.sp.jedit.AbstractOptionPane
-
-
-class OptionPane extends AbstractOptionPane("isabelle")
-{
- private val logic_name = new JComboBox()
- private val font_size = new JSpinner()
-
- override def _init()
- {
- addComponent(Isabelle.Property("logic.title"), {
- for (name <- Isabelle.system.find_logics()) {
- logic_name.addItem(name)
- if (name == Isabelle.Property("logic"))
- logic_name.setSelectedItem(name)
- }
- logic_name
- })
- addComponent(Isabelle.Property("font-size.title"), {
- font_size.setValue(Isabelle.Int_Property("font-size"))
- font_size
- })
- }
-
- override def _save()
- {
- val logic = logic_name.getSelectedItem.asInstanceOf[String]
- Isabelle.Property("logic") = logic
-
- val size = font_size.getValue().asInstanceOf[Int]
- Isabelle.Int_Property("font-size") = size
- }
-}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 08 16:30:20 2009 +0100
@@ -3,6 +3,7 @@
*
* @author Johannes Hölzl, TU Munich
* @author Fabian Immler, TU Munich
+ * @author Makarius
*/
package isabelle.jedit
@@ -14,8 +15,7 @@
import scala.collection.mutable
-import isabelle.prover.{Prover, Command}
-import isabelle.proofdocument.ProofDocument
+import isabelle.proofdocument.{Command, Proof_Document, Prover}
import isabelle.Isabelle_System
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
@@ -98,12 +98,12 @@
/* mapping buffer <-> prover */
- private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
+ private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup]
private def install(view: View)
{
val buffer = view.getBuffer
- val prover_setup = new ProverSetup(buffer)
+ val prover_setup = new Prover_Setup(buffer)
mapping.update(buffer, prover_setup)
prover_setup.activate(view)
}
@@ -115,7 +115,7 @@
if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
else install(view)
- def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
+ def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer)
def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
--- a/src/Tools/jEdit/src/jedit/prover_setup.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/prover_setup.scala Tue Dec 08 16:30:20 2009 +0100
@@ -9,18 +9,18 @@
import org.gjt.sp.jedit.{Buffer, View}
-import isabelle.prover.Prover
+import isabelle.proofdocument.{Prover, Theory_View}
-class ProverSetup(buffer: Buffer)
+class Prover_Setup(buffer: Buffer)
{
var prover: Prover = null
- var theory_view: TheoryView = null
+ var theory_view: Theory_View = null
def activate(view: View)
{
- // TheoryView starts prover
- theory_view = new TheoryView(view.getTextArea)
+ // Theory_View starts prover
+ theory_view = new Theory_View(view.getTextArea)
prover = theory_view.prover
theory_view.activate()
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Tue Dec 08 16:30:20 2009 +0100
@@ -15,8 +15,8 @@
import org.gjt.sp.jedit.gui.DockableWindowManager
-class OutputDockable(view : View, position : String) extends JPanel {
-
+class Raw_Output_Dockable(view: View, position: String) extends JPanel
+{
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
--- a/src/Tools/jEdit/src/jedit/results_dockable.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/results_dockable.scala Tue Dec 08 16:30:20 2009 +0100
@@ -7,13 +7,14 @@
package isabelle.jedit
+
import isabelle.XML
+import scala.swing.{BorderPanel, Component}
+
import java.io.StringReader
import java.awt.{BorderLayout, Dimension}
-
import javax.swing.{JButton, JPanel, JScrollPane}
-
import java.util.logging.{Logger, Level}
import org.lobobrowser.html.parser._
@@ -31,12 +32,12 @@
import scala.io.Source
-class StateViewDockable(view : View, position : String) extends JPanel {
-
+class Results_Dockable(view : View, position : String) extends BorderPanel
+{
// outer panel
+
if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(500, 250))
- setLayout(new BorderLayout)
+ preferredSize = new Dimension(500, 250)
// global logging
@@ -87,7 +88,8 @@
doc.appendChild(empty_body)
panel.setDocument(doc, rcontext)
- add(panel, BorderLayout.CENTER)
+
+ add(Component.wrap(panel), BorderPanel.Position.Center)
// register for state-view
--- a/src/Tools/jEdit/src/jedit/token_marker.scala Tue Dec 08 14:49:01 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-/*
- * include isabelle's command- and keyword-declarations
- * live in jEdits syntax-highlighting
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-
-import isabelle.prover.Prover
-import isabelle.Markup
-
-import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.syntax.{Token => JToken,
- TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
-
-import java.awt.Color
-import java.awt.Font
-import javax.swing.text.Segment;
-
-
-object DynamicTokenMarker
-{
- /* line context */
-
- private val rule_set = new ParserRuleSet("isabelle", "MAIN")
- private class LineContext(val line: Int, prev: LineContext)
- extends TokenMarker.LineContext(rule_set, prev)
-
-
- /* mapping to jEdit token types */
- // TODO: as properties or CSS style sheet
-
- private val choose_byte: Map[String, Byte] =
- {
- import JToken._
- Map[String, Byte](
- // logical entities
- Markup.TCLASS -> LABEL,
- Markup.TYCON -> LABEL,
- Markup.FIXED_DECL -> LABEL,
- Markup.FIXED -> LABEL,
- Markup.CONST_DECL -> LABEL,
- Markup.CONST -> LABEL,
- Markup.FACT_DECL -> LABEL,
- Markup.FACT -> LABEL,
- Markup.DYNAMIC_FACT -> LABEL,
- Markup.LOCAL_FACT_DECL -> LABEL,
- Markup.LOCAL_FACT -> LABEL,
- // inner syntax
- Markup.TFREE -> LITERAL2,
- Markup.FREE -> LITERAL2,
- Markup.TVAR -> LITERAL3,
- Markup.SKOLEM -> LITERAL3,
- Markup.BOUND -> LITERAL3,
- Markup.VAR -> LITERAL3,
- Markup.NUM -> DIGIT,
- Markup.FLOAT -> DIGIT,
- Markup.XNUM -> DIGIT,
- Markup.XSTR -> LITERAL4,
- Markup.LITERAL -> LITERAL4,
- Markup.INNER_COMMENT -> COMMENT1,
- Markup.SORT -> FUNCTION,
- Markup.TYP -> FUNCTION,
- Markup.TERM -> FUNCTION,
- Markup.PROP -> FUNCTION,
- Markup.ATTRIBUTE -> FUNCTION,
- Markup.METHOD -> FUNCTION,
- // ML syntax
- Markup.ML_KEYWORD -> KEYWORD2,
- Markup.ML_IDENT -> NULL,
- Markup.ML_TVAR -> LITERAL3,
- Markup.ML_NUMERAL -> DIGIT,
- Markup.ML_CHAR -> LITERAL1,
- Markup.ML_STRING -> LITERAL1,
- Markup.ML_COMMENT -> COMMENT1,
- Markup.ML_MALFORMED -> INVALID,
- // embedded source text
- Markup.ML_SOURCE -> COMMENT4,
- Markup.DOC_SOURCE -> COMMENT4,
- Markup.ANTIQ -> COMMENT4,
- Markup.ML_ANTIQ -> COMMENT4,
- Markup.DOC_ANTIQ -> COMMENT4,
- // outer syntax
- Markup.IDENT -> NULL,
- Markup.COMMAND -> OPERATOR,
- Markup.KEYWORD -> KEYWORD4,
- Markup.VERBATIM -> COMMENT3,
- Markup.COMMENT -> COMMENT1,
- Markup.CONTROL -> COMMENT3,
- Markup.MALFORMED -> INVALID,
- Markup.STRING -> LITERAL3,
- Markup.ALTSTRING -> LITERAL1
- ).withDefaultValue(NULL)
- }
-
- def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
- styles(choose_byte(kind)).getForegroundColor
-}
-
-
-class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
- extends TokenMarker
-{
- override def markTokens(prev: TokenMarker.LineContext,
- handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
- {
- val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
- val line = if (prev == null) 0 else previous.line + 1
- val context = new DynamicTokenMarker.LineContext(line, previous)
- val start = buffer.getLineStartOffset(line)
- val stop = start + line_segment.count
-
- val theory_view = Isabelle.prover_setup(buffer).get.theory_view
- val document = theory_view.current_document()
- def to: Int => Int = theory_view.to_current(document, _)
- def from: Int => Int = theory_view.from_current(document, _)
-
- var next_x = start
- var cmd = document.command_at(from(start))
- while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
- val command = cmd.get
- for {
- markup <- command.highlight(document).flatten
- command_start = command.start(document)
- abs_start = to(command_start + markup.start)
- abs_stop = to(command_start + markup.stop)
- if (abs_stop > start)
- if (abs_start < stop)
- byte = DynamicTokenMarker.choose_byte(markup.info.toString)
- token_start = (abs_start - start) max 0
- token_length =
- (abs_stop - abs_start) -
- ((start - abs_start) max 0) -
- ((abs_stop - stop) max 0)
- } {
- if (start + token_start > next_x)
- handler.handleToken(line_segment, 1,
- next_x - start, start + token_start - next_x, context)
- handler.handleToken(line_segment, byte,
- token_start, token_length, context)
- next_x = start + token_start + token_length
- }
- cmd = document.commands.next(command)
- }
- if (next_x < stop)
- handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
-
- handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
- handler.setLineContext(context)
- return context
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/command.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Tue Dec 08 16:30:20 2009 +0100
@@ -5,14 +5,13 @@
* @author Fabian Immler, TU Munich
*/
-package isabelle.prover
+package isabelle.proofdocument
import scala.actors.Actor, Actor._
import scala.collection.mutable
-import isabelle.proofdocument.{Token, ProofDocument}
import isabelle.jedit.{Isabelle, Plugin}
import isabelle.XML
@@ -70,8 +69,8 @@
def content(i: Int, j: Int): String = content.substring(i, j)
val symbol_index = new Symbol.Index(content)
- def start(doc: ProofDocument) = doc.token_start(tokens.first)
- def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
+ def start(doc: Proof_Document) = doc.token_start(tokens.first)
+ def stop(doc: Proof_Document) = doc.token_start(tokens.last) + tokens.last.length
def contains(p: Token) = tokens.contains(p)
@@ -93,15 +92,15 @@
/* results, markup, ... */
private val empty_cmd_state = new Command_State(this)
- private def cmd_state(doc: ProofDocument) =
+ private def cmd_state(doc: Proof_Document) =
doc.states.getOrElse(this, empty_cmd_state)
- def status(doc: ProofDocument) = cmd_state(doc).state.status
- def results(doc: ProofDocument) = cmd_state(doc).results
- def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
- def highlight(doc: ProofDocument) = cmd_state(doc).highlight
- def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
- def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
+ def status(doc: Proof_Document) = cmd_state(doc).state.status
+ def results(doc: Proof_Document) = cmd_state(doc).results
+ def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
+ def highlight(doc: Proof_Document) = cmd_state(doc).highlight
+ def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
+ def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
}
--- a/src/Tools/jEdit/src/proofdocument/markup_node.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala Tue Dec 08 16:30:20 2009 +0100
@@ -2,14 +2,14 @@
* Document markup nodes, with connection to Swing tree model
*
* @author Fabian Immler, TU Munich
+ * @author Makarius
*/
-package isabelle.prover
+package isabelle.proofdocument
import javax.swing.tree.DefaultMutableTreeNode
-import isabelle.proofdocument.ProofDocument
class Markup_Node(val start: Int, val stop: Int, val info: Any)
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 08 16:30:20 2009 +0100
@@ -8,14 +8,13 @@
package isabelle.proofdocument
+
import scala.actors.Actor, Actor._
import java.util.regex.Pattern
-import isabelle.prover.{Prover, Command, Command_State}
-
-object ProofDocument
+object Proof_Document
{
// Be careful when changing this regex. Not only must it handle the
// spurious end of a token but also:
@@ -34,14 +33,14 @@
"[()\\[\\]{}:;]", Pattern.MULTILINE)
val empty =
- new ProofDocument(isabelle.jedit.Isabelle.system.id(),
+ new Proof_Document(isabelle.jedit.Isabelle.system.id(),
Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
type StructureChange = List[(Option[Command], Option[Command])]
}
-class ProofDocument(
+class Proof_Document(
val id: String,
val tokens: Linear_Set[Token],
val token_start: Map[Token, Int],
@@ -49,10 +48,10 @@
var states: Map[Command, Command_State], // FIXME immutable
is_command_keyword: String => Boolean)
{
- import ProofDocument.StructureChange
+ import Proof_Document.StructureChange
- def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(id, tokens, token_start, commands, states, f)
+ def set_command_keyword(f: String => Boolean): Proof_Document =
+ new Proof_Document(id, tokens, token_start, commands, states, f)
def content = Token.string_from_tokens(Nil ++ tokens, token_start)
@@ -60,9 +59,9 @@
/** token view **/
- def text_changed(change: Change): (ProofDocument, StructureChange) =
+ def text_changed(change: Change): (Proof_Document, StructureChange) =
{
- def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
+ def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = {
val (doc, chgs) = doc_chgs
val (new_doc, chg) = doc.text_edit(edit, change.id)
(new_doc, chgs ++ chg)
@@ -70,7 +69,7 @@
((this, Nil: StructureChange) /: change.edits)(edit_doc)
}
- def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
+ def text_edit(e: Edit, id: String): (Proof_Document, StructureChange) =
{
case class TextChange(start: Int, added: String, removed: String)
val change = e match {
@@ -116,7 +115,7 @@
val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
val matcher =
- ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
+ Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
while (matcher.find() && invalid_tokens != Nil) {
val kind =
@@ -158,7 +157,7 @@
after_change: Option[Token],
new_tokens: List[Token],
new_token_start: Map[Token, Int]):
- (ProofDocument, StructureChange) =
+ (Proof_Document, StructureChange) =
{
val new_tokenset = Linear_Set[Token]() ++ new_tokens
val cmd_before_change = before_change match {
@@ -236,7 +235,7 @@
val doc =
- new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
+ new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset,
states -- removed_commands, is_command_keyword)
val removes =
--- a/src/Tools/jEdit/src/proofdocument/prover.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/prover.scala Tue Dec 08 16:30:20 2009 +0100
@@ -6,7 +6,7 @@
* @author Makarius
*/
-package isabelle.prover
+package isabelle.proofdocument
import scala.actors.Actor, Actor._
@@ -14,7 +14,6 @@
import javax.swing.JTextArea
import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{ProofDocument, Change, Token}
class Prover(system: Isabelle_System, logic: String)
@@ -41,7 +40,7 @@
/* outgoing messages */
val command_change = new Event_Bus[Command]
- val document_change = new Event_Bus[ProofDocument]
+ val document_change = new Event_Bus[Proof_Document]
/* prover process */
@@ -67,12 +66,12 @@
@volatile private var states = Map[Isar_Document.State_ID, Command_State]()
@volatile private var commands = Map[Isar_Document.Command_ID, Command]()
val document_0 =
- ProofDocument.empty.
+ Proof_Document.empty.
set_command_keyword((s: String) => command_decls().contains(s))
@volatile private var document_versions = List(document_0)
def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
- def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
+ def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
document_versions.find(_.id == id)
--- a/src/Tools/jEdit/src/proofdocument/state.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/state.scala Tue Dec 08 16:30:20 2009 +0100
@@ -5,7 +5,7 @@
* @author Makarius
*/
-package isabelle.prover
+package isabelle.proofdocument
class State(
--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 08 16:30:20 2009 +0100
@@ -6,14 +6,12 @@
* @author Makarius
*/
-package isabelle.jedit
+package isabelle.proofdocument
+
import scala.actors.Actor, Actor._
import scala.collection.mutable
-import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
-import isabelle.prover.{Prover, Command}
-
import java.awt.{Color, Graphics2D}
import javax.swing.event.{CaretListener, CaretEvent}
@@ -21,10 +19,12 @@
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
+import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker, Raw_Output_Dockable}
-object TheoryView
+
+object Theory_View
{
- def choose_color(command: Command, doc: ProofDocument): Color =
+ def choose_color(command: Command, doc: Proof_Document): Color =
{
command.status(doc) match {
case Command.Status.UNPROCESSED => new Color(255, 228, 225)
@@ -36,7 +36,7 @@
}
-class TheoryView(text_area: JEditTextArea)
+class Theory_View(text_area: JEditTextArea)
{
private val buffer = text_area.getBuffer
@@ -115,8 +115,8 @@
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
val document = current_document()
- def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
- def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
+ def from_current(pos: Int) = Theory_View.this.from_current(document, pos)
+ def to_current(pos: Int) = Theory_View.this.to_current(document, pos)
val saved_color = gfx.getColor
val metrics = text_area.getPainter.getFontMetrics
@@ -128,7 +128,7 @@
val begin = start max to_current(e.start(document))
val finish = (end - 1) min to_current(e.stop(document))
encolor(gfx, y, metrics.getHeight, begin, finish,
- TheoryView.choose_color(e, document), true)
+ Theory_View.choose_color(e, document), true)
cmd = document.commands.next(e)
}
@@ -166,18 +166,19 @@
}
}
- def activate() {
+ def activate()
+ {
text_area.addCaretListener(selected_state_controller)
text_area.addLeftOfScrollBar(overview)
text_area.getPainter.
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
- buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
+ buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
buffer.addBufferListener(buffer_listener)
val dockable =
- text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
+ text_area.getView.getDockableWindowManager.getDockable("isabelle-raw-output")
if (dockable != null) {
- val output_dockable = dockable.asInstanceOf[OutputDockable]
+ val output_dockable = dockable.asInstanceOf[Raw_Output_Dockable]
val output_text_view = prover.output_text_view
output_dockable.set_text(output_text_view)
}
@@ -196,7 +197,7 @@
/* history of changes */
- private def doc_or_pred(c: Change): ProofDocument =
+ private def doc_or_pred(c: Change): Proof_Document =
prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
def current_document() = doc_or_pred(current_change)
@@ -254,14 +255,14 @@
/* transforming offsets */
- private def changes_from(doc: ProofDocument): List[Edit] =
+ private def changes_from(doc: Proof_Document): List[Edit] =
List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
edits.toList
- def from_current(doc: ProofDocument, offset: Int): Int =
+ def from_current(doc: Proof_Document, offset: Int): Int =
(offset /: changes_from(doc).reverse) ((i, change) => change before i)
- def to_current(doc: ProofDocument, offset: Int): Int =
+ def to_current(doc: Proof_Document, offset: Int): Int =
(offset /: changes_from(doc)) ((i, change) => change after i)
--- a/src/Tools/jEdit/src/proofdocument/token.scala Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/token.scala Tue Dec 08 16:30:20 2009 +0100
@@ -8,9 +8,6 @@
package isabelle.proofdocument
-import isabelle.prover.Command
-
-
object Token {
object Kind extends Enumeration
{