src/Pure/System/session.scala
changeset 44182 ecb51b457064
parent 44163 32e0c150c010
child 44183 1de22a7b2a82
     1.1 --- a/src/Pure/System/session.scala	Sat Aug 13 13:48:26 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Aug 13 15:59:26 2011 +0200
     1.3 @@ -164,8 +164,10 @@
     1.4  
     1.5    private case class Start(timeout: Time, args: List[String])
     1.6    private case object Interrupt
     1.7 -  private case class Init_Node(name: String, header: Document.Node.Header, text: String)
     1.8 -  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
     1.9 +  private case class Init_Node(
    1.10 +    name: String, master_dir: String, header: Document.Node_Header, text: String)
    1.11 +  private case class Edit_Node(
    1.12 +    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
    1.13    private case class Change_Node(
    1.14      name: String,
    1.15      doc_edits: List[Document.Edit_Command],
    1.16 @@ -180,15 +182,15 @@
    1.17  
    1.18      /* incoming edits */
    1.19  
    1.20 -    def handle_edits(name: String,
    1.21 -        header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
    1.22 +    def handle_edits(name: String, master_dir: String,
    1.23 +        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
    1.24      //{{{
    1.25      {
    1.26        val syntax = current_syntax()
    1.27        val previous = global_state().history.tip.version
    1.28 -      val doc_edits =
    1.29 -        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
    1.30 -          edits.map(edit => (name, edit))
    1.31 +      val norm_header =
    1.32 +        Document.Node.norm_header[Text.Edit](file_store.append(master_dir, _), header)
    1.33 +      val doc_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    1.34        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    1.35        val change =
    1.36          global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
    1.37 @@ -325,14 +327,14 @@
    1.38          case Interrupt if prover.isDefined =>
    1.39            prover.get.interrupt
    1.40  
    1.41 -        case Init_Node(name, header, text) if prover.isDefined =>
    1.42 +        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
    1.43            // FIXME compare with existing node
    1.44 -          handle_edits(name, header,
    1.45 +          handle_edits(name, master_dir, header,
    1.46              List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
    1.47            reply(())
    1.48  
    1.49 -        case Edit_Node(name, header, text_edits) if prover.isDefined =>
    1.50 -          handle_edits(name, header, List(Document.Node.Edits(text_edits)))
    1.51 +        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
    1.52 +          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
    1.53            reply(())
    1.54  
    1.55          case change: Change_Node if prover.isDefined =>
    1.56 @@ -360,9 +362,9 @@
    1.57  
    1.58    def interrupt() { session_actor ! Interrupt }
    1.59  
    1.60 -  def init_node(name: String, header: Document.Node.Header, text: String)
    1.61 -  { session_actor !? Init_Node(name, header, text) }
    1.62 +  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
    1.63 +  { session_actor !? Init_Node(name, master_dir, header, text) }
    1.64  
    1.65 -  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
    1.66 -  { session_actor !? Edit_Node(name, header, edits) }
    1.67 +  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
    1.68 +  { session_actor !? Edit_Node(name, master_dir, header, edits) }
    1.69  }