# HG changeset patch # User wenzelm # Date 1309714952 -7200 # Node ID e32de528b5ef33132f200d7e391855157c35cba0 # Parent 42b98a59ec302a1fe7506860c37412ac7dcde6f3 more explicit edit_node vs. init_node; some support for master_dir and header; diff -r 42b98a59ec30 -r e32de528b5ef src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sun Jul 03 15:10:17 2011 +0200 +++ b/src/Pure/System/session.scala Sun Jul 03 19:42:32 2011 +0200 @@ -145,13 +145,17 @@ def current_state(): Document.State = global_state.peek() private case object Interrupt_Prover - private case class Edit_Version(edits: List[Document.Edit_Text]) + private case class Edit_Node(thy_name: String, + header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit]) + private case class Init_Node(thy_name: String, + header: Exn.Result[Thy_Header.Header], text: String) private case class Start(timeout: Time, args: List[String]) var verbose: Boolean = false private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true) { + val this_actor = self var prover: Isabelle_Process with Isar_Document = null @@ -251,6 +255,21 @@ //}}} + def edit_version(edits: List[Document.Edit_Text]) + //{{{ + { + val previous = global_state.peek().history.tip.version + val syntax = current_syntax() + val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) } + val change = global_state.change_yield(_.extend_history(previous, edits, result)) + + change.version.map(_ => { + assignments.await { global_state.peek().is_assigned(previous.get_finished) } + this_actor ! change }) + } + //}}} + + /* main loop */ var finished = false @@ -259,27 +278,26 @@ case Interrupt_Prover => if (prover != null) prover.interrupt - case Edit_Version(edits) if prover != null => - val previous = global_state.peek().history.tip.version - val syntax = current_syntax() - val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) } - val change = global_state.change_yield(_.extend_history(previous, edits, result)) - - val this_actor = self - change.version.map(_ => { - assignments.await { global_state.peek().is_assigned(previous.get_finished) } - this_actor ! change }) - + case Edit_Node(thy_name, header, text_edits) if prover != null => + edit_version(List((thy_name, Some(text_edits)))) reply(()) - case change: Document.Change if prover != null => handle_change(change) + case Init_Node(thy_name, header, text) if prover != null => + // FIXME compare with existing node + edit_version(List( + (thy_name, None), + (thy_name, Some(List(Text.Edit.insert(0, text)))))) + reply(()) + + case change: Document.Change if prover != null => + handle_change(change) case result: Isabelle_Process.Result => handle_result(result) case Start(timeout, args) if prover == null => if (phase == Session.Inactive || phase == Session.Failed) { phase = Session.Startup - prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document + prover = new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document } case Stop => @@ -308,7 +326,15 @@ def interrupt() { session_actor ! Interrupt_Prover } - def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) } + def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit]) + { + session_actor !? Edit_Node(thy_name, header, edits) + } + + def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String) + { + session_actor !? Init_Node(thy_name, header, text) + } def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = global_state.peek().snapshot(name, pending_edits) diff -r 42b98a59ec30 -r e32de528b5ef src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sun Jul 03 15:10:17 2011 +0200 +++ b/src/Pure/Thy/thy_header.scala Sun Jul 03 19:42:32 2011 +0200 @@ -36,8 +36,10 @@ /* file name */ - val Thy_Path1 = new Regex("([^/]*)\\.thy") - val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy") + def thy_path(name: String): Path = Path.basic(name).ext("thy") + + private val Thy_Path1 = new Regex("([^/]*)\\.thy") + private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy") def split_thy_path(path: String): Option[(String, String)] = path match { @@ -108,4 +110,15 @@ try { read(reader).decode_permissive_utf8 } finally { reader.close } } + + + /* check */ + + def check(name: String, source: CharSequence): Header = + { + val header = read(source) + val name1 = header.name + if (name == name1) header + else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1)) + } } diff -r 42b98a59ec30 -r e32de528b5ef src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sun Jul 03 15:10:17 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sun Jul 03 19:42:32 2011 +0200 @@ -45,10 +45,10 @@ } } - def init(session: Session, buffer: Buffer, thy_name: String): Document_Model = + def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model = { exit(buffer) - val model = new Document_Model(session, buffer, thy_name) + val model = new Document_Model(session, buffer, master_dir, thy_name) buffer.setProperty(key, model) model.activate() model @@ -56,31 +56,36 @@ } -class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String) +class Document_Model(val session: Session, + val buffer: Buffer, val master_dir: String, val thy_name: String) { /* pending text edits */ + private def capture_header(): Exn.Result[Thy_Header.Header] = + Exn.capture { + session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength)) + } + private object pending_edits // owned by Swing thread { private val pending = new mutable.ListBuffer[Text.Edit] def snapshot(): List[Text.Edit] = pending.toList - def flush(more_edits: Option[List[Text.Edit]]*) + def flush() { Swing_Thread.require() - val edits = snapshot() - pending.clear - - val all_edits = - if (edits.isEmpty) more_edits.toList - else Some(edits) :: more_edits.toList - if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _))) + snapshot() match { + case Nil => + case edits => + pending.clear + session.edit_node(master_dir + "/" + thy_name, capture_header(), edits) + } } def init() { - Swing_Thread.require() - flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer))))) + flush() + session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer)) } private val delay_flush = @@ -100,7 +105,7 @@ def snapshot(): Document.Snapshot = { Swing_Thread.require() - session.snapshot(thy_name, pending_edits.snapshot()) + session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot()) } diff -r 42b98a59ec30 -r e32de528b5ef src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Jul 03 15:10:17 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sun Jul 03 19:42:32 2011 +0200 @@ -201,8 +201,8 @@ case None => // FIXME strip protocol prefix of URL Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match { - case Some((dir, thy_name)) => - Some(Document_Model.init(session, buffer, dir + "/" + thy_name)) + case Some((master_dir, thy_name)) => + Some(Document_Model.init(session, buffer, master_dir, thy_name)) case None => None } }