--- a/src/Pure/PIDE/document.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 30 17:02:06 2011 +0200
@@ -191,11 +191,11 @@
abstract class Snapshot
{
+ val state: State
val version: Version
val node: Node
val is_outdated: Boolean
- def lookup_command(id: Command_ID): Option[Command]
- def state(command: Command): Command.State
+ def command_state(command: Command): Command.State
def convert(i: Text.Offset): Text.Offset
def convert(range: Text.Range): Text.Range
def revert(i: Text.Offset): Text.Offset
@@ -269,7 +269,16 @@
copy(commands = commands + (id -> command.empty_state))
}
- def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
+ def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
+
+ def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
+ commands.get(id) orElse execs.get(id) match {
+ case None => None
+ case Some(st) =>
+ val command = st.command
+ version.nodes.find({ case (_, node) => node.commands(command) })
+ .map({ case (name, node) => (name, node, command) })
+ }
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename
@@ -366,13 +375,12 @@
new Snapshot
{
+ val state = State.this
val version = stable.version.get_finished
val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
- def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
-
- def state(command: Command): Command.State =
+ def command_state(command: Command): Command.State =
try {
the_exec(the_assignment(version).check_finished.command_execs
.getOrElse(command.id, fail))
@@ -390,7 +398,7 @@
val former_range = revert(range)
for {
(command, command_start) <- node.command_range(former_range).toStream
- Text.Info(r0, x) <- state(command).markup.
+ Text.Info(r0, x) <- command_state(command).markup.
select((former_range - command_start).restrict(command.range)) {
case Text.Info(r0, info)
if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
--- a/src/Pure/System/session.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Pure/System/session.scala Tue Aug 30 17:02:06 2011 +0200
@@ -243,7 +243,7 @@
def id_command(command: Command)
{
- if (global_state().lookup_command(command.id).isEmpty) {
+ if (!global_state().defined_command(command.id)) {
global_state.change(_.define_command(command))
prover.get.define_command(command.id, Symbol.encode(command.source))
}
--- a/src/Pure/Thy/thy_header.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Aug 30 17:02:06 2011 +0200
@@ -119,6 +119,8 @@
Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
def norm_deps(f: String => String, g: String => String): Thy_Header =
- copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
+ copy(imports = imports.map(name => f(name)))
+ // FIXME
+ // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
}
--- a/src/Pure/Thy/thy_load.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala Tue Aug 30 17:02:06 2011 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/thy_load.scala
Author: Makarius
-Loading files that contribute to a theory.
+Primitives for loading theory files.
*/
package isabelle
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Aug 30 17:02:06 2011 +0200
@@ -17,6 +17,7 @@
"src/isabelle_markup.scala"
"src/isabelle_options.scala"
"src/isabelle_sidekick.scala"
+ "src/jedit_thy_load.scala"
"src/output_dockable.scala"
"src/plugin.scala"
"src/protocol_dockable.scala"
--- a/src/Tools/jEdit/src/document_view.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Tue Aug 30 17:02:06 2011 +0200
@@ -118,14 +118,17 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
+ val buffer_range = Text.Range(0, (model.buffer.getLength - 1) max 0)
Text.Perspective(
for {
i <- 0 until text_area.getVisibleLines
val start = text_area.getScreenLineStartOffset(i)
val stop = text_area.getScreenLineEndOffset(i)
if start >= 0 && stop >= 0
+ val range <- buffer_range.try_restrict(Text.Range(start, stop))
+ if !range.is_singularity
}
- yield Text.Range(start, stop))
+ yield range)
}
private def update_perspective = new TextAreaExtension
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Aug 30 17:02:06 2011 +0200
@@ -16,11 +16,21 @@
import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
-private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
+private class Internal_Hyperlink(name: String, start: Int, end: Int, line: Int, offset: Int)
extends AbstractHyperlink(start, end, line, "")
{
- override def click(view: View) {
- view.getTextArea.moveCaretPosition(def_offset)
+ override def click(view: View)
+ {
+ val text_area = view.getTextArea
+ if (Isabelle.buffer_name(view.getBuffer) == name)
+ text_area.moveCaretPosition(offset)
+ else
+ Isabelle.jedit_buffer(name) match {
+ case Some(buffer) =>
+ view.setBuffer(buffer)
+ text_area.moveCaretPosition(offset)
+ case None =>
+ }
}
}
@@ -60,21 +70,22 @@
(Position.File.unapply(props), Position.Line.unapply(props)) match {
case (Some(def_file), Some(def_line)) =>
new External_Hyperlink(begin, end, line, def_file, def_line)
- case _ =>
+ case _ if !snapshot.is_outdated =>
(props, props) match {
case (Position.Id(def_id), Position.Offset(def_offset)) =>
- snapshot.lookup_command(def_id) match {
- case Some(def_cmd) =>
- snapshot.node.command_start(def_cmd) match {
+ snapshot.state.find_command(snapshot.version, def_id) match {
+ case Some((def_name, def_node, def_cmd)) =>
+ def_node.command_start(def_cmd) match {
case Some(def_cmd_start) =>
- new Internal_Hyperlink(begin, end, line,
- snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
+ new Internal_Hyperlink(def_name, begin, end, line,
+ def_cmd_start + def_cmd.decode(def_offset))
case None => null
}
case None => null
}
case _ => null
}
+ case _ => null
}
}
markup match {
--- a/src/Tools/jEdit/src/isabelle_markup.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Aug 30 17:02:06 2011 +0200
@@ -23,7 +23,7 @@
def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
- val outdated_color = new Color(240, 240, 240)
+ val outdated_color = new Color(238, 227, 227)
val unfinished_color = new Color(255, 228, 225)
val light_color = new Color(240, 240, 240)
@@ -52,7 +52,7 @@
def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
{
- val state = snapshot.state(command)
+ val state = snapshot.command_state(command)
if (snapshot.is_outdated) Some(outdated_color)
else
Isar_Document.command_status(state.status) match {
@@ -64,7 +64,7 @@
def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
{
- val state = snapshot.state(command)
+ val state = snapshot.command_state(command)
if (snapshot.is_outdated) None
else
Isar_Document.command_status(state.status) match {
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 30 17:02:06 2011 +0200
@@ -152,7 +152,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
+ snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Tue Aug 30 17:02:06 2011 +0200
@@ -0,0 +1,68 @@
+/* Title: Tools/jEdit/src/plugin.scala
+ Author: Makarius
+
+Primitives for loading theory files, based on jEdit buffer content.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.io.File
+import javax.swing.text.Segment
+
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
+import org.gjt.sp.jedit.MiscUtilities
+
+
+class JEdit_Thy_Load extends Thy_Load
+{
+ /* loaded theories provided by prover */
+
+ private var loaded_theories: Set[String] = Set()
+
+ override def register_thy(thy_name: String)
+ {
+ synchronized { loaded_theories += thy_name }
+ }
+
+ override def is_loaded(thy_name: String): Boolean =
+ synchronized { loaded_theories.contains(thy_name) }
+
+
+ /* file-system operations */
+
+ override def append(master_dir: String, source_path: Path): String =
+ {
+ val path = source_path.expand
+ if (path.is_absolute) Isabelle_System.platform_path(path)
+ else {
+ val vfs = VFSManager.getVFSForPath(master_dir)
+ if (vfs.isInstanceOf[FileVFS])
+ MiscUtilities.resolveSymlinks(
+ vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+ else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+ }
+ }
+
+ override def check_thy(node_name: String): Thy_Header =
+ {
+ Swing_Thread.now {
+ Isabelle.jedit_buffer(node_name) match {
+ case Some(buffer) =>
+ Isabelle.buffer_lock(buffer) {
+ val text = new Segment
+ buffer.getText(0, buffer.getLength, text)
+ Some(Thy_Header.read(text))
+ }
+ case None => None
+ }
+ } getOrElse {
+ val file = new File(node_name) // FIXME load URL via jEdit VFS (!?)
+ if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+ Thy_Header.read(file)
+ }
+ }
+}
+
--- a/src/Tools/jEdit/src/output_dockable.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Aug 30 17:02:06 2011 +0200
@@ -86,7 +86,7 @@
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
val snapshot = doc_view.update_snapshot()
val filtered_results =
- snapshot.state(cmd).results.iterator.map(_._2) filter {
+ snapshot.command_state(cmd).results.iterator.map(_._2) filter {
case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable
case _ => true
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 30 16:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 30 17:02:06 2011 +0200
@@ -10,23 +10,20 @@
import isabelle._
import java.lang.System
-import java.io.{File, FileInputStream, IOException}
import java.awt.Font
import javax.swing.JOptionPane
-import javax.swing.text.Segment
import scala.collection.mutable
import scala.swing.ComboBox
import scala.util.Sorting
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
- Buffer, EditPane, MiscUtilities, ServiceManager, View}
+ Buffer, EditPane, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.util.Log
@@ -162,10 +159,27 @@
}
+ /* buffers */
+
+ def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+ Swing_Thread.now { buffer_lock(buffer) { body } }
+
+ def buffer_text(buffer: JEditBuffer): String =
+ buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+
+ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
+ def buffer_path(buffer: Buffer): (String, String) =
+ (buffer.getDirectory, buffer_name(buffer))
+
+
/* main jEdit components */
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
+ def jedit_buffer(name: String): Option[Buffer] =
+ jedit_buffers().find(buffer => buffer_name(buffer) == name)
+
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
@@ -183,17 +197,6 @@
finally { buffer.readUnlock() }
}
- def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
- Swing_Thread.now { buffer_lock(buffer) { body } }
-
- def buffer_text(buffer: JEditBuffer): String =
- buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
-
- def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
-
- def buffer_path(buffer: Buffer): (String, String) =
- (buffer.getDirectory, buffer_name(buffer))
-
/* document model and view */
@@ -347,52 +350,9 @@
class Plugin extends EBPlugin
{
- /* theory files via editor document model */
-
- val thy_load = new Thy_Load
- {
- private var loaded_theories: Set[String] = Set()
-
- def register_thy(thy_name: String)
- {
- synchronized { loaded_theories += thy_name }
- }
- def is_loaded(thy_name: String): Boolean =
- synchronized { loaded_theories.contains(thy_name) }
+ /* theory files */
- def append(master_dir: String, source_path: Path): String =
- {
- val path = source_path.expand
- if (path.is_absolute) Isabelle_System.platform_path(path)
- else {
- val vfs = VFSManager.getVFSForPath(master_dir)
- if (vfs.isInstanceOf[FileVFS])
- MiscUtilities.resolveSymlinks(
- vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
- else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
- }
- }
-
- def check_thy(node_name: String): Thy_Header =
- {
- Swing_Thread.now {
- Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
- case Some(buffer) =>
- Isabelle.buffer_lock(buffer) {
- val text = new Segment
- buffer.getText(0, buffer.getLength, text)
- Some(Thy_Header.read(text))
- }
- case None => None
- }
- } getOrElse {
- val file = new File(node_name) // FIXME load URL via jEdit VFS (!?)
- if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
- Thy_Header.read(file)
- }
- }
- }
-
+ val thy_load = new JEdit_Thy_Load
val thy_info = new Thy_Info(thy_load)
private lazy val delay_load =