tuned signature;
authorwenzelm
Sat, 02 Jul 2011 21:24:19 +0200
changeset 44521ea08ce1c314b
parent 44520 474745a899ea
child 44522 ac886d096c11
tuned signature;
src/Pure/System/session.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/System/session.scala	Sat Jul 02 20:54:38 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Jul 02 21:24:19 2011 +0200
     1.3 @@ -116,6 +116,8 @@
     1.4  
     1.5    /** main protocol actor **/
     1.6  
     1.7 +  val thy_header = new Thy_Header(system.symbols)
     1.8 +
     1.9    @volatile private var syntax = new Outer_Syntax(system.symbols)
    1.10    def current_syntax(): Outer_Syntax = syntax
    1.11  
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jul 02 20:54:38 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jul 02 21:24:19 2011 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4  {
     2.5    /* pending text edits */
     2.6  
     2.7 -  object pending_edits  // owned by Swing thread
     2.8 +  private object pending_edits  // owned by Swing thread
     2.9    {
    2.10      private val pending = new mutable.ListBuffer[Text.Edit]
    2.11      def snapshot(): List[Text.Edit] = pending.toList