# HG changeset patch
# User wenzelm
# Date 1309634659 -7200
# Node ID ea08ce1c314bdbd7dd8ff00ee896e0add64bd87d
# Parent  474745a899ea310ef0a2577d27f9fd26a399c814
tuned signature;

diff -r 474745a899ea -r ea08ce1c314b src/Pure/System/session.scala
--- 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
 
diff -r 474745a899ea -r ea08ce1c314b src/Tools/jEdit/src/document_model.scala
--- 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