--- a/src/Pure/Isar/outer_syntax.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sat Mar 29 12:05:24 2014 +0100
@@ -57,13 +57,13 @@
def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
- def thy_load(span: List[Token]): Option[List[String]] =
+ def load(span: List[Token]): Option[List[String]] =
keywords.get(Command.name(span)) match {
case Some((Keyword.THY_LOAD, exts)) => Some(exts)
case _ => None
}
- val thy_load_commands: List[(String, List[String])] =
+ val load_commands: List[(String, List[String])] =
(for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
--- a/src/Pure/PIDE/document.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Pure/PIDE/document.scala Sat Mar 29 12:05:24 2014 +0100
@@ -189,7 +189,7 @@
final class Commands private(val commands: Linear_Set[Command])
{
- lazy val thy_load_commands: List[Command] =
+ lazy val load_commands: List[Command] =
commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -244,7 +244,7 @@
perspective.overlays == other_perspective.overlays
def commands: Linear_Set[Command] = _commands.commands
- def thy_load_commands: List[Command] = _commands.thy_load_commands
+ def load_commands: List[Command] = _commands.load_commands
def update_commands(new_commands: Linear_Set[Command]): Node =
if (new_commands eq _commands.commands) this
@@ -290,10 +290,10 @@
def entries: Iterator[(Node.Name, Node)] =
graph.entries.map({ case (name, (node, _)) => (name, node) })
- def thy_load_commands(file_name: Node.Name): List[Command] =
+ def load_commands(file_name: Node.Name): List[Command] =
(for {
(_, node) <- entries
- cmd <- node.thy_load_commands.iterator
+ cmd <- node.load_commands.iterator
name <- cmd.blobs_names.iterator
if name == file_name
} yield cmd).toList
@@ -421,7 +421,7 @@
val node_name: Node.Name
val node: Node
- val thy_load_commands: List[Command]
+ val load_commands: List[Command]
def is_loaded: Boolean
def eq_content(other: Snapshot): Boolean
@@ -694,11 +694,11 @@
val node_name = name
val node = version.nodes(name)
- val thy_load_commands: List[Command] =
+ val load_commands: List[Command] =
if (node_name.is_theory) Nil
- else version.nodes.thy_load_commands(node_name)
+ else version.nodes.load_commands(node_name)
- val is_loaded: Boolean = node_name.is_theory || !thy_load_commands.isEmpty
+ val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
def eq_content(other: Snapshot): Boolean =
{
@@ -713,8 +713,8 @@
!is_outdated && !other.is_outdated &&
node.commands.size == other.node.commands.size &&
(node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
- thy_load_commands.length == other.thy_load_commands.length &&
- (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
+ load_commands.length == other.load_commands.length &&
+ (load_commands zip other.load_commands).forall(eq_commands)
}
@@ -729,7 +729,7 @@
{
val former_range = revert(range)
val (file_name, command_range_iterator) =
- thy_load_commands match {
+ load_commands match {
case command :: _ => (node_name.node, Iterator((command, 0)))
case _ => ("", node.command_range(former_range))
}
--- a/src/Pure/PIDE/markup_tree.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Sat Mar 29 12:05:24 2014 +0100
@@ -118,7 +118,7 @@
private def overlapping(range: Text.Range): Branches.T =
if (branches.isEmpty ||
- (range.contains(branches.firstKey.start) && range.contains(branches.lastKey.stop)))
+ (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop))
branches
else {
val start = Text.Range(range.start)
--- a/src/Pure/PIDE/resources.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Mar 29 12:05:24 2014 +0100
@@ -51,7 +51,7 @@
/* theory files */
def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
- syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+ syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
def body_files(syntax: Outer_Syntax, text: String): List[String] =
{
@@ -91,15 +91,15 @@
with_thy_text(name, check_thy_text(name, _))
- /* theory text edits */
+ /* document changes */
- def text_edits(
- reparse_limit: Int,
- previous: Document.Version,
- doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
- Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+ def parse_change(
+ reparse_limit: Int,
+ previous: Document.Version,
+ doc_blobs: Document.Blobs,
+ edits: List[Document.Edit_Text]): Session.Change =
+ Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
- def syntax_changed() { }
+ def commit(change: Session.Change) { }
}
--- a/src/Pure/PIDE/session.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Pure/PIDE/session.scala Sat Mar 29 12:05:24 2014 +0100
@@ -18,6 +18,17 @@
object Session
{
+ /* change */
+
+ sealed case class Change(
+ previous: Document.Version,
+ doc_blobs: Document.Blobs,
+ syntax_changed: Boolean,
+ deps_changed: Boolean,
+ doc_edits: List[Document.Edit_Command],
+ version: Document.Version)
+
+
/* events */
//{{{
@@ -179,12 +190,12 @@
case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
val prev = previous.get_finished
- val (syntax_changed, doc_edits, version) =
- Timing.timeit("text_edits", timing) {
- resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
+ val change =
+ Timing.timeit("parse_change", timing) {
+ resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
}
- version_result.fulfill(version)
- sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
+ version_result.fulfill(change.version)
+ sender ! change
case bad => System.err.println("change_parser: ignoring bad message " + bad)
}
@@ -249,12 +260,6 @@
private case class Start(args: List[String])
private case class Cancel_Exec(exec_id: Document_ID.Exec)
- private case class Change(
- doc_blobs: Document.Blobs,
- syntax_changed: Boolean,
- doc_edits: List[Document.Edit_Command],
- previous: Document.Version,
- version: Document.Version)
private case class Protocol_Command(name: String, args: List[String])
private case class Messages(msgs: List[Isabelle_Process.Message])
private case class Update_Options(options: Options)
@@ -367,18 +372,16 @@
/* resulting changes */
- def handle_change(change: Change)
+ def handle_change(change: Session.Change)
//{{{
{
- val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
-
def id_command(command: Command)
{
for {
digest <- command.blobs_digests
if !global_state().defined_blob(digest)
} {
- doc_blobs.get(digest) match {
+ change.doc_blobs.get(digest) match {
case Some(blob) =>
global_state >> (_.define_blob(digest))
prover.get.define_blob(blob)
@@ -392,16 +395,15 @@
prover.get.define_command(command)
}
}
- doc_edits foreach {
+ change.doc_edits foreach {
case (_, edit) =>
edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
}
- val assignment = global_state().the_assignment(previous).check_finished
- global_state >> (_.define_version(version, assignment))
- prover.get.update(previous.id, version.id, doc_edits)
-
- if (syntax_changed) resources.syntax_changed()
+ val assignment = global_state().the_assignment(change.previous).check_finished
+ global_state >> (_.define_version(change.version, assignment))
+ prover.get.update(change.previous.id, change.version.id, change.doc_edits)
+ resources.commit(change)
}
//}}}
@@ -556,11 +558,11 @@
all_messages.event(output)
}
- case change: Change
+ case change: Session.Change
if prover.isDefined && global_state().is_assigned(change.previous) =>
handle_change(change)
- case bad if !bad.isInstanceOf[Change] =>
+ case bad if !bad.isInstanceOf[Session.Change] =>
System.err.println("session_actor: ignoring bad message " + bad)
}
}
--- a/src/Pure/Thy/thy_syntax.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Sat Mar 29 12:05:24 2014 +0100
@@ -156,7 +156,8 @@
base_syntax: Outer_Syntax,
previous: Document.Version,
edits: List[Document.Edit_Text]):
- ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
+ (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
+ List[Document.Edit_Command]) =
{
var updated_imports = false
var updated_keywords = false
@@ -178,7 +179,7 @@
case _ =>
}
- val syntax =
+ val (syntax, syntax_changed) =
if (previous.is_init || updated_keywords) {
val syntax =
(base_syntax /: nodes.entries) {
@@ -193,7 +194,7 @@
nodes.descendants(doc_edits.iterator.map(_._1).toList)
else Nil
- (syntax, reparse, nodes, doc_edits.toList)
+ (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
}
@@ -245,7 +246,7 @@
}
def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
- syntax.thy_load(span) match {
+ syntax.load(span) match {
case Some(exts) =>
find_file(span) match {
case Some(file) =>
@@ -431,58 +432,59 @@
}
}
- def text_edits(
+ def parse_change(
resources: Resources,
reparse_limit: Int,
previous: Document.Version,
doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text])
- : (Boolean, List[Document.Edit_Command], Document.Version) =
+ edits: List[Document.Edit_Text]): Session.Change =
{
- val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
+ val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
header_edits(resources.base_syntax, previous, edits)
- if (edits.isEmpty)
- (false, Nil, Document.Version.make(syntax, previous.nodes))
- else {
- val reparse =
- (reparse0 /: nodes0.entries)({
- case (reparse, (name, node)) =>
- if (node.thy_load_commands.exists(_.blobs_changed(doc_blobs)))
- name :: reparse
- else reparse
- })
- val reparse_set = reparse.toSet
+ val (doc_edits, version) =
+ if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
+ else {
+ val reparse =
+ (reparse0 /: nodes0.entries)({
+ case (reparse, (name, node)) =>
+ if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
+ name :: reparse
+ else reparse
+ })
+ val reparse_set = reparse.toSet
- var nodes = nodes0
- val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+ var nodes = nodes0
+ val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
- val node_edits =
- (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
- .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
+ val node_edits =
+ (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+ .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
- node_edits foreach {
- case (name, edits) =>
- val node = nodes(name)
- val commands = node.commands
+ node_edits foreach {
+ case (name, edits) =>
+ val node = nodes(name)
+ val commands = node.commands
- val node1 =
- if (reparse_set(name) && !commands.isEmpty)
- node.update_commands(
- reparse_spans(resources, syntax, doc_blobs,
- name, commands, commands.head, commands.last))
- else node
- val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
+ val node1 =
+ if (reparse_set(name) && !commands.isEmpty)
+ node.update_commands(
+ reparse_spans(resources, syntax, doc_blobs,
+ name, commands, commands.head, commands.last))
+ else node
+ val node2 =
+ (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
- if (!(node.same_perspective(node2.perspective)))
- doc_edits += (name -> node2.perspective)
+ if (!(node.same_perspective(node2.perspective)))
+ doc_edits += (name -> node2.perspective)
- doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+ doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
- nodes += (name -> node2)
+ nodes += (name -> node2)
+ }
+ (doc_edits.toList, Document.Version.make(syntax, nodes))
}
- (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
- }
+ Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
}
}
--- a/src/Tools/jEdit/src/document_model.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sat Mar 29 12:05:24 2014 +0100
@@ -115,9 +115,9 @@
}
else Nil
- val thy_load_ranges =
+ val load_ranges =
for {
- cmd <- snapshot.node.thy_load_commands
+ cmd <- snapshot.node.load_commands
blob_name <- cmd.blobs_names
blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
@@ -125,11 +125,11 @@
range = snapshot.convert(cmd.proper_range + start)
} yield range
- val reparse = snapshot.node.thy_load_commands.exists(_.blobs_changed(doc_blobs))
+ val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
(reparse,
Document.Node.Perspective(node_required,
- Text.Perspective(document_view_ranges ::: thy_load_ranges),
+ Text.Perspective(document_view_ranges ::: load_ranges),
PIDE.editor.node_overlays(node_name)))
}
else (false, empty_perspective)
--- a/src/Tools/jEdit/src/document_view.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sat Mar 29 12:05:24 2014 +0100
@@ -210,17 +210,17 @@
if (model.buffer == text_area.getBuffer) {
val snapshot = model.snapshot()
- val thy_load_changed =
- snapshot.thy_load_commands.exists(changed.commands.contains)
+ val load_changed =
+ snapshot.load_commands.exists(changed.commands.contains)
- if (changed.assignment || thy_load_changed ||
+ if (changed.assignment || load_changed ||
(changed.nodes.contains(model.node_name) &&
changed.commands.exists(snapshot.node.commands.contains)))
Swing_Thread.later { overview.delay_repaint.invoke() }
val visible_lines = text_area.getVisibleLines
if (visible_lines > 0) {
- if (changed.assignment || thy_load_changed)
+ if (changed.assignment || load_changed)
text_area.invalidateScreenLineRange(0, visible_lines)
else {
val visible_range = JEdit_Lib.visible_range(text_area).get
--- a/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 29 12:05:24 2014 +0100
@@ -85,7 +85,7 @@
case _ =>
PIDE.document_model(buffer) match {
case Some(model) if !model.is_theory =>
- snapshot.version.nodes.thy_load_commands(model.node_name) match {
+ snapshot.version.nodes.load_commands(model.node_name) match {
case cmd :: _ => Some(cmd)
case Nil => None
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Mar 29 12:05:24 2014 +0100
@@ -117,7 +117,10 @@
/* theory text edits */
- override def syntax_changed(): Unit =
- Swing_Thread.later { jEdit.propertiesChanged() }
+ override def commit(change: Session.Change)
+ {
+ if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
+ if (change.deps_changed) PIDE.deps_changed()
+ }
}
--- a/src/Tools/jEdit/src/plugin.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 29 12:05:24 2014 +0100
@@ -39,6 +39,7 @@
@volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
def options_changed() { plugin.options_changed() }
+ def deps_changed() { plugin.deps_changed() }
def resources(): JEdit_Resources =
session.resources.asInstanceOf[JEdit_Resources]
@@ -168,13 +169,19 @@
class Plugin extends EBPlugin
{
- /* options */
+ /* global changes */
- def options_changed() {
+ def options_changed()
+ {
PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
Swing_Thread.later { delay_load.invoke() }
}
+ def deps_changed()
+ {
+ Swing_Thread.later { delay_load.invoke() }
+ }
+
/* theory files */
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 29 11:41:39 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 29 12:05:24 2014 +0100
@@ -10,7 +10,7 @@
import isabelle._
-import java.awt.{Graphics2D, Shape, Color, Point, Toolkit}
+import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor}
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import java.awt.font.TextAttribute
@@ -100,7 +100,9 @@
/* active areas within the text */
- private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]])
+ private class Active_Area[A](
+ rendering: Rendering => Text.Range => Option[Text.Info[A]],
+ cursor: Option[Int])
{
private var the_text_info: Option[(String, Text.Info[A])] = None
@@ -115,6 +117,12 @@
new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
if (new_text_info != old_text_info) {
+ if (cursor.isDefined) {
+ if (new_text_info.isDefined)
+ text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
+ else
+ text_area.getPainter.resetCursor
+ }
for {
r0 <- JEdit_Lib.visible_range(text_area)
opt <- List(old_text_info, new_text_info)
@@ -133,10 +141,13 @@
// owned by Swing thread
- private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
+ private val highlight_area =
+ new Active_Area[Color]((r: Rendering) => r.highlight _, None)
private val hyperlink_area =
- new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
- private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
+ new Active_Area[PIDE.editor.Hyperlink](
+ (r: Rendering) => r.hyperlink _, Some(Cursor.HAND_CURSOR))
+ private val active_area =
+ new Active_Area[XML.Elem]((r: Rendering) => r.active _, Some(Cursor.DEFAULT_CURSOR))
private val active_areas =
List((highlight_area, true), (hyperlink_area, true), (active_area, false))