--- a/src/Pure/System/session.scala Sat Jul 02 20:54:38 2011 +0200
+++ b/src/Pure/System/session.scala Sat Jul 02 21:24:19 2011 +0200
@@ -116,6 +116,8 @@
/** main protocol actor **/
+ val thy_header = new Thy_Header(system.symbols)
+
@volatile private var syntax = new Outer_Syntax(system.symbols)
def current_syntax(): Outer_Syntax = syntax
--- a/src/Tools/jEdit/src/document_model.scala Sat Jul 02 20:54:38 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sat Jul 02 21:24:19 2011 +0200
@@ -60,7 +60,7 @@
{
/* pending text edits */
- object pending_edits // owned by Swing thread
+ private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
def snapshot(): List[Text.Edit] = pending.toList