1.1 --- a/src/Pure/System/session.scala	Sun Jul 03 15:10:17 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Jul 03 19:42:32 2011 +0200
     1.3 @@ -145,13 +145,17 @@
     1.4    def current_state(): Document.State = global_state.peek()
     1.5  
     1.6    private case object Interrupt_Prover
     1.7 -  private case class Edit_Version(edits: List[Document.Edit_Text])
     1.8 +  private case class Edit_Node(thy_name: String,
     1.9 +    header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
    1.10 +  private case class Init_Node(thy_name: String,
    1.11 +    header: Exn.Result[Thy_Header.Header], text: String)
    1.12    private case class Start(timeout: Time, args: List[String])
    1.13  
    1.14    var verbose: Boolean = false
    1.15  
    1.16    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    1.17    {
    1.18 +    val this_actor = self
    1.19      var prover: Isabelle_Process with Isar_Document = null
    1.20  
    1.21  
    1.22 @@ -251,6 +255,21 @@
    1.23      //}}}
    1.24  
    1.25  
    1.26 +    def edit_version(edits: List[Document.Edit_Text])
    1.27 +    //{{{
    1.28 +    {
    1.29 +      val previous = global_state.peek().history.tip.version
    1.30 +      val syntax = current_syntax()
    1.31 +      val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
    1.32 +      val change = global_state.change_yield(_.extend_history(previous, edits, result))
    1.33 +
    1.34 +      change.version.map(_ => {
    1.35 +        assignments.await { global_state.peek().is_assigned(previous.get_finished) }
    1.36 +        this_actor ! change })
    1.37 +    }
    1.38 +    //}}}
    1.39 +
    1.40 +
    1.41      /* main loop */
    1.42  
    1.43      var finished = false
    1.44 @@ -259,27 +278,26 @@
    1.45          case Interrupt_Prover =>
    1.46            if (prover != null) prover.interrupt
    1.47  
    1.48 -        case Edit_Version(edits) if prover != null =>
    1.49 -          val previous = global_state.peek().history.tip.version
    1.50 -          val syntax = current_syntax()
    1.51 -          val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
    1.52 -          val change = global_state.change_yield(_.extend_history(previous, edits, result))
    1.53 -
    1.54 -          val this_actor = self
    1.55 -          change.version.map(_ => {
    1.56 -            assignments.await { global_state.peek().is_assigned(previous.get_finished) }
    1.57 -            this_actor ! change })
    1.58 -
    1.59 +        case Edit_Node(thy_name, header, text_edits) if prover != null =>
    1.60 +          edit_version(List((thy_name, Some(text_edits))))
    1.61            reply(())
    1.62  
    1.63 -        case change: Document.Change if prover != null => handle_change(change)
    1.64 +        case Init_Node(thy_name, header, text) if prover != null =>
    1.65 +          // FIXME compare with existing node
    1.66 +          edit_version(List(
    1.67 +            (thy_name, None),
    1.68 +            (thy_name, Some(List(Text.Edit.insert(0, text))))))
    1.69 +          reply(())
    1.70 +
    1.71 +        case change: Document.Change if prover != null =>
    1.72 +          handle_change(change)
    1.73  
    1.74          case result: Isabelle_Process.Result => handle_result(result)
    1.75  
    1.76          case Start(timeout, args) if prover == null =>
    1.77            if (phase == Session.Inactive || phase == Session.Failed) {
    1.78              phase = Session.Startup
    1.79 -            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
    1.80 +            prover = new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document
    1.81            }
    1.82  
    1.83          case Stop =>
    1.84 @@ -308,7 +326,15 @@
    1.85  
    1.86    def interrupt() { session_actor ! Interrupt_Prover }
    1.87  
    1.88 -  def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
    1.89 +  def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
    1.90 +  {
    1.91 +    session_actor !? Edit_Node(thy_name, header, edits)
    1.92 +  }
    1.93 +
    1.94 +  def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
    1.95 +  {
    1.96 +    session_actor !? Init_Node(thy_name, header, text)
    1.97 +  }
    1.98  
    1.99    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   1.100      global_state.peek().snapshot(name, pending_edits)

     2.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 03 15:10:17 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 03 19:42:32 2011 +0200
     2.3 @@ -36,8 +36,10 @@
     2.4  
     2.5    /* file name */
     2.6  
     2.7 -  val Thy_Path1 = new Regex("([^/]*)\\.thy")
     2.8 -  val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
     2.9 +  def thy_path(name: String): Path = Path.basic(name).ext("thy")
    2.10 +
    2.11 +  private val Thy_Path1 = new Regex("([^/]*)\\.thy")
    2.12 +  private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
    2.13  
    2.14    def split_thy_path(path: String): Option[(String, String)] =
    2.15      path match {
    2.16 @@ -108,4 +110,15 @@
    2.17      try { read(reader).decode_permissive_utf8 }
    2.18      finally { reader.close }
    2.19    }
    2.20 +
    2.21 +
    2.22 +  /* check */
    2.23 +
    2.24 +  def check(name: String, source: CharSequence): Header =
    2.25 +  {
    2.26 +    val header = read(source)
    2.27 +    val name1 = header.name
    2.28 +    if (name == name1) header
    2.29 +    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
    2.30 +  }
    2.31  }

     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Jul 03 15:10:17 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Jul 03 19:42:32 2011 +0200
     3.3 @@ -45,10 +45,10 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
     3.8 +  def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
     3.9    {
    3.10      exit(buffer)
    3.11 -    val model = new Document_Model(session, buffer, thy_name)
    3.12 +    val model = new Document_Model(session, buffer, master_dir, thy_name)
    3.13      buffer.setProperty(key, model)
    3.14      model.activate()
    3.15      model
    3.16 @@ -56,31 +56,36 @@
    3.17  }
    3.18  
    3.19  
    3.20 -class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
    3.21 +class Document_Model(val session: Session,
    3.22 +  val buffer: Buffer, val master_dir: String, val thy_name: String)
    3.23  {
    3.24    /* pending text edits */
    3.25  
    3.26 +  private def capture_header(): Exn.Result[Thy_Header.Header] =
    3.27 +    Exn.capture {
    3.28 +      session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength))
    3.29 +    }
    3.30 +
    3.31    private object pending_edits  // owned by Swing thread
    3.32    {
    3.33      private val pending = new mutable.ListBuffer[Text.Edit]
    3.34      def snapshot(): List[Text.Edit] = pending.toList
    3.35  
    3.36 -    def flush(more_edits: Option[List[Text.Edit]]*)
    3.37 +    def flush()
    3.38      {
    3.39        Swing_Thread.require()
    3.40 -      val edits = snapshot()
    3.41 -      pending.clear
    3.42 -
    3.43 -      val all_edits =
    3.44 -        if (edits.isEmpty) more_edits.toList
    3.45 -        else Some(edits) :: more_edits.toList
    3.46 -      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
    3.47 +      snapshot() match {
    3.48 +        case Nil =>
    3.49 +        case edits =>
    3.50 +          pending.clear
    3.51 +          session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
    3.52 +      }
    3.53      }
    3.54  
    3.55      def init()
    3.56      {
    3.57 -      Swing_Thread.require()
    3.58 -      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
    3.59 +      flush()
    3.60 +      session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
    3.61      }
    3.62  
    3.63      private val delay_flush =
    3.64 @@ -100,7 +105,7 @@
    3.65    def snapshot(): Document.Snapshot =
    3.66    {
    3.67      Swing_Thread.require()
    3.68 -    session.snapshot(thy_name, pending_edits.snapshot())
    3.69 +    session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
    3.70    }
    3.71  
    3.72  

     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Jul 03 15:10:17 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Jul 03 19:42:32 2011 +0200
     4.3 @@ -201,8 +201,8 @@
     4.4            case None =>
     4.5              // FIXME strip protocol prefix of URL
     4.6              Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
     4.7 -              case Some((dir, thy_name)) =>
     4.8 -                Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
     4.9 +              case Some((master_dir, thy_name)) =>
    4.10 +                Some(Document_Model.init(session, buffer, master_dir, thy_name))
    4.11                case None => None
    4.12              }
    4.13          }