src/Tools/jEdit/src/document_model.scala
changeset 44182 ecb51b457064
parent 44160 8848867501fb
child 44358 2a2df4de1bbe
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 13:48:26 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 15:59:26 2011 +0200
     1.3 @@ -62,9 +62,8 @@
     1.4  {
     1.5    /* pending text edits */
     1.6  
     1.7 -  def node_header(): Document.Node.Header =
     1.8 -    Document.Node.Header(master_dir,
     1.9 -      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
    1.10 +  def node_header(): Exn.Result[Thy_Header] =
    1.11 +    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
    1.12  
    1.13    private object pending_edits  // owned by Swing thread
    1.14    {
    1.15 @@ -78,14 +77,14 @@
    1.16          case Nil =>
    1.17          case edits =>
    1.18            pending.clear
    1.19 -          session.edit_node(node_name, node_header(), edits)
    1.20 +          session.edit_node(node_name, master_dir, node_header(), edits)
    1.21        }
    1.22      }
    1.23  
    1.24      def init()
    1.25      {
    1.26        flush()
    1.27 -      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
    1.28 +      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
    1.29      }
    1.30  
    1.31      private val delay_flush =