# HG changeset patch
# User wenzelm
# Date 1260280141 -3600
# Node ID bfea7839d9e14bf9633775b7fe867ef856432303
# Parent 710e3a9a4c9548983db3d2d591181276983b6424
misc rearrangement of files;
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala
--- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Tue Dec 08 14:29:29 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()))
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/Document_Overview.scala
--- a/src/Tools/jEdit/src/jedit/Document_Overview.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-/*
- * Information on command status left of scrollbar (with panel)
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-import isabelle.prover.{Prover, Command}
-import isabelle.proofdocument.ProofDocument
-
-import javax.swing.{JPanel, ToolTipManager}
-import java.awt.event.{MouseAdapter, MouseEvent}
-import java.awt.{BorderLayout, Graphics, Dimension}
-
-import org.gjt.sp.jedit.gui.RolloverButton
-import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.buffer.JEditBuffer
-
-
-class Document_Overview(
- prover: Prover,
- text_area: JEditTextArea,
- to_current: (ProofDocument, Int) => Int)
- extends JPanel(new BorderLayout)
-{
- private val WIDTH = 10
- private val HEIGHT = 2
-
- setRequestFocusEnabled(false)
-
- addMouseListener(new MouseAdapter {
- override def mousePressed(event: MouseEvent) {
- val line = y_to_line(event.getY)
- if (line >= 0 && line < text_area.getLineCount)
- text_area.setCaretPosition(text_area.getLineStartOffset(line))
- }
- })
-
- override def addNotify() {
- super.addNotify()
- ToolTipManager.sharedInstance.registerComponent(this)
- }
-
- override def removeNotify() {
- super.removeNotify
- ToolTipManager.sharedInstance.unregisterComponent(this)
- }
-
- override def getToolTipText(event: MouseEvent): String =
- {
- val buffer = text_area.getBuffer
- val lineCount = buffer.getLineCount
- val line = y_to_line(event.getY())
- if (line >= 0 && line < text_area.getLineCount) "TODO:
Tooltip"
- else ""
- }
-
- override def paintComponent(gfx: Graphics) {
- super.paintComponent(gfx)
- val buffer = text_area.getBuffer
- val theory_view = Isabelle.prover_setup(buffer).get.theory_view
- val doc = theory_view.current_document()
-
- for (command <- doc.commands) {
- val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
- 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.fillRect(0, y, getWidth - 1, height)
- }
- }
-
- override def getPreferredSize = new Dimension(WIDTH, 0)
-
- private def line_to_y(line: Int): Int =
- (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
-
- private def y_to_line(y: Int): Int =
- (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
-}
\ No newline at end of file
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Dec 08 14:29:29 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
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-/*
- * Hyperlink setup for Isabelle proof documents
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-import java.io.File
-
-import gatchan.jedit.hyperlinks.Hyperlink
-import gatchan.jedit.hyperlinks.HyperlinkSource
-import gatchan.jedit.hyperlinks.AbstractHyperlink
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.jEdit
-import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.TextUtilities
-
-import isabelle.prover.Command
-
-
-class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
- extends AbstractHyperlink(start, end, line, "")
-{
- override def click(view: View) {
- view.getTextArea.moveCaretPosition(ref_offset)
- }
-}
-
-class ExternalHyperlink(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 Some(file) =>
- jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
- }
- }
-}
-
-class IsabelleHyperlinkSource extends HyperlinkSource
-{
- 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
- else if (prover.get == null || theory_view_opt.get == null) null
- else {
- val theory_view = theory_view_opt.get
- val document = theory_view.current_document()
- val offset = theory_view.from_current(document, original_offset)
- document.command_at(offset) match {
- case Some(command) =>
- command.ref_at(document, offset - command.start(document)) match {
- case Some(ref) =>
- val command_start = command.start(document)
- val begin = theory_view.to_current(document, command_start + ref.start)
- val line = buffer.getLineOfOffset(begin)
- 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)
- case Command.RefInfo(_, _, Some(id), Some(offset)) =>
- prover.get.command(id) match {
- case Some(ref_cmd) =>
- new InternalHyperlink(begin, end, line,
- theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
- case None => null
- }
- case _ => null
- }
- case None => null
- }
- case None => null
- }
- }
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-/*
- * SideKick parser for Isabelle proof documents
- *
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.jedit
-
-import scala.collection.Set
-import scala.collection.immutable.TreeSet
-
-import javax.swing.tree.DefaultMutableTreeNode
-import javax.swing.text.Position
-import javax.swing.Icon
-
-import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
-import errorlist.DefaultErrorSource
-import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
-
-import isabelle.prover.{Command, Markup_Node}
-import isabelle.proofdocument.ProofDocument
-
-
-class IsabelleSideKickParser extends SideKickParser("isabelle")
-{
- /* parsing */
-
- @volatile private var stopped = false
- override def stop() = { stopped = true }
-
- def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
- {
- implicit def int_to_pos(offset: Int): Position =
- new Position { def getOffset = offset; override def toString = offset.toString }
-
- stopped = false
-
- val data = new SideKickParsedData(buffer.getName)
- val root = data.root
- data.getAsset(root).setEnd(buffer.getLength)
-
- val prover_setup = Isabelle.prover_setup(buffer)
- if (prover_setup.isDefined) {
- val document = prover_setup.get.theory_view.current_document()
- for (command <- document.commands if !stopped) {
- root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
- {
- val content = command.content(node.start, node.stop)
- val command_start = command.start(document)
- val id = command.id
-
- new DefaultMutableTreeNode(new IAsset {
- override def getIcon: Icon = null
- override def getShortString: String = content
- override def getLongString: String = node.info.toString
- override def getName: String = id
- override def setName(name: String) = ()
- override def setStart(start: Position) = ()
- override def getStart: Position = command_start + node.start
- override def setEnd(end: Position) = ()
- override def getEnd: Position = command_start + node.stop
- override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
- })
- }))
- }
- if (stopped) root.add(new DefaultMutableTreeNode(""))
- }
- else root.add(new DefaultMutableTreeNode(""))
-
- data
- }
-
-
- /* completion */
-
- override def supportsCompletion = true
- override def canCompleteAnywhere = true
-
- override def complete(pane: EditPane, caret: Int): SideKickCompletion =
- {
- val buffer = pane.getBuffer
-
- val line = buffer.getLineOfOffset(caret)
- val start = buffer.getLineStartOffset(line)
- val text = buffer.getSegment(start, caret - start)
-
- val completion =
- Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
-
- completion.complete(text) match {
- case None => null
- case Some((word, cs)) =>
- val ds =
- if (Isabelle_Encoding.is_active(buffer))
- cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
- else cs
- new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
- }
- }
-
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/Isabelle_Encoding.scala
--- a/src/Tools/jEdit/src/jedit/Isabelle_Encoding.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-/*
- * Isabelle encoding -- based on utf-8
- *
- * @author Makarius
- */
-
-package isabelle.jedit
-
-import org.gjt.sp.jedit.io.Encoding
-import org.gjt.sp.jedit.buffer.JEditBuffer
-
-import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
-import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
- CharArrayReader, ByteArrayOutputStream}
-
-import scala.io.{Source, BufferedSource}
-
-
-object Isabelle_Encoding
-{
- val NAME = "UTF-8-Isabelle"
-
- def is_active(buffer: JEditBuffer): Boolean =
- buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
-}
-
-class Isabelle_Encoding extends Encoding
-{
- private val charset = Charset.forName(Isabelle_System.charset)
- private val BUFSIZE = 32768
-
- private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
- {
- def source(): Source =
- BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
- new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
- }
-
- override def getTextReader(in: InputStream): Reader =
- text_reader(in, charset.newDecoder())
-
- override def getPermissiveTextReader(in: InputStream): Reader =
- {
- val decoder = charset.newDecoder()
- decoder.onMalformedInput(CodingErrorAction.REPLACE)
- decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, decoder)
- }
-
- override def getTextWriter(out: OutputStream): Writer =
- {
- val buffer = new ByteArrayOutputStream(BUFSIZE) {
- override def flush()
- {
- val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
- out.write(text.getBytes(Isabelle_System.charset))
- out.flush()
- }
- override def close() { out.close() }
- }
- new OutputStreamWriter(buffer, charset.newEncoder())
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala Tue Dec 08 14:29:29 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
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/OutputDockable.scala
--- a/src/Tools/jEdit/src/jedit/OutputDockable.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/*
- * Dockable window for raw process output
- *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
- */
-
-package isabelle.jedit
-
-
-import java.awt.{Dimension, Graphics, GridLayout}
-import javax.swing.{JPanel, JTextArea, JScrollPane}
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
-
-class OutputDockable(view : View, position : String) extends JPanel {
-
- if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(500, 250))
-
- setLayout(new GridLayout(1, 1))
- add(new JScrollPane(new JTextArea))
-
- def set_text(output_text_view: JTextArea) {
- removeAll()
- add(new JScrollPane(output_text_view))
- revalidate()
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,155 +0,0 @@
-/*
- * Main Isabelle/jEdit plugin setup
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-
-import java.io.{FileInputStream, IOException}
-import java.awt.Font
-import javax.swing.JScrollPane
-
-import scala.collection.mutable
-
-import isabelle.prover.{Prover, Command}
-import isabelle.proofdocument.ProofDocument
-import isabelle.Isabelle_System
-
-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 Isabelle
-{
- /* name */
-
- val NAME = "Isabelle"
-
-
- /* properties */
-
- val OPTION_PREFIX = "options.isabelle."
-
- object Property
- {
- def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
- def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
- }
-
- object Boolean_Property
- {
- def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
- def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
- }
-
- object Int_Property
- {
- def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
- def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
- }
-
-
- /* Isabelle system instance */
-
- var system: Isabelle_System = null
- def symbols = system.symbols
- lazy val completion = new Completion + symbols
-
-
- /* settings */
-
- def default_logic(): String =
- {
- val logic = Isabelle.Property("logic")
- if (logic != null) logic
- else system.getenv_strict("ISABELLE_LOGIC")
- }
-
-
- /* plugin instance */
-
- var plugin: Plugin = null
-
-
- /* running provers */
-
- def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
-}
-
-
-class Plugin extends EBPlugin
-{
- /* event buses */
-
- val state_update = new Event_Bus[Command]
-
-
- /* selected state */
-
- private var _selected_state: Command = null
- def selected_state = _selected_state
- def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
-
-
- /* mapping buffer <-> prover */
-
- private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
-
- private def install(view: View)
- {
- val buffer = view.getBuffer
- val prover_setup = new ProverSetup(buffer)
- mapping.update(buffer, prover_setup)
- prover_setup.activate(view)
- }
-
- private def uninstall(view: View) =
- mapping.removeKey(view.getBuffer).get.deactivate
-
- def switch_active (view: View) =
- if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
- else install(view)
-
- def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
- def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
-
-
- /* main plugin plumbing */
-
- override def handleMessage(msg: EBMessage)
- {
- msg match {
- case epu: EditPaneUpdate =>
- val buffer = epu.getEditPane.getBuffer
- epu.getWhat match {
- case EditPaneUpdate.BUFFER_CHANGED =>
- (mapping get buffer) map (_.theory_view.activate)
- case EditPaneUpdate.BUFFER_CHANGING =>
- if (buffer != null)
- (mapping get buffer) map (_.theory_view.deactivate)
- case _ =>
- }
- case _ =>
- }
- }
-
- override def start()
- {
- Isabelle.plugin = this
- Isabelle.system = new Isabelle_System
- if (!Isabelle.system.register_fonts())
- System.err.println("Failed to register Isabelle fonts")
- }
-
- override def stop()
- {
- // TODO: proper cleanup
- Isabelle.system = null
- Isabelle.plugin = null
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/*
- * Independent prover sessions for each buffer
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-
-import org.gjt.sp.jedit.{Buffer, View}
-
-import isabelle.prover.Prover
-
-
-class ProverSetup(buffer: Buffer)
-{
- var prover: Prover = null
- var theory_view: TheoryView = null
-
- def activate(view: View)
- {
- // TheoryView starts prover
- theory_view = new TheoryView(view.getTextArea)
- prover = theory_view.prover
-
- theory_view.activate()
- prover.begin_document(buffer.getName)
- }
-
- def deactivate()
- {
- theory_view.deactivate
- prover.stop
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-/*
- * Dockable window with rendered state output
- *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
- */
-
-package isabelle.jedit
-
-import isabelle.XML
-
-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._
-import org.lobobrowser.html.test._
-import org.lobobrowser.html.gui._
-import org.lobobrowser.html._
-import org.lobobrowser.html.style.CSSUtilities
-import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
-
-import org.gjt.sp.jedit.jEdit
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-import org.gjt.sp.jedit.textarea.AntiAlias
-
-import scala.io.Source
-
-
-class StateViewDockable(view : View, position : String) extends JPanel {
-
- // outer panel
- if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(500, 250))
- setLayout(new BorderLayout)
-
-
- // global logging
-
- Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
-
-
- // document template with styles
-
- private def try_file(name: String): String =
- {
- val file = Isabelle.system.platform_file(name)
- if (file.exists) Source.fromFile(file).mkString else ""
- }
-
-
- // HTML panel
-
- val panel = new HtmlPanel
- val ucontext = new SimpleUserAgentContext
- val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
- val doc = {
- val builder = new DocumentBuilderImpl(ucontext, rcontext)
- builder.parse(new InputSourceImpl(new StringReader(
- """
-
-
-
-
-
-
-""")))
- }
-
- val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
- doc.appendChild(empty_body)
-
- panel.setDocument(doc, rcontext)
- add(panel, BorderLayout.CENTER)
-
-
- // register for state-view
- Isabelle.plugin.state_update += (cmd => {
- val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
-
- Swing_Thread.later {
- val node =
- if (cmd == null) empty_body
- else {
- val xml = XML.elem(HTML.BODY,
- cmd.results(theory_view.current_document).
- map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
- XML.document_node(doc, xml)
- }
- doc.removeChild(doc.getLastChild())
- doc.appendChild(node)
- panel.delayedRelayout(node.asInstanceOf[NodeImpl])
- }
- })
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,327 +0,0 @@
-/*
- * jEdit text area as document text source
- *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
- * @author Makarius
- */
-
-package isabelle.jedit
-
-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}
-
-import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
-
-
-object TheoryView
-{
- def choose_color(command: Command, doc: ProofDocument): Color =
- {
- command.status(doc) match {
- case Command.Status.UNPROCESSED => new Color(255, 228, 225)
- case Command.Status.FINISHED => new Color(234, 248, 255)
- case Command.Status.FAILED => new Color(255, 106, 106)
- case _ => Color.red
- }
- }
-}
-
-
-class TheoryView(text_area: JEditTextArea)
-{
- private val buffer = text_area.getBuffer
-
-
- /* prover setup */
-
- val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
-
- prover.command_change += ((command: Command) =>
- if (current_document().commands.contains(command))
- Swing_Thread.later {
- // FIXME proper handling of buffer vs. text areas
- // repaint if buffer is active
- if (text_area.getBuffer == buffer) {
- update_syntax(command)
- invalidate_line(command)
- overview.repaint()
- }
- })
-
-
- /* changes vs. edits */
-
- private val change_0 = new Change(prover.document_0.id, None, Nil)
- private var _changes = List(change_0) // owned by Swing/AWT thread
- def changes = _changes
- private var current_change = change_0
-
- private val edits = new mutable.ListBuffer[Edit] // owned by Swing thread
-
- private val edits_delay = Swing_Thread.delay_last(300) {
- if (!edits.isEmpty) {
- val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
- _changes ::= change
- prover.input(change)
- current_change = change
- edits.clear
- }
- }
-
-
- /* buffer_listener */
-
- private val buffer_listener = new BufferListener {
- override def preContentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int)
- {
- edits += Insert(offset, buffer.getText(offset, length))
- edits_delay()
- }
-
- override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed_length: Int)
- {
- edits += Remove(start, buffer.getText(start, removed_length))
- edits_delay()
- }
-
- override def contentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
- override def contentRemoved(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
- override def bufferLoaded(buffer: JEditBuffer) { }
- override def foldHandlerChanged(buffer: JEditBuffer) { }
- override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
- override def transactionComplete(buffer: JEditBuffer) { }
- }
-
-
- /* text_area_extension */
-
- private val text_area_extension = new TextAreaExtension {
- override def paintValidLine(gfx: Graphics2D,
- 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)
- val saved_color = gfx.getColor
-
- val metrics = text_area.getPainter.getFontMetrics
-
- // encolor phase
- var cmd = document.command_at(from_current(start))
- while (cmd.isDefined && cmd.get.start(document) < end) {
- val e = cmd.get
- 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)
- cmd = document.commands.next(e)
- }
-
- gfx.setColor(saved_color)
- }
-
- override def getToolTipText(x: Int, y: Int): String =
- {
- val document = current_document()
- val offset = from_current(document, text_area.xyToOffset(x, y))
- document.command_at(offset) match {
- case Some(cmd) =>
- document.token_start(cmd.tokens.first)
- cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
- case None => null
- }
- }
- }
-
-
- /* activation */
-
- private val overview = new Document_Overview(prover, text_area, to_current)
-
- private val selected_state_controller = new CaretListener {
- override def caretUpdate(e: CaretEvent) {
- val doc = current_document()
- doc.command_at(e.getDot) match {
- case Some(cmd)
- if (doc.token_start(cmd.tokens.first) <= e.getDot &&
- Isabelle.plugin.selected_state != cmd) =>
- Isabelle.plugin.selected_state = cmd
- case _ =>
- }
- }
- }
-
- 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.addBufferListener(buffer_listener)
-
- val dockable =
- text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
- if (dockable != null) {
- val output_dockable = dockable.asInstanceOf[OutputDockable]
- val output_text_view = prover.output_text_view
- output_dockable.set_text(output_text_view)
- }
-
- buffer.propertiesChanged()
- }
-
- def deactivate() {
- buffer.setTokenMarker(buffer.getMode.getTokenMarker)
- buffer.removeBufferListener(buffer_listener)
- text_area.getPainter.removeExtension(text_area_extension)
- text_area.removeLeftOfScrollBar(overview)
- text_area.removeCaretListener(selected_state_controller)
- }
-
-
- /* history of changes */
-
- private def doc_or_pred(c: Change): ProofDocument =
- prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
-
- def current_document() = doc_or_pred(current_change)
-
-
- /* update to desired version */
-
- def set_version(goal: Change) {
- // changes in buffer must be ignored
- buffer.removeBufferListener(buffer_listener)
-
- def apply(change: Change): Unit = change.edits.foreach {
- case Insert(start, text) => buffer.insert(start, text)
- case Remove(start, text) => buffer.remove(start, text.length)
- }
-
- def unapply(change: Change): Unit = change.edits.reverse.foreach {
- case Insert(start, text) => buffer.remove(start, text.length)
- case Remove(start, text) => buffer.insert(start, text)
- }
-
- // undo/redo changes
- val ancs_current = current_change.ancestors
- val ancs_goal = goal.ancestors
- val paired = ancs_current.reverse zip ancs_goal.reverse
- def last_common[A](xs: List[(A, A)]): Option[A] = {
- xs match {
- case (x, y) :: xs =>
- if (x == y)
- xs match {
- case (a, b) :: ys =>
- if (a == b) last_common(xs)
- else Some(x)
- case _ => Some(x)
- }
- else None
- case _ => None
- }
- }
- val common_anc = last_common(paired).get
-
- ancs_current.takeWhile(_ != common_anc) map unapply
- ancs_goal.takeWhile(_ != common_anc).reverse map apply
-
- current_change = goal
- // invoke repaint
- buffer.propertiesChanged()
- invalidate_all()
- overview.repaint()
-
- // track changes in buffer
- buffer.addBufferListener(buffer_listener)
- }
-
-
- /* transforming offsets */
-
- private def changes_from(doc: ProofDocument): List[Edit] =
- List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
- edits.toList
-
- def from_current(doc: ProofDocument, offset: Int): Int =
- (offset /: changes_from(doc).reverse) ((i, change) => change before i)
-
- def to_current(doc: ProofDocument, offset: Int): Int =
- (offset /: changes_from(doc)) ((i, change) => change after i)
-
-
- private def lines_of_command(cmd: Command) =
- {
- val document = current_document()
- (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
- buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
- }
-
-
- /* (re)painting */
-
- private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
-
- private def update_syntax(cmd: Command) {
- val (line1, line2) = lines_of_command(cmd)
- if (line2 >= text_area.getFirstLine &&
- line1 <= text_area.getFirstLine + text_area.getVisibleLines)
- update_delay()
- }
-
- private def invalidate_line(cmd: Command) =
- {
- val (start, stop) = lines_of_command(cmd)
- text_area.invalidateLineRange(start, stop)
-
- if (Isabelle.plugin.selected_state == cmd)
- Isabelle.plugin.selected_state = cmd // update State view
- }
-
- private def invalidate_all() =
- text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
- text_area.getLastPhysicalLine)
-
- private def encolor(gfx: Graphics2D,
- y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
- {
- val start = text_area.offsetToXY(begin)
- val stop =
- if (finish < buffer.getLength) text_area.offsetToXY(finish)
- else {
- val p = text_area.offsetToXY(finish - 1)
- val metrics = text_area.getPainter.getFontMetrics
- p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
- p
- }
-
- if (start != null && stop != null) {
- gfx.setColor(color)
- if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
- else gfx.drawRect(start.x, y, stop.x - start.x, height)
- }
- }
-
-
- /* init */
-
- prover.start()
-
- edits += Insert(0, buffer.getText(0, buffer.getLength))
- edits_delay()
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/browse_version_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/browse_version_dockable.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,43 @@
+/*
+ * 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()))
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/document_overview.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_overview.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,82 @@
+/*
+ * Information on command status left of scrollbar (with panel)
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+import isabelle.prover.{Prover, Command}
+import isabelle.proofdocument.ProofDocument
+
+import javax.swing.{JPanel, ToolTipManager}
+import java.awt.event.{MouseAdapter, MouseEvent}
+import java.awt.{BorderLayout, Graphics, Dimension}
+
+import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.buffer.JEditBuffer
+
+
+class Document_Overview(
+ prover: Prover,
+ text_area: JEditTextArea,
+ to_current: (ProofDocument, Int) => Int)
+ extends JPanel(new BorderLayout)
+{
+ private val WIDTH = 10
+ private val HEIGHT = 2
+
+ setRequestFocusEnabled(false)
+
+ addMouseListener(new MouseAdapter {
+ override def mousePressed(event: MouseEvent) {
+ val line = y_to_line(event.getY)
+ if (line >= 0 && line < text_area.getLineCount)
+ text_area.setCaretPosition(text_area.getLineStartOffset(line))
+ }
+ })
+
+ override def addNotify() {
+ super.addNotify()
+ ToolTipManager.sharedInstance.registerComponent(this)
+ }
+
+ override def removeNotify() {
+ super.removeNotify
+ ToolTipManager.sharedInstance.unregisterComponent(this)
+ }
+
+ override def getToolTipText(event: MouseEvent): String =
+ {
+ val buffer = text_area.getBuffer
+ val lineCount = buffer.getLineCount
+ val line = y_to_line(event.getY())
+ if (line >= 0 && line < text_area.getLineCount) "TODO:
Tooltip"
+ else ""
+ }
+
+ override def paintComponent(gfx: Graphics) {
+ super.paintComponent(gfx)
+ val buffer = text_area.getBuffer
+ val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+ val doc = theory_view.current_document()
+
+ for (command <- doc.commands) {
+ val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
+ 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.fillRect(0, y, getWidth - 1, height)
+ }
+ }
+
+ override def getPreferredSize = new Dimension(WIDTH, 0)
+
+ private def line_to_y(line: Int): Int =
+ (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
+
+ private def y_to_line(y: Int): Int =
+ (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
+}
\ No newline at end of file
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/isabelle_encoding.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,63 @@
+/*
+ * Isabelle encoding -- based on utf-8
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+import org.gjt.sp.jedit.io.Encoding
+import org.gjt.sp.jedit.buffer.JEditBuffer
+
+import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
+import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
+ CharArrayReader, ByteArrayOutputStream}
+
+import scala.io.{Source, BufferedSource}
+
+
+object Isabelle_Encoding
+{
+ val NAME = "UTF-8-Isabelle"
+
+ def is_active(buffer: JEditBuffer): Boolean =
+ buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
+}
+
+class Isabelle_Encoding extends Encoding
+{
+ private val charset = Charset.forName(Isabelle_System.charset)
+ private val BUFSIZE = 32768
+
+ private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
+ {
+ def source(): Source =
+ BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
+ new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
+ }
+
+ override def getTextReader(in: InputStream): Reader =
+ text_reader(in, charset.newDecoder())
+
+ override def getPermissiveTextReader(in: InputStream): Reader =
+ {
+ val decoder = charset.newDecoder()
+ decoder.onMalformedInput(CodingErrorAction.REPLACE)
+ decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, decoder)
+ }
+
+ override def getTextWriter(out: OutputStream): Writer =
+ {
+ val buffer = new ByteArrayOutputStream(BUFSIZE) {
+ override def flush()
+ {
+ val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
+ out.write(text.getBytes(Isabelle_System.charset))
+ out.flush()
+ }
+ override def close() { out.close() }
+ }
+ new OutputStreamWriter(buffer, charset.newEncoder())
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,80 @@
+/*
+ * Hyperlink setup for Isabelle proof documents
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+import java.io.File
+
+import gatchan.jedit.hyperlinks.Hyperlink
+import gatchan.jedit.hyperlinks.HyperlinkSource
+import gatchan.jedit.hyperlinks.AbstractHyperlink
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.jEdit
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.TextUtilities
+
+import isabelle.prover.Command
+
+
+class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
+ extends AbstractHyperlink(start, end, line, "")
+{
+ override def click(view: View) {
+ view.getTextArea.moveCaretPosition(ref_offset)
+ }
+}
+
+class ExternalHyperlink(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 Some(file) =>
+ jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
+ }
+ }
+}
+
+class IsabelleHyperlinkSource extends HyperlinkSource
+{
+ 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
+ else if (prover.get == null || theory_view_opt.get == null) null
+ else {
+ val theory_view = theory_view_opt.get
+ val document = theory_view.current_document()
+ val offset = theory_view.from_current(document, original_offset)
+ document.command_at(offset) match {
+ case Some(command) =>
+ command.ref_at(document, offset - command.start(document)) match {
+ case Some(ref) =>
+ val command_start = command.start(document)
+ val begin = theory_view.to_current(document, command_start + ref.start)
+ val line = buffer.getLineOfOffset(begin)
+ 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)
+ case Command.RefInfo(_, _, Some(id), Some(offset)) =>
+ prover.get.command(id) match {
+ case Some(ref_cmd) =>
+ new InternalHyperlink(begin, end, line,
+ theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+ case None => null
+ }
+ case _ => null
+ }
+ case None => null
+ }
+ case None => null
+ }
+ }
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,102 @@
+/*
+ * SideKick parser for Isabelle proof documents
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+import scala.collection.Set
+import scala.collection.immutable.TreeSet
+
+import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.text.Position
+import javax.swing.Icon
+
+import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
+import errorlist.DefaultErrorSource
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
+
+import isabelle.prover.{Command, Markup_Node}
+import isabelle.proofdocument.ProofDocument
+
+
+class IsabelleSideKickParser extends SideKickParser("isabelle")
+{
+ /* parsing */
+
+ @volatile private var stopped = false
+ override def stop() = { stopped = true }
+
+ def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
+ {
+ implicit def int_to_pos(offset: Int): Position =
+ new Position { def getOffset = offset; override def toString = offset.toString }
+
+ stopped = false
+
+ val data = new SideKickParsedData(buffer.getName)
+ val root = data.root
+ data.getAsset(root).setEnd(buffer.getLength)
+
+ val prover_setup = Isabelle.prover_setup(buffer)
+ if (prover_setup.isDefined) {
+ val document = prover_setup.get.theory_view.current_document()
+ for (command <- document.commands if !stopped) {
+ root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
+ {
+ val content = command.content(node.start, node.stop)
+ val command_start = command.start(document)
+ val id = command.id
+
+ new DefaultMutableTreeNode(new IAsset {
+ override def getIcon: Icon = null
+ override def getShortString: String = content
+ override def getLongString: String = node.info.toString
+ override def getName: String = id
+ override def setName(name: String) = ()
+ override def setStart(start: Position) = ()
+ override def getStart: Position = command_start + node.start
+ override def setEnd(end: Position) = ()
+ override def getEnd: Position = command_start + node.stop
+ override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
+ })
+ }))
+ }
+ if (stopped) root.add(new DefaultMutableTreeNode(""))
+ }
+ else root.add(new DefaultMutableTreeNode(""))
+
+ data
+ }
+
+
+ /* completion */
+
+ override def supportsCompletion = true
+ override def canCompleteAnywhere = true
+
+ override def complete(pane: EditPane, caret: Int): SideKickCompletion =
+ {
+ val buffer = pane.getBuffer
+
+ val line = buffer.getLineOfOffset(caret)
+ val start = buffer.getLineStartOffset(line)
+ val text = buffer.getSegment(start, caret - start)
+
+ val completion =
+ Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
+
+ completion.complete(text) match {
+ case None => null
+ case Some((word, cs)) =>
+ val ds =
+ if (Isabelle_Encoding.is_active(buffer))
+ cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
+ else cs
+ new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
+ }
+ }
+
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/option_pane.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/option_pane.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,43 @@
+/*
+ * 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
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/plugin.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,155 @@
+/*
+ * Main Isabelle/jEdit plugin setup
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import java.io.{FileInputStream, IOException}
+import java.awt.Font
+import javax.swing.JScrollPane
+
+import scala.collection.mutable
+
+import isabelle.prover.{Prover, Command}
+import isabelle.proofdocument.ProofDocument
+import isabelle.Isabelle_System
+
+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 Isabelle
+{
+ /* name */
+
+ val NAME = "Isabelle"
+
+
+ /* properties */
+
+ val OPTION_PREFIX = "options.isabelle."
+
+ object Property
+ {
+ def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
+ def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
+ }
+
+ object Boolean_Property
+ {
+ def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
+ def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
+ }
+
+ object Int_Property
+ {
+ def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
+ def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
+ }
+
+
+ /* Isabelle system instance */
+
+ var system: Isabelle_System = null
+ def symbols = system.symbols
+ lazy val completion = new Completion + symbols
+
+
+ /* settings */
+
+ def default_logic(): String =
+ {
+ val logic = Isabelle.Property("logic")
+ if (logic != null) logic
+ else system.getenv_strict("ISABELLE_LOGIC")
+ }
+
+
+ /* plugin instance */
+
+ var plugin: Plugin = null
+
+
+ /* running provers */
+
+ def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
+}
+
+
+class Plugin extends EBPlugin
+{
+ /* event buses */
+
+ val state_update = new Event_Bus[Command]
+
+
+ /* selected state */
+
+ private var _selected_state: Command = null
+ def selected_state = _selected_state
+ def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
+
+
+ /* mapping buffer <-> prover */
+
+ private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
+
+ private def install(view: View)
+ {
+ val buffer = view.getBuffer
+ val prover_setup = new ProverSetup(buffer)
+ mapping.update(buffer, prover_setup)
+ prover_setup.activate(view)
+ }
+
+ private def uninstall(view: View) =
+ mapping.removeKey(view.getBuffer).get.deactivate
+
+ def switch_active (view: View) =
+ if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
+ else install(view)
+
+ def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
+ def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
+
+
+ /* main plugin plumbing */
+
+ override def handleMessage(msg: EBMessage)
+ {
+ msg match {
+ case epu: EditPaneUpdate =>
+ val buffer = epu.getEditPane.getBuffer
+ epu.getWhat match {
+ case EditPaneUpdate.BUFFER_CHANGED =>
+ (mapping get buffer) map (_.theory_view.activate)
+ case EditPaneUpdate.BUFFER_CHANGING =>
+ if (buffer != null)
+ (mapping get buffer) map (_.theory_view.deactivate)
+ case _ =>
+ }
+ case _ =>
+ }
+ }
+
+ override def start()
+ {
+ Isabelle.plugin = this
+ Isabelle.system = new Isabelle_System
+ if (!Isabelle.system.register_fonts())
+ System.err.println("Failed to register Isabelle fonts")
+ }
+
+ override def stop()
+ {
+ // TODO: proper cleanup
+ Isabelle.system = null
+ Isabelle.plugin = null
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/prover_setup.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/prover_setup.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,35 @@
+/*
+ * Independent prover sessions for each buffer
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import org.gjt.sp.jedit.{Buffer, View}
+
+import isabelle.prover.Prover
+
+
+class ProverSetup(buffer: Buffer)
+{
+ var prover: Prover = null
+ var theory_view: TheoryView = null
+
+ def activate(view: View)
+ {
+ // TheoryView starts prover
+ theory_view = new TheoryView(view.getTextArea)
+ prover = theory_view.prover
+
+ theory_view.activate()
+ prover.begin_document(buffer.getName)
+ }
+
+ def deactivate()
+ {
+ theory_view.deactivate
+ prover.stop
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/raw_output_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,31 @@
+/*
+ * Dockable window for raw process output
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import java.awt.{Dimension, Graphics, GridLayout}
+import javax.swing.{JPanel, JTextArea, JScrollPane}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class OutputDockable(view : View, position : String) extends JPanel {
+
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
+ setLayout(new GridLayout(1, 1))
+ add(new JScrollPane(new JTextArea))
+
+ def set_text(output_text_view: JTextArea) {
+ removeAll()
+ add(new JScrollPane(output_text_view))
+ revalidate()
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/results_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/results_dockable.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,111 @@
+/*
+ * Dockable window with rendered state output
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.jedit
+
+import isabelle.XML
+
+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._
+import org.lobobrowser.html.test._
+import org.lobobrowser.html.gui._
+import org.lobobrowser.html._
+import org.lobobrowser.html.style.CSSUtilities
+import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
+
+import org.gjt.sp.jedit.jEdit
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.textarea.AntiAlias
+
+import scala.io.Source
+
+
+class StateViewDockable(view : View, position : String) extends JPanel {
+
+ // outer panel
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+ setLayout(new BorderLayout)
+
+
+ // global logging
+
+ Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
+
+
+ // document template with styles
+
+ private def try_file(name: String): String =
+ {
+ val file = Isabelle.system.platform_file(name)
+ if (file.exists) Source.fromFile(file).mkString else ""
+ }
+
+
+ // HTML panel
+
+ val panel = new HtmlPanel
+ val ucontext = new SimpleUserAgentContext
+ val rcontext = new SimpleHtmlRendererContext(panel, ucontext)
+ val doc = {
+ val builder = new DocumentBuilderImpl(ucontext, rcontext)
+ builder.parse(new InputSourceImpl(new StringReader(
+ """
+
+
+
+
+
+
+""")))
+ }
+
+ val empty_body = XML.document_node(doc, XML.elem(HTML.BODY))
+ doc.appendChild(empty_body)
+
+ panel.setDocument(doc, rcontext)
+ add(panel, BorderLayout.CENTER)
+
+
+ // register for state-view
+ Isabelle.plugin.state_update += (cmd => {
+ val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
+
+ Swing_Thread.later {
+ val node =
+ if (cmd == null) empty_body
+ else {
+ val xml = XML.elem(HTML.BODY,
+ cmd.results(theory_view.current_document).
+ map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))
+ XML.document_node(doc, xml)
+ }
+ doc.removeChild(doc.getLastChild())
+ doc.appendChild(node)
+ panel.delayedRelayout(node.asInstanceOf[NodeImpl])
+ }
+ })
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/jedit/token_marker.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/token_marker.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,154 @@
+/*
+ * 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
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/Change.scala
--- a/src/Tools/jEdit/src/proofdocument/Change.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-/*
- * Changes of plain text
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.proofdocument
-
-
-sealed abstract class Edit
-{
- val start: Int
- def before(offset: Int): Int
- def after(offset: Int): Int
-}
-
-
-case class Insert(start: Int, text: String) extends Edit
-{
- def before(offset: Int): Int =
- if (start > offset) offset
- else (offset - text.length) max start
-
- def after(offset: Int): Int =
- if (start <= offset) offset + text.length else offset
-}
-
-
-case class Remove(start: Int, text: String) extends Edit
-{
- def before(offset: Int): Int =
- if (start <= offset) offset + text.length else offset
-
- def after(offset: Int): Int =
- if (start > offset) offset
- else (offset - text.length) max start
-}
-// TODO: merge multiple inserts?
-
-
-class Change(
- val id: String,
- val parent: Option[Change],
- val edits: List[Edit])
-{
- def ancestors(done: Change => Boolean): List[Change] =
- if (done(this)) Nil
- else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
- def ancestors: List[Change] = ancestors(_ => false)
-
- override def toString =
- "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")"
-}
\ No newline at end of file
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,277 +0,0 @@
-/*
- * Document as list of commands, consisting of lists of tokens
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-import scala.actors.Actor, Actor._
-
-import java.util.regex.Pattern
-
-import isabelle.prover.{Prover, Command, Command_State}
-
-
-object ProofDocument
-{
- // Be careful when changing this regex. Not only must it handle the
- // spurious end of a token but also:
- // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
- // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
-
- val token_pattern =
- Pattern.compile(
- "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
- "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
- "(\\?'?|')[A-Za-z_0-9.]*|" +
- "[A-Za-z_0-9.]+|" +
- "[!#$%&*+-/<=>?@^_|~]+|" +
- "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
- "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
- "[()\\[\\]{}:;]", Pattern.MULTILINE)
-
- val empty =
- new ProofDocument(isabelle.jedit.Isabelle.system.id(),
- Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
-
- type StructureChange = List[(Option[Command], Option[Command])]
-
-}
-
-class ProofDocument(
- val id: String,
- val tokens: Linear_Set[Token],
- val token_start: Map[Token, Int],
- val commands: Linear_Set[Command],
- var states: Map[Command, Command_State], // FIXME immutable
- is_command_keyword: String => Boolean)
-{
- import ProofDocument.StructureChange
-
- def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(id, tokens, token_start, commands, states, f)
-
- def content = Token.string_from_tokens(Nil ++ tokens, token_start)
-
-
-
- /** token view **/
-
- def text_changed(change: Change): (ProofDocument, StructureChange) =
- {
- def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
- val (doc, chgs) = doc_chgs
- val (new_doc, chg) = doc.text_edit(edit, change.id)
- (new_doc, chgs ++ chg)
- }
- ((this, Nil: StructureChange) /: change.edits)(edit_doc)
- }
-
- def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
- {
- case class TextChange(start: Int, added: String, removed: String)
- val change = e match {
- case Insert(s, a) => TextChange(s, a, "")
- case Remove(s, r) => TextChange(s, "", r)
- }
- //indices of tokens
- var start: Map[Token, Int] = token_start
- def stop(t: Token) = start(t) + t.length
- // split old token lists
- val tokens = Nil ++ this.tokens
- val (begin, remaining) = tokens.span(stop(_) < change.start)
- val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
- // update indices
- start = end.foldLeft(start)((s, t) =>
- s + (t -> (s(t) + change.added.length - change.removed.length)))
-
- val split_begin = removed.takeWhile(start(_) < change.start).
- map (t => {
- val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
- start += (split_tok -> start(t))
- split_tok
- })
-
- val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
- map (t => {
- val split_tok =
- new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
- start += (split_tok -> start(t))
- split_tok
- })
- // update indices
- start = removed.foldLeft (start) ((s, t) => s - t)
- start = split_end.foldLeft (start) ((s, t) =>
- s + (t -> (change.start + change.added.length)))
-
- val ins = new Token(change.added, Token.Kind.OTHER)
- start += (ins -> change.start)
-
- var invalid_tokens = split_begin ::: ins :: split_end ::: end
- var new_tokens: List[Token] = Nil
- var old_suffix: List[Token] = Nil
-
- val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
- val matcher =
- ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
-
- while (matcher.find() && invalid_tokens != Nil) {
- val kind =
- if (is_command_keyword(matcher.group))
- Token.Kind.COMMAND_START
- else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
- Token.Kind.COMMENT
- else
- Token.Kind.OTHER
- val new_token = new Token(matcher.group, kind)
- start += (new_token -> (match_start + matcher.start))
- new_tokens ::= new_token
-
- invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
- invalid_tokens match {
- case t :: ts =>
- if (start(t) == start(new_token) &&
- start(t) > change.start + change.added.length) {
- old_suffix = t :: ts
- new_tokens = new_tokens.tail
- invalid_tokens = Nil
- }
- case _ =>
- }
- }
- val insert = new_tokens.reverse
- val new_token_list = begin ::: insert ::: old_suffix
- token_changed(id, begin.lastOption, insert,
- old_suffix.firstOption, new_token_list, start)
- }
-
-
- /** command view **/
-
- private def token_changed(
- new_id: String,
- before_change: Option[Token],
- inserted_tokens: List[Token],
- after_change: Option[Token],
- new_tokens: List[Token],
- new_token_start: Map[Token, Int]):
- (ProofDocument, StructureChange) =
- {
- val new_tokenset = Linear_Set[Token]() ++ new_tokens
- val cmd_before_change = before_change match {
- case None => None
- case Some(bc) =>
- val cmd_with_bc = commands.find(_.contains(bc)).get
- if (cmd_with_bc.tokens.last == bc) {
- if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
- Some(cmd_with_bc)
- else commands.prev(cmd_with_bc)
- }
- else commands.prev(cmd_with_bc)
- }
-
- val cmd_after_change = after_change match {
- case None => None
- case Some(ac) =>
- val cmd_with_ac = commands.find(_.contains(ac)).get
- if (ac.is_start)
- Some(cmd_with_ac)
- else
- commands.next(cmd_with_ac)
- }
-
- val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
- takeWhile(Some(_) != cmd_after_change)
-
- // calculate inserted commands
- def tokens_to_commands(tokens: List[Token]): List[Command]= {
- tokens match {
- case Nil => Nil
- case t :: ts =>
- val (cmd, rest) =
- ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
- new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
- }
- }
-
- val split_begin =
- if (before_change.isDefined) {
- val changed =
- if (cmd_before_change.isDefined)
- new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
- else new_tokenset
- if (changed.exists(_ == before_change.get))
- changed.takeWhile(_ != before_change.get).toList :::
- List(before_change.get)
- else Nil
- } else Nil
-
- val split_end =
- if (after_change.isDefined) {
- val unchanged = new_tokens.dropWhile(_ != after_change.get)
- if(cmd_after_change.isDefined) {
- if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
- unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
- else Nil
- } else {
- unchanged
- }
- } else Nil
-
- val rescan_begin =
- split_begin :::
- before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
- val rescanning_tokens =
- after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
- split_end
- val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
-
- // build new document
- val new_commandset = commands.
- delete_between(cmd_before_change, cmd_after_change).
- append_after(cmd_before_change, inserted_commands)
-
-
- val doc =
- new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
- states -- removed_commands, is_command_keyword)
-
- val removes =
- for (cmd <- removed_commands) yield (cmd_before_change -> None)
- val inserts =
- for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
-
- return (doc, removes.toList ++ inserts)
- }
-
- val commands_offsets = {
- var last_stop = 0
- (for (c <- commands) yield {
- val r = c -> (last_stop,c.stop(this))
- last_stop = c.stop(this)
- r
- }).toArray
- }
-
- def command_at(pos: Int): Option[Command] =
- find_command(pos, 0, commands_offsets.length)
-
- // use a binary search to find commands for a given offset
- private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
- {
- val middle_index = (array_start + array_stop) / 2
- if (middle_index >= commands_offsets.length) return None
- val (middle, (start, stop)) = commands_offsets(middle_index)
- // does middle contain pos?
- if (start <= pos && pos < stop)
- Some(middle)
- else if (start > pos)
- find_command(pos, array_start, middle_index)
- else if (stop <= pos)
- find_command(pos, middle_index + 1, array_stop)
- else error("impossible")
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-/*
- * Document tokens as text ranges
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.proofdocument
-
-
-import isabelle.prover.Command
-
-
-object Token {
- object Kind extends Enumeration
- {
- val COMMAND_START = Value("COMMAND_START")
- val COMMENT = Value("COMMENT")
- val OTHER = Value("OTHER")
- }
-
- def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
- def stop(t: Token) = starts(t) + t.length
- tokens match {
- case Nil => ""
- case tok :: toks =>
- val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
- (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
- res
- }
- }
-
-}
-
-class Token(
- val content: String,
- val kind: Token.Kind.Value)
-{
- override def toString = content
- val length = content.length
- val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/change.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/change.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,54 @@
+/*
+ * Changes of plain text
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.proofdocument
+
+
+sealed abstract class Edit
+{
+ val start: Int
+ def before(offset: Int): Int
+ def after(offset: Int): Int
+}
+
+
+case class Insert(start: Int, text: String) extends Edit
+{
+ def before(offset: Int): Int =
+ if (start > offset) offset
+ else (offset - text.length) max start
+
+ def after(offset: Int): Int =
+ if (start <= offset) offset + text.length else offset
+}
+
+
+case class Remove(start: Int, text: String) extends Edit
+{
+ def before(offset: Int): Int =
+ if (start <= offset) offset + text.length else offset
+
+ def after(offset: Int): Int =
+ if (start > offset) offset
+ else (offset - text.length) max start
+}
+// TODO: merge multiple inserts?
+
+
+class Change(
+ val id: String,
+ val parent: Option[Change],
+ val edits: List[Edit])
+{
+ def ancestors(done: Change => Boolean): List[Change] =
+ if (done(this)) Nil
+ else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
+ def ancestors: List[Change] = ancestors(_ => false)
+
+ override def toString =
+ "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")"
+}
\ No newline at end of file
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/command.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,124 @@
+/*
+ * Prover commands with semantic state
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.prover
+
+
+import scala.actors.Actor, Actor._
+
+import scala.collection.mutable
+
+import isabelle.proofdocument.{Token, ProofDocument}
+import isabelle.jedit.{Isabelle, Plugin}
+import isabelle.XML
+
+
+trait Accumulator extends Actor
+{
+ start() // start actor
+
+ protected var _state: State
+ def state = _state
+
+ override def act() {
+ loop {
+ react {
+ case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
+ case bad => System.err.println("prover: ignoring bad message " + bad)
+ }
+ }
+ }
+}
+
+
+object Command
+{
+ object Status extends Enumeration
+ {
+ val UNPROCESSED = Value("UNPROCESSED")
+ val FINISHED = Value("FINISHED")
+ val FAILED = Value("FAILED")
+ }
+
+ case class HighlightInfo(highlight: String) { override def toString = highlight }
+ case class TypeInfo(ty: String)
+ case class RefInfo(file: Option[String], line: Option[Int],
+ command_id: Option[String], offset: Option[Int])
+}
+
+
+class Command(
+ val tokens: List[Token],
+ val starts: Map[Token, Int]) extends Accumulator
+{
+ require(!tokens.isEmpty)
+
+ val id = Isabelle.system.id()
+ override def hashCode = id.hashCode
+
+
+ /* content */
+
+ override def toString = name
+
+ val name = tokens.head.content
+ val content: String = Token.string_from_tokens(tokens, starts)
+ 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 contains(p: Token) = tokens.contains(p)
+
+ protected override var _state = new State(this)
+
+
+ /* markup */
+
+ lazy val empty_markup = new Markup_Text(Nil, content)
+
+ def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
+ {
+ val start = symbol_index.decode(begin)
+ val stop = symbol_index.decode(end)
+ new Markup_Tree(new Markup_Node(start, stop, info), Nil)
+ }
+
+
+ /* results, markup, ... */
+
+ private val empty_cmd_state = new Command_State(this)
+ private def cmd_state(doc: ProofDocument) =
+ 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)
+}
+
+
+class Command_State(val command: Command) extends Accumulator
+{
+ protected override var _state = new State(command)
+
+ def results: List[XML.Tree] =
+ command.state.results ::: state.results
+
+ def markup_root: Markup_Text =
+ (command.state.markup_root /: state.markup_root.markup)(_ + _)
+
+ def type_at(pos: Int): Option[String] = state.type_at(pos)
+
+ def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
+
+ def highlight: Markup_Text =
+ (command.state.highlight /: state.highlight.markup)(_ + _)
+}
\ No newline at end of file
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/markup_node.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,111 @@
+/*
+ * Document markup nodes, with connection to Swing tree model
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.prover
+
+
+import javax.swing.tree.DefaultMutableTreeNode
+
+import isabelle.proofdocument.ProofDocument
+
+
+class Markup_Node(val start: Int, val stop: Int, val info: Any)
+{
+ def fits_into(that: Markup_Node): Boolean =
+ that.start <= this.start && this.stop <= that.stop
+}
+
+
+class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
+{
+ def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
+
+ private def add(branch: Markup_Tree) = // FIXME avoid sort
+ set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
+
+ private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
+
+ def + (new_tree: Markup_Tree): Markup_Tree =
+ {
+ val new_node = new_tree.node
+ if (new_node fits_into node) {
+ var inserted = false
+ val new_branches =
+ branches.map(branch =>
+ if ((new_node fits_into branch.node) && !inserted) {
+ inserted = true
+ branch + new_tree
+ }
+ else branch)
+ if (!inserted) {
+ // new_tree did not fit into children of this
+ // -> insert between this and its branches
+ val fitting = branches filter(_.node fits_into new_node)
+ (this remove fitting) add ((new_tree /: fitting)(_ + _))
+ }
+ else set_branches(new_branches)
+ }
+ else {
+ System.err.println("ignored nonfitting markup: " + new_node)
+ this
+ }
+ }
+
+ def flatten: List[Markup_Node] =
+ {
+ var next_x = node.start
+ if (branches.isEmpty) List(this.node)
+ else {
+ val filled_gaps =
+ for {
+ child <- branches
+ markups =
+ if (next_x < child.node.start)
+ new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+ else child.flatten
+ update = (next_x = child.node.stop)
+ markup <- markups
+ } yield markup
+ if (next_x < node.stop)
+ filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+ else filled_gaps
+ }
+ }
+}
+
+
+class Markup_Text(val markup: List[Markup_Tree], val content: String)
+{
+ private lazy val root =
+ new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+
+ def + (new_tree: Markup_Tree): Markup_Text =
+ new Markup_Text((root + new_tree).branches, content)
+
+ def filter(pred: Markup_Node => Boolean): Markup_Text =
+ {
+ def filt(tree: Markup_Tree): List[Markup_Tree] =
+ {
+ val branches = tree.branches.flatMap(filt(_))
+ if (pred(tree.node)) List(tree.set_branches(branches))
+ else branches
+ }
+ new Markup_Text(markup.flatMap(filt(_)), content)
+ }
+
+ def flatten: List[Markup_Node] = markup.flatten(_.flatten)
+
+ def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
+ {
+ def swing(tree: Markup_Tree): DefaultMutableTreeNode =
+ {
+ val node = swing_node(tree.node)
+ tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
+ node
+ }
+ swing(root)
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/proof_document.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,277 @@
+/*
+ * Document as list of commands, consisting of lists of tokens
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.proofdocument
+
+import scala.actors.Actor, Actor._
+
+import java.util.regex.Pattern
+
+import isabelle.prover.{Prover, Command, Command_State}
+
+
+object ProofDocument
+{
+ // Be careful when changing this regex. Not only must it handle the
+ // spurious end of a token but also:
+ // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
+ // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
+
+ val token_pattern =
+ Pattern.compile(
+ "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
+ "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
+ "(\\?'?|')[A-Za-z_0-9.]*|" +
+ "[A-Za-z_0-9.]+|" +
+ "[!#$%&*+-/<=>?@^_|~]+|" +
+ "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
+ "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
+ "[()\\[\\]{}:;]", Pattern.MULTILINE)
+
+ val empty =
+ new ProofDocument(isabelle.jedit.Isabelle.system.id(),
+ Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
+
+ type StructureChange = List[(Option[Command], Option[Command])]
+
+}
+
+class ProofDocument(
+ val id: String,
+ val tokens: Linear_Set[Token],
+ val token_start: Map[Token, Int],
+ val commands: Linear_Set[Command],
+ var states: Map[Command, Command_State], // FIXME immutable
+ is_command_keyword: String => Boolean)
+{
+ import ProofDocument.StructureChange
+
+ def set_command_keyword(f: String => Boolean): ProofDocument =
+ new ProofDocument(id, tokens, token_start, commands, states, f)
+
+ def content = Token.string_from_tokens(Nil ++ tokens, token_start)
+
+
+
+ /** token view **/
+
+ def text_changed(change: Change): (ProofDocument, StructureChange) =
+ {
+ def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
+ val (doc, chgs) = doc_chgs
+ val (new_doc, chg) = doc.text_edit(edit, change.id)
+ (new_doc, chgs ++ chg)
+ }
+ ((this, Nil: StructureChange) /: change.edits)(edit_doc)
+ }
+
+ def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
+ {
+ case class TextChange(start: Int, added: String, removed: String)
+ val change = e match {
+ case Insert(s, a) => TextChange(s, a, "")
+ case Remove(s, r) => TextChange(s, "", r)
+ }
+ //indices of tokens
+ var start: Map[Token, Int] = token_start
+ def stop(t: Token) = start(t) + t.length
+ // split old token lists
+ val tokens = Nil ++ this.tokens
+ val (begin, remaining) = tokens.span(stop(_) < change.start)
+ val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
+ // update indices
+ start = end.foldLeft(start)((s, t) =>
+ s + (t -> (s(t) + change.added.length - change.removed.length)))
+
+ val split_begin = removed.takeWhile(start(_) < change.start).
+ map (t => {
+ val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
+ start += (split_tok -> start(t))
+ split_tok
+ })
+
+ val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
+ map (t => {
+ val split_tok =
+ new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
+ start += (split_tok -> start(t))
+ split_tok
+ })
+ // update indices
+ start = removed.foldLeft (start) ((s, t) => s - t)
+ start = split_end.foldLeft (start) ((s, t) =>
+ s + (t -> (change.start + change.added.length)))
+
+ val ins = new Token(change.added, Token.Kind.OTHER)
+ start += (ins -> change.start)
+
+ var invalid_tokens = split_begin ::: ins :: split_end ::: end
+ var new_tokens: List[Token] = Nil
+ var old_suffix: List[Token] = Nil
+
+ val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
+ val matcher =
+ ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
+
+ while (matcher.find() && invalid_tokens != Nil) {
+ val kind =
+ if (is_command_keyword(matcher.group))
+ Token.Kind.COMMAND_START
+ else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
+ Token.Kind.COMMENT
+ else
+ Token.Kind.OTHER
+ val new_token = new Token(matcher.group, kind)
+ start += (new_token -> (match_start + matcher.start))
+ new_tokens ::= new_token
+
+ invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
+ invalid_tokens match {
+ case t :: ts =>
+ if (start(t) == start(new_token) &&
+ start(t) > change.start + change.added.length) {
+ old_suffix = t :: ts
+ new_tokens = new_tokens.tail
+ invalid_tokens = Nil
+ }
+ case _ =>
+ }
+ }
+ val insert = new_tokens.reverse
+ val new_token_list = begin ::: insert ::: old_suffix
+ token_changed(id, begin.lastOption, insert,
+ old_suffix.firstOption, new_token_list, start)
+ }
+
+
+ /** command view **/
+
+ private def token_changed(
+ new_id: String,
+ before_change: Option[Token],
+ inserted_tokens: List[Token],
+ after_change: Option[Token],
+ new_tokens: List[Token],
+ new_token_start: Map[Token, Int]):
+ (ProofDocument, StructureChange) =
+ {
+ val new_tokenset = Linear_Set[Token]() ++ new_tokens
+ val cmd_before_change = before_change match {
+ case None => None
+ case Some(bc) =>
+ val cmd_with_bc = commands.find(_.contains(bc)).get
+ if (cmd_with_bc.tokens.last == bc) {
+ if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
+ Some(cmd_with_bc)
+ else commands.prev(cmd_with_bc)
+ }
+ else commands.prev(cmd_with_bc)
+ }
+
+ val cmd_after_change = after_change match {
+ case None => None
+ case Some(ac) =>
+ val cmd_with_ac = commands.find(_.contains(ac)).get
+ if (ac.is_start)
+ Some(cmd_with_ac)
+ else
+ commands.next(cmd_with_ac)
+ }
+
+ val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
+ takeWhile(Some(_) != cmd_after_change)
+
+ // calculate inserted commands
+ def tokens_to_commands(tokens: List[Token]): List[Command]= {
+ tokens match {
+ case Nil => Nil
+ case t :: ts =>
+ val (cmd, rest) =
+ ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
+ new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
+ }
+ }
+
+ val split_begin =
+ if (before_change.isDefined) {
+ val changed =
+ if (cmd_before_change.isDefined)
+ new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
+ else new_tokenset
+ if (changed.exists(_ == before_change.get))
+ changed.takeWhile(_ != before_change.get).toList :::
+ List(before_change.get)
+ else Nil
+ } else Nil
+
+ val split_end =
+ if (after_change.isDefined) {
+ val unchanged = new_tokens.dropWhile(_ != after_change.get)
+ if(cmd_after_change.isDefined) {
+ if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+ unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+ else Nil
+ } else {
+ unchanged
+ }
+ } else Nil
+
+ val rescan_begin =
+ split_begin :::
+ before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
+ val rescanning_tokens =
+ after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
+ split_end
+ val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
+
+ // build new document
+ val new_commandset = commands.
+ delete_between(cmd_before_change, cmd_after_change).
+ append_after(cmd_before_change, inserted_commands)
+
+
+ val doc =
+ new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
+ states -- removed_commands, is_command_keyword)
+
+ val removes =
+ for (cmd <- removed_commands) yield (cmd_before_change -> None)
+ val inserts =
+ for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
+
+ return (doc, removes.toList ++ inserts)
+ }
+
+ val commands_offsets = {
+ var last_stop = 0
+ (for (c <- commands) yield {
+ val r = c -> (last_stop,c.stop(this))
+ last_stop = c.stop(this)
+ r
+ }).toArray
+ }
+
+ def command_at(pos: Int): Option[Command] =
+ find_command(pos, 0, commands_offsets.length)
+
+ // use a binary search to find commands for a given offset
+ private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
+ {
+ val middle_index = (array_start + array_stop) / 2
+ if (middle_index >= commands_offsets.length) return None
+ val (middle, (start, stop)) = commands_offsets(middle_index)
+ // does middle contain pos?
+ if (start <= pos && pos < stop)
+ Some(middle)
+ else if (start > pos)
+ find_command(pos, array_start, middle_index)
+ else if (stop <= pos)
+ find_command(pos, middle_index + 1, array_stop)
+ else error("impossible")
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/prover.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/prover.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,175 @@
+/*
+ * Higher-level prover communication: interactive document model
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.prover
+
+
+import scala.actors.Actor, Actor._
+
+import javax.swing.JTextArea
+
+import isabelle.jedit.Isabelle
+import isabelle.proofdocument.{ProofDocument, Change, Token}
+
+
+class Prover(system: Isabelle_System, logic: String)
+{
+ /* incoming messages */
+
+ private var prover_ready = false
+
+ private val receiver = new Actor {
+ def act() {
+ loop {
+ react {
+ case result: Isabelle_Process.Result => handle_result(result)
+ case change: Change if prover_ready => handle_change(change)
+ case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
+ }
+ }
+ }
+ }
+
+ def input(change: Change) { receiver ! change }
+
+
+ /* outgoing messages */
+
+ val command_change = new Event_Bus[Command]
+ val document_change = new Event_Bus[ProofDocument]
+
+
+ /* prover process */
+
+ private val process =
+ new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
+
+
+ /* outer syntax keywords and completion */
+
+ @volatile private var _command_decls = Map[String, String]()
+ def command_decls() = _command_decls
+
+ @volatile private var _keyword_decls = Set[String]()
+ def keyword_decls() = _keyword_decls
+
+ @volatile private var _completion = Isabelle.completion
+ def completion() = _completion
+
+
+ /* document state information */
+
+ @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.
+ 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] =
+ document_versions.find(_.id == id)
+
+
+ /* prover results */
+
+ val output_text_view = new JTextArea // FIXME separate jEdit component
+
+ private def handle_result(result: Isabelle_Process.Result)
+ {
+ // FIXME separate jEdit component
+ Swing_Thread.later { output_text_view.append(result.toString + "\n") }
+
+ val message = Isabelle_Process.parse_message(system, result)
+
+ val state =
+ Position.id_of(result.props) match {
+ case None => None
+ case Some(id) => commands.get(id) orElse states.get(id) orElse None
+ }
+ if (state.isDefined) state.get ! (this, message)
+ else if (result.kind == Isabelle_Process.Kind.STATUS) {
+ //{{{ global status message
+ message match {
+ case XML.Elem(Markup.MESSAGE, _, elems) =>
+ for (elem <- elems) {
+ elem match {
+ // document edits
+ case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
+ document_versions.find(_.id == doc_id) match {
+ case Some(doc) =>
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+ <- edits }
+ {
+ commands.get(cmd_id) match {
+ case Some(cmd) =>
+ val state = new Command_State(cmd)
+ states += (state_id -> state)
+ doc.states += (cmd -> state)
+ command_change.event(cmd) // FIXME really!?
+ case None =>
+ }
+ }
+ case None =>
+ }
+
+ // command and keyword declarations
+ case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+ _command_decls += (name -> kind)
+ _completion += name
+ case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+ _keyword_decls += name
+ _completion += name
+
+ // process ready (after initialization)
+ case XML.Elem(Markup.READY, _, _) => prover_ready = true
+
+ case _ =>
+ }
+ }
+ case _ =>
+ }
+ //}}}
+ }
+ }
+
+
+ /* document changes */
+
+ def begin_document(path: String) {
+ process.begin_document(document_0.id, path)
+ }
+
+ def handle_change(change: Change) {
+ val old = document(change.parent.get.id).get
+ val (doc, changes) = old.text_changed(change)
+ document_versions ::= doc
+
+ val id_changes = changes map { case (c1, c2) =>
+ (c1.map(_.id).getOrElse(document_0.id),
+ c2 match {
+ case None => None
+ case Some(command) =>
+ commands += (command.id -> command)
+ process.define_command(command.id, system.symbols.encode(command.content))
+ Some(command.id)
+ })
+ }
+ process.edit_document(old.id, doc.id, id_changes)
+
+ document_change.event(doc)
+ }
+
+
+ /* main controls */
+
+ def start() { receiver.start() }
+
+ def stop() { process.kill() }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/state.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/state.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,117 @@
+/*
+ * Accumulating results from prover
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.prover
+
+
+class State(
+ val command: Command,
+ val status: Command.Status.Value,
+ rev_results: List[XML.Tree],
+ val markup_root: Markup_Text)
+{
+ def this(command: Command) =
+ this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
+
+
+ /* content */
+
+ private def set_status(st: Command.Status.Value): State =
+ new State(command, st, rev_results, markup_root)
+
+ private def add_result(res: XML.Tree): State =
+ new State(command, status, res :: rev_results, markup_root)
+
+ private def add_markup(node: Markup_Tree): State =
+ new State(command, status, rev_results, markup_root + node)
+
+ lazy val results = rev_results.reverse
+
+
+ /* markup */
+
+ lazy val highlight: Markup_Text =
+ {
+ markup_root.filter(_.info match {
+ case Command.HighlightInfo(_) => true
+ case _ => false
+ })
+ }
+
+ private lazy val types: List[Markup_Node] =
+ markup_root.filter(_.info match {
+ case Command.TypeInfo(_) => true
+ case _ => false }).flatten
+
+ def type_at(pos: Int): Option[String] =
+ {
+ types.find(t => t.start <= pos && pos < t.stop) match {
+ case Some(t) =>
+ t.info match {
+ case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
+ case _ => None
+ }
+ case None => None
+ }
+ }
+
+ private lazy val refs: List[Markup_Node] =
+ markup_root.filter(_.info match {
+ case Command.RefInfo(_, _, _, _) => true
+ case _ => false }).flatten
+
+ def ref_at(pos: Int): Option[Markup_Node] =
+ refs.find(t => t.start <= pos && pos < t.stop)
+
+
+ /* message dispatch */
+
+ def + (prover: Prover, message: XML.Tree): State =
+ {
+ val changed: State =
+ message match {
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
+ case XML.Elem(kind, atts, body) =>
+ val (begin, end) = Position.offsets_of(atts)
+ if (begin.isEmpty || end.isEmpty) state
+ else if (kind == Markup.ML_TYPING) {
+ val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
+ state.add_markup(
+ command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
+ }
+ else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+ state.add_markup(command.markup_node(
+ begin.get - 1, end.get - 1,
+ Command.RefInfo(
+ Position.file_of(atts),
+ Position.line_of(atts),
+ Position.id_of(atts),
+ Position.offset_of(atts))))
+ case _ => state
+ }
+ }
+ else {
+ state.add_markup(
+ command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
+ }
+ case _ =>
+ System.err.println("ignored status report: " + elem)
+ state
+ })
+ case _ => add_result(message)
+ }
+ if (!(this eq changed)) prover.command_change.event(command)
+ changed
+ }
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/theory_view.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,327 @@
+/*
+ * jEdit text area as document text source
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+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}
+
+import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
+
+
+object TheoryView
+{
+ def choose_color(command: Command, doc: ProofDocument): Color =
+ {
+ command.status(doc) match {
+ case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+ case Command.Status.FINISHED => new Color(234, 248, 255)
+ case Command.Status.FAILED => new Color(255, 106, 106)
+ case _ => Color.red
+ }
+ }
+}
+
+
+class TheoryView(text_area: JEditTextArea)
+{
+ private val buffer = text_area.getBuffer
+
+
+ /* prover setup */
+
+ val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
+
+ prover.command_change += ((command: Command) =>
+ if (current_document().commands.contains(command))
+ Swing_Thread.later {
+ // FIXME proper handling of buffer vs. text areas
+ // repaint if buffer is active
+ if (text_area.getBuffer == buffer) {
+ update_syntax(command)
+ invalidate_line(command)
+ overview.repaint()
+ }
+ })
+
+
+ /* changes vs. edits */
+
+ private val change_0 = new Change(prover.document_0.id, None, Nil)
+ private var _changes = List(change_0) // owned by Swing/AWT thread
+ def changes = _changes
+ private var current_change = change_0
+
+ private val edits = new mutable.ListBuffer[Edit] // owned by Swing thread
+
+ private val edits_delay = Swing_Thread.delay_last(300) {
+ if (!edits.isEmpty) {
+ val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
+ _changes ::= change
+ prover.input(change)
+ current_change = change
+ edits.clear
+ }
+ }
+
+
+ /* buffer_listener */
+
+ private val buffer_listener = new BufferListener {
+ override def preContentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int)
+ {
+ edits += Insert(offset, buffer.getText(offset, length))
+ edits_delay()
+ }
+
+ override def preContentRemoved(buffer: JEditBuffer,
+ start_line: Int, start: Int, num_lines: Int, removed_length: Int)
+ {
+ edits += Remove(start, buffer.getText(start, removed_length))
+ edits_delay()
+ }
+
+ override def contentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+ override def contentRemoved(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+ override def bufferLoaded(buffer: JEditBuffer) { }
+ override def foldHandlerChanged(buffer: JEditBuffer) { }
+ override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
+ override def transactionComplete(buffer: JEditBuffer) { }
+ }
+
+
+ /* text_area_extension */
+
+ private val text_area_extension = new TextAreaExtension {
+ override def paintValidLine(gfx: Graphics2D,
+ 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)
+ val saved_color = gfx.getColor
+
+ val metrics = text_area.getPainter.getFontMetrics
+
+ // encolor phase
+ var cmd = document.command_at(from_current(start))
+ while (cmd.isDefined && cmd.get.start(document) < end) {
+ val e = cmd.get
+ 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)
+ cmd = document.commands.next(e)
+ }
+
+ gfx.setColor(saved_color)
+ }
+
+ override def getToolTipText(x: Int, y: Int): String =
+ {
+ val document = current_document()
+ val offset = from_current(document, text_area.xyToOffset(x, y))
+ document.command_at(offset) match {
+ case Some(cmd) =>
+ document.token_start(cmd.tokens.first)
+ cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
+ case None => null
+ }
+ }
+ }
+
+
+ /* activation */
+
+ private val overview = new Document_Overview(prover, text_area, to_current)
+
+ private val selected_state_controller = new CaretListener {
+ override def caretUpdate(e: CaretEvent) {
+ val doc = current_document()
+ doc.command_at(e.getDot) match {
+ case Some(cmd)
+ if (doc.token_start(cmd.tokens.first) <= e.getDot &&
+ Isabelle.plugin.selected_state != cmd) =>
+ Isabelle.plugin.selected_state = cmd
+ case _ =>
+ }
+ }
+ }
+
+ 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.addBufferListener(buffer_listener)
+
+ val dockable =
+ text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
+ if (dockable != null) {
+ val output_dockable = dockable.asInstanceOf[OutputDockable]
+ val output_text_view = prover.output_text_view
+ output_dockable.set_text(output_text_view)
+ }
+
+ buffer.propertiesChanged()
+ }
+
+ def deactivate() {
+ buffer.setTokenMarker(buffer.getMode.getTokenMarker)
+ buffer.removeBufferListener(buffer_listener)
+ text_area.getPainter.removeExtension(text_area_extension)
+ text_area.removeLeftOfScrollBar(overview)
+ text_area.removeCaretListener(selected_state_controller)
+ }
+
+
+ /* history of changes */
+
+ private def doc_or_pred(c: Change): ProofDocument =
+ prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
+
+ def current_document() = doc_or_pred(current_change)
+
+
+ /* update to desired version */
+
+ def set_version(goal: Change) {
+ // changes in buffer must be ignored
+ buffer.removeBufferListener(buffer_listener)
+
+ def apply(change: Change): Unit = change.edits.foreach {
+ case Insert(start, text) => buffer.insert(start, text)
+ case Remove(start, text) => buffer.remove(start, text.length)
+ }
+
+ def unapply(change: Change): Unit = change.edits.reverse.foreach {
+ case Insert(start, text) => buffer.remove(start, text.length)
+ case Remove(start, text) => buffer.insert(start, text)
+ }
+
+ // undo/redo changes
+ val ancs_current = current_change.ancestors
+ val ancs_goal = goal.ancestors
+ val paired = ancs_current.reverse zip ancs_goal.reverse
+ def last_common[A](xs: List[(A, A)]): Option[A] = {
+ xs match {
+ case (x, y) :: xs =>
+ if (x == y)
+ xs match {
+ case (a, b) :: ys =>
+ if (a == b) last_common(xs)
+ else Some(x)
+ case _ => Some(x)
+ }
+ else None
+ case _ => None
+ }
+ }
+ val common_anc = last_common(paired).get
+
+ ancs_current.takeWhile(_ != common_anc) map unapply
+ ancs_goal.takeWhile(_ != common_anc).reverse map apply
+
+ current_change = goal
+ // invoke repaint
+ buffer.propertiesChanged()
+ invalidate_all()
+ overview.repaint()
+
+ // track changes in buffer
+ buffer.addBufferListener(buffer_listener)
+ }
+
+
+ /* transforming offsets */
+
+ private def changes_from(doc: ProofDocument): List[Edit] =
+ List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
+ edits.toList
+
+ def from_current(doc: ProofDocument, offset: Int): Int =
+ (offset /: changes_from(doc).reverse) ((i, change) => change before i)
+
+ def to_current(doc: ProofDocument, offset: Int): Int =
+ (offset /: changes_from(doc)) ((i, change) => change after i)
+
+
+ private def lines_of_command(cmd: Command) =
+ {
+ val document = current_document()
+ (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
+ buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
+ }
+
+
+ /* (re)painting */
+
+ private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
+
+ private def update_syntax(cmd: Command) {
+ val (line1, line2) = lines_of_command(cmd)
+ if (line2 >= text_area.getFirstLine &&
+ line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+ update_delay()
+ }
+
+ private def invalidate_line(cmd: Command) =
+ {
+ val (start, stop) = lines_of_command(cmd)
+ text_area.invalidateLineRange(start, stop)
+
+ if (Isabelle.plugin.selected_state == cmd)
+ Isabelle.plugin.selected_state = cmd // update State view
+ }
+
+ private def invalidate_all() =
+ text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
+ text_area.getLastPhysicalLine)
+
+ private def encolor(gfx: Graphics2D,
+ y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
+ {
+ val start = text_area.offsetToXY(begin)
+ val stop =
+ if (finish < buffer.getLength) text_area.offsetToXY(finish)
+ else {
+ val p = text_area.offsetToXY(finish - 1)
+ val metrics = text_area.getPainter.getFontMetrics
+ p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
+ p
+ }
+
+ if (start != null && stop != null) {
+ gfx.setColor(color)
+ if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
+ else gfx.drawRect(start.x, y, stop.x - start.x, height)
+ }
+ }
+
+
+ /* init */
+
+ prover.start()
+
+ edits += Insert(0, buffer.getText(0, buffer.getLength))
+ edits_delay()
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/proofdocument/token.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/token.scala Tue Dec 08 14:49:01 2009 +0100
@@ -0,0 +1,42 @@
+/*
+ * Document tokens as text ranges
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.proofdocument
+
+
+import isabelle.prover.Command
+
+
+object Token {
+ object Kind extends Enumeration
+ {
+ val COMMAND_START = Value("COMMAND_START")
+ val COMMENT = Value("COMMENT")
+ val OTHER = Value("OTHER")
+ }
+
+ def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
+ def stop(t: Token) = starts(t) + t.length
+ tokens match {
+ case Nil => ""
+ case tok :: toks =>
+ val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
+ (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
+ res
+ }
+ }
+
+}
+
+class Token(
+ val content: String,
+ val kind: Token.Kind.Value)
+{
+ override def toString = content
+ val length = content.length
+ val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
+}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-/*
- * Prover commands with semantic state
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.prover
-
-
-import scala.actors.Actor, Actor._
-
-import scala.collection.mutable
-
-import isabelle.proofdocument.{Token, ProofDocument}
-import isabelle.jedit.{Isabelle, Plugin}
-import isabelle.XML
-
-
-trait Accumulator extends Actor
-{
- start() // start actor
-
- protected var _state: State
- def state = _state
-
- override def act() {
- loop {
- react {
- case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
- case bad => System.err.println("prover: ignoring bad message " + bad)
- }
- }
- }
-}
-
-
-object Command
-{
- object Status extends Enumeration
- {
- val UNPROCESSED = Value("UNPROCESSED")
- val FINISHED = Value("FINISHED")
- val FAILED = Value("FAILED")
- }
-
- case class HighlightInfo(highlight: String) { override def toString = highlight }
- case class TypeInfo(ty: String)
- case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[String], offset: Option[Int])
-}
-
-
-class Command(
- val tokens: List[Token],
- val starts: Map[Token, Int]) extends Accumulator
-{
- require(!tokens.isEmpty)
-
- val id = Isabelle.system.id()
- override def hashCode = id.hashCode
-
-
- /* content */
-
- override def toString = name
-
- val name = tokens.head.content
- val content: String = Token.string_from_tokens(tokens, starts)
- 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 contains(p: Token) = tokens.contains(p)
-
- protected override var _state = new State(this)
-
-
- /* markup */
-
- lazy val empty_markup = new Markup_Text(Nil, content)
-
- def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
- {
- val start = symbol_index.decode(begin)
- val stop = symbol_index.decode(end)
- new Markup_Tree(new Markup_Node(start, stop, info), Nil)
- }
-
-
- /* results, markup, ... */
-
- private val empty_cmd_state = new Command_State(this)
- private def cmd_state(doc: ProofDocument) =
- 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)
-}
-
-
-class Command_State(val command: Command) extends Accumulator
-{
- protected override var _state = new State(command)
-
- def results: List[XML.Tree] =
- command.state.results ::: state.results
-
- def markup_root: Markup_Text =
- (command.state.markup_root /: state.markup_root.markup)(_ + _)
-
- def type_at(pos: Int): Option[String] = state.type_at(pos)
-
- def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
-
- def highlight: Markup_Text =
- (command.state.highlight /: state.highlight.markup)(_ + _)
-}
\ No newline at end of file
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-/*
- * Document markup nodes, with connection to Swing tree model
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.prover
-
-
-import javax.swing.tree.DefaultMutableTreeNode
-
-import isabelle.proofdocument.ProofDocument
-
-
-class Markup_Node(val start: Int, val stop: Int, val info: Any)
-{
- def fits_into(that: Markup_Node): Boolean =
- that.start <= this.start && this.stop <= that.stop
-}
-
-
-class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
-{
- def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
-
- private def add(branch: Markup_Tree) = // FIXME avoid sort
- set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
-
- private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
-
- def + (new_tree: Markup_Tree): Markup_Tree =
- {
- val new_node = new_tree.node
- if (new_node fits_into node) {
- var inserted = false
- val new_branches =
- branches.map(branch =>
- if ((new_node fits_into branch.node) && !inserted) {
- inserted = true
- branch + new_tree
- }
- else branch)
- if (!inserted) {
- // new_tree did not fit into children of this
- // -> insert between this and its branches
- val fitting = branches filter(_.node fits_into new_node)
- (this remove fitting) add ((new_tree /: fitting)(_ + _))
- }
- else set_branches(new_branches)
- }
- else {
- System.err.println("ignored nonfitting markup: " + new_node)
- this
- }
- }
-
- def flatten: List[Markup_Node] =
- {
- var next_x = node.start
- if (branches.isEmpty) List(this.node)
- else {
- val filled_gaps =
- for {
- child <- branches
- markups =
- if (next_x < child.node.start)
- new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
- else child.flatten
- update = (next_x = child.node.stop)
- markup <- markups
- } yield markup
- if (next_x < node.stop)
- filled_gaps + new Markup_Node(next_x, node.stop, node.info)
- else filled_gaps
- }
- }
-}
-
-
-class Markup_Text(val markup: List[Markup_Tree], val content: String)
-{
- private lazy val root =
- new Markup_Tree(new Markup_Node(0, content.length, None), markup)
-
- def + (new_tree: Markup_Tree): Markup_Text =
- new Markup_Text((root + new_tree).branches, content)
-
- def filter(pred: Markup_Node => Boolean): Markup_Text =
- {
- def filt(tree: Markup_Tree): List[Markup_Tree] =
- {
- val branches = tree.branches.flatMap(filt(_))
- if (pred(tree.node)) List(tree.set_branches(branches))
- else branches
- }
- new Markup_Text(markup.flatMap(filt(_)), content)
- }
-
- def flatten: List[Markup_Node] = markup.flatten(_.flatten)
-
- def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
- {
- def swing(tree: Markup_Tree): DefaultMutableTreeNode =
- {
- val node = swing_node(tree.node)
- tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
- node
- }
- swing(root)
- }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,175 +0,0 @@
-/*
- * Higher-level prover communication: interactive document model
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.prover
-
-
-import scala.actors.Actor, Actor._
-
-import javax.swing.JTextArea
-
-import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{ProofDocument, Change, Token}
-
-
-class Prover(system: Isabelle_System, logic: String)
-{
- /* incoming messages */
-
- private var prover_ready = false
-
- private val receiver = new Actor {
- def act() {
- loop {
- react {
- case result: Isabelle_Process.Result => handle_result(result)
- case change: Change if prover_ready => handle_change(change)
- case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
- }
- }
- }
- }
-
- def input(change: Change) { receiver ! change }
-
-
- /* outgoing messages */
-
- val command_change = new Event_Bus[Command]
- val document_change = new Event_Bus[ProofDocument]
-
-
- /* prover process */
-
- private val process =
- new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
-
-
- /* outer syntax keywords and completion */
-
- @volatile private var _command_decls = Map[String, String]()
- def command_decls() = _command_decls
-
- @volatile private var _keyword_decls = Set[String]()
- def keyword_decls() = _keyword_decls
-
- @volatile private var _completion = Isabelle.completion
- def completion() = _completion
-
-
- /* document state information */
-
- @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.
- 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] =
- document_versions.find(_.id == id)
-
-
- /* prover results */
-
- val output_text_view = new JTextArea // FIXME separate jEdit component
-
- private def handle_result(result: Isabelle_Process.Result)
- {
- // FIXME separate jEdit component
- Swing_Thread.later { output_text_view.append(result.toString + "\n") }
-
- val message = Isabelle_Process.parse_message(system, result)
-
- val state =
- Position.id_of(result.props) match {
- case None => None
- case Some(id) => commands.get(id) orElse states.get(id) orElse None
- }
- if (state.isDefined) state.get ! (this, message)
- else if (result.kind == Isabelle_Process.Kind.STATUS) {
- //{{{ global status message
- message match {
- case XML.Elem(Markup.MESSAGE, _, elems) =>
- for (elem <- elems) {
- elem match {
- // document edits
- case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
- document_versions.find(_.id == doc_id) match {
- case Some(doc) =>
- for {
- XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
- <- edits }
- {
- commands.get(cmd_id) match {
- case Some(cmd) =>
- val state = new Command_State(cmd)
- states += (state_id -> state)
- doc.states += (cmd -> state)
- command_change.event(cmd) // FIXME really!?
- case None =>
- }
- }
- case None =>
- }
-
- // command and keyword declarations
- case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
- _command_decls += (name -> kind)
- _completion += name
- case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
- _keyword_decls += name
- _completion += name
-
- // process ready (after initialization)
- case XML.Elem(Markup.READY, _, _) => prover_ready = true
-
- case _ =>
- }
- }
- case _ =>
- }
- //}}}
- }
- }
-
-
- /* document changes */
-
- def begin_document(path: String) {
- process.begin_document(document_0.id, path)
- }
-
- def handle_change(change: Change) {
- val old = document(change.parent.get.id).get
- val (doc, changes) = old.text_changed(change)
- document_versions ::= doc
-
- val id_changes = changes map { case (c1, c2) =>
- (c1.map(_.id).getOrElse(document_0.id),
- c2 match {
- case None => None
- case Some(command) =>
- commands += (command.id -> command)
- process.define_command(command.id, system.symbols.encode(command.content))
- Some(command.id)
- })
- }
- process.edit_document(old.id, doc.id, id_changes)
-
- document_change.event(doc)
- }
-
-
- /* main controls */
-
- def start() { receiver.start() }
-
- def stop() { process.kill() }
-}
diff -r 710e3a9a4c95 -r bfea7839d9e1 src/Tools/jEdit/src/prover/State.scala
--- a/src/Tools/jEdit/src/prover/State.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-/*
- * Accumulating results from prover
- *
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.prover
-
-
-class State(
- val command: Command,
- val status: Command.Status.Value,
- rev_results: List[XML.Tree],
- val markup_root: Markup_Text)
-{
- def this(command: Command) =
- this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
-
-
- /* content */
-
- private def set_status(st: Command.Status.Value): State =
- new State(command, st, rev_results, markup_root)
-
- private def add_result(res: XML.Tree): State =
- new State(command, status, res :: rev_results, markup_root)
-
- private def add_markup(node: Markup_Tree): State =
- new State(command, status, rev_results, markup_root + node)
-
- lazy val results = rev_results.reverse
-
-
- /* markup */
-
- lazy val highlight: Markup_Text =
- {
- markup_root.filter(_.info match {
- case Command.HighlightInfo(_) => true
- case _ => false
- })
- }
-
- private lazy val types: List[Markup_Node] =
- markup_root.filter(_.info match {
- case Command.TypeInfo(_) => true
- case _ => false }).flatten
-
- def type_at(pos: Int): Option[String] =
- {
- types.find(t => t.start <= pos && pos < t.stop) match {
- case Some(t) =>
- t.info match {
- case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
- case _ => None
- }
- case None => None
- }
- }
-
- private lazy val refs: List[Markup_Node] =
- markup_root.filter(_.info match {
- case Command.RefInfo(_, _, _, _) => true
- case _ => false }).flatten
-
- def ref_at(pos: Int): Option[Markup_Node] =
- refs.find(t => t.start <= pos && pos < t.stop)
-
-
- /* message dispatch */
-
- def + (prover: Prover, message: XML.Tree): State =
- {
- val changed: State =
- message match {
- case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(kind, atts, body) =>
- val (begin, end) = Position.offsets_of(atts)
- if (begin.isEmpty || end.isEmpty) state
- else if (kind == Markup.ML_TYPING) {
- val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
- state.add_markup(
- command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
- }
- else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
- state.add_markup(command.markup_node(
- begin.get - 1, end.get - 1,
- Command.RefInfo(
- Position.file_of(atts),
- Position.line_of(atts),
- Position.id_of(atts),
- Position.offset_of(atts))))
- case _ => state
- }
- }
- else {
- state.add_markup(
- command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
- }
- case _ =>
- System.err.println("ignored status report: " + elem)
- state
- })
- case _ => add_result(message)
- }
- if (!(this eq changed)) prover.command_change.event(command)
- changed
- }
-}