--- a/src/Tools/jEdit/src/document_model.scala Wed Jul 31 18:08:12 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 31 19:59:14 2013 +0200
@@ -79,15 +79,15 @@
/* perspective */
- var required_node = false
+ var node_required = false
def node_perspective(): Document.Node.Perspective_Text =
{
Swing_Thread.require()
val perspective =
- if (PIDE.continuous_checking) {
- (required_node, Text.Perspective(
+ if (Isabelle.continuous_checking) {
+ (node_required, Text.Perspective(
for {
doc_view <- PIDE.document_views(buffer)
range <- doc_view.perspective().ranges
@@ -104,6 +104,7 @@
def init_edits(): List[Document.Edit_Text] =
{
Swing_Thread.require()
+
val header = node_header()
val text = JEdit_Lib.buffer_text(buffer)
val perspective = node_perspective()
@@ -118,6 +119,7 @@
: List[Document.Edit_Text] =
{
Swing_Thread.require()
+
val header = node_header()
List(session.header_edit(name, header),
@@ -132,7 +134,7 @@
{
private val pending = new mutable.ListBuffer[Text.Edit]
private var last_perspective: Document.Node.Perspective_Text =
- Document.Node.Perspective(required_node, Text.Perspective.empty)
+ Document.Node.Perspective(node_required, Text.Perspective.empty)
def snapshot(): List[Text.Edit] = pending.toList