# HG changeset patch # User wenzelm # Date 1309791298 -7200 # Node ID 67d82d94a0765ee60aaaad689683fb2bd3590ad8 # Parent 0d96ec6ec33b6248f5d6d58210b4830aca38725d# Parent dcd0b667f73d607d2c67cc47533c2cc0a0212b1c merged diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/General/path.scala Mon Jul 04 16:54:58 2011 +0200 @@ -19,7 +19,7 @@ private case object Parent extends Elem private def err_elem(msg: String, s: String): Nothing = - error (msg + " path element specification: " + Library.quote(s)) + error (msg + " path element specification: " + quote(s)) private def check_elem(s: String): String = if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) @@ -27,7 +27,7 @@ s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match { case Nil => s case bads => - err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s) + err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s) } private def root_elem(s: String): Elem = Root(check_elem(s)) @@ -114,7 +114,7 @@ case _ => elems.map(Path.implode_elem).reverse.mkString("/") } - override def toString: String = Library.quote(implode) + override def toString: String = quote(implode) /* base element */ diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/General/yxml.scala Mon Jul 04 16:54:58 2011 +0200 @@ -144,12 +144,12 @@ def parse_body_failsafe(source: CharSequence): XML.Body = { try { parse_body(source) } - catch { case _: RuntimeException => List(markup_failsafe(source)) } + catch { case ERROR(_) => List(markup_failsafe(source)) } } def parse_failsafe(source: CharSequence): XML.Tree = { try { parse(source) } - catch { case _: RuntimeException => markup_failsafe(source) } + catch { case ERROR(_) => markup_failsafe(source) } } } diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/PIDE/document.ML Mon Jul 04 16:54:58 2011 +0200 @@ -80,10 +80,10 @@ NONE => entries | SOME next => Entries.update (next, NONE) entries); -fun edit_node (hook, SOME id2) (Node entries) = - Node (Entries.insert_after hook (id2, NONE) entries) - | edit_node (hook, NONE) (Node entries) = - Node (entries |> Entries.delete_after hook |> reset_after hook); +fun edit_node (id, SOME id2) (Node entries) = + Node (Entries.insert_after id (id2, NONE) entries) + | edit_node (id, NONE) (Node entries) = + Node (entries |> Entries.delete_after id |> reset_after id); (* version operations *) diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/PIDE/text.scala Mon Jul 04 16:54:58 2011 +0200 @@ -46,7 +46,7 @@ def try_restrict(that: Range): Option[Range] = try { Some (restrict(that)) } - catch { case _: RuntimeException => None } + catch { case ERROR(_) => None } } @@ -57,7 +57,7 @@ def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) def try_restrict(r: Text.Range): Option[Info[A]] = try { Some(Info(range.restrict(r), info)) } - catch { case _: RuntimeException => None } + catch { case ERROR(_) => None } } diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/System/cygwin.scala --- a/src/Pure/System/cygwin.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/System/cygwin.scala Mon Jul 04 16:54:58 2011 +0200 @@ -115,7 +115,7 @@ try { Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe) } - catch { case _: RuntimeException => error("Failed to download Cygwin setup program") } + catch { case ERROR(_) => error("Failed to download Cygwin setup program") } val (_, rc) = Standard_System.raw_exec(root, null, true, setup_exe.toString, "-R", root.toString, "-l", download.toString, diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/System/gui_setup.scala --- a/src/Pure/System/gui_setup.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/System/gui_setup.scala Mon Jul 04 16:54:58 2011 +0200 @@ -51,9 +51,7 @@ if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n") text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n") text.append("Isabelle java: " + isabelle_system.this_java() + "\n") - } catch { - case e: RuntimeException => text.append(e.getMessage + "\n") - } + } catch { case ERROR(msg) => text.append(msg + "\n") } // reactions listenTo(ok) diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/System/session.scala Mon Jul 04 16:54:58 2011 +0200 @@ -2,7 +2,7 @@ Author: Makarius Options: :folding=explicit:collapseFolds=1: -Isabelle session, potentially with running prover. +Main Isabelle/Scala session, potentially with running prover process. */ package isabelle @@ -16,6 +16,14 @@ object Session { + /* abstract file store */ + + abstract class File_Store + { + def read(path: Path): String + } + + /* events */ case object Global_Settings @@ -32,7 +40,7 @@ } -class Session(val system: Isabelle_System) +class Session(val system: Isabelle_System, val file_store: Session.File_Store) { /* real time parameters */ // FIXME properties or settings (!?) @@ -116,6 +124,8 @@ /** main protocol actor **/ + /* global state */ + @volatile private var syntax = new Outer_Syntax(system.symbols) def current_syntax(): Outer_Syntax = syntax @@ -134,15 +144,41 @@ private val global_state = new Volatile(Document.State.init) def current_state(): Document.State = global_state.peek() + + /* theory files */ + + val thy_header = new Thy_Header(system.symbols) + + val thy_load = new Thy_Load + { + override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) = + { + val file = system.platform_file(dir + Thy_Header.thy_path(name)) + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) + val text = Standard_System.read_file(file) + val header = thy_header.read(text) + (text, header) + } + } + + val thy_info = new Thy_Info(thy_load) + + + /* actor messages */ + 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) { - var prover: Isabelle_Process with Isar_Document = null + val this_actor = self + var prover: Option[Isabelle_Process with Isar_Document] = None /* document changes */ @@ -174,7 +210,8 @@ case Some(command) => if (global_state.peek().lookup_command(command.id).isEmpty) { global_state.change(_.define_command(command)) - prover.define_command(command.id, system.symbols.encode(command.source)) + prover.get. + define_command(command.id, system.symbols.encode(command.source)) } Some(command.id) } @@ -183,7 +220,7 @@ (name -> Some(ids)) } global_state.change(_.define_version(version, former_assignment)) - prover.edit_version(previous.id, version.id, id_edits) + prover.get.edit_version(previous.id, version.id, id_edits) } //}}} @@ -241,47 +278,63 @@ //}}} + 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 while (!finished) { receive { case Interrupt_Prover => - if (prover != null) prover.interrupt + prover.map(_.interrupt) - case Edit_Version(edits) if prover != null => - val previous = global_state.peek().history.tip.version - val result = Future.fork { Thy_Syntax.text_edits(Session.this, 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.isDefined => + 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.isDefined => + // 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.isDefined => + handle_change(change) case result: Isabelle_Process.Result => handle_result(result) - case Start(timeout, args) if prover == null => + case Start(timeout, args) if prover.isEmpty => if (phase == Session.Inactive || phase == Session.Failed) { phase = Session.Startup - prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document + prover = + Some(new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document) } case Stop => if (phase == Session.Ready) { global_state.change(_ => Document.State.init) // FIXME event bus!? phase = Session.Shutdown - prover.terminate + prover.get.terminate phase = Session.Inactive } finished = true reply(()) - case bad if prover != null => + case bad if prover.isDefined => System.err.println("session_actor: ignoring bad message " + bad) } } @@ -297,7 +350,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 0d96ec6ec33b -r 67d82d94a076 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/Thy/thy_header.scala Mon Jul 04 16:54:58 2011 +0200 @@ -9,7 +9,7 @@ import scala.annotation.tailrec import scala.collection.mutable -import scala.util.parsing.input.Reader +import scala.util.parsing.input.{Reader, CharSequenceReader} import scala.util.matching.Regex import java.io.File @@ -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 { @@ -99,10 +101,24 @@ } } + def read(source: CharSequence): Header = + read(new CharSequenceReader(source)) + def read(file: File): Header = { val reader = Scan.byte_reader(file) 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 " + quote(name1)) + } } diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Jul 04 16:54:58 2011 +0200 @@ -34,10 +34,11 @@ datatype action = Update | Remove; local - val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list); + val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list); in - fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f)); - fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks); + fun add_hook f = Synchronized.change hooks (cons f); + fun perform action name = + List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks); end; @@ -135,7 +136,7 @@ (** thy operations **) -(* remove theory *) +(* main loader actions *) fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () => if is_finished name then error (loader_msg "attempt to change finished theory" [name]) @@ -151,11 +152,23 @@ if known_thy name then remove_thy name else ()); +fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () => + let + val name = Context.theory_name theory; + val parents = map Context.theory_name (Theory.parents_of theory); + val _ = kill_thy name; + val _ = map get_theory parents; + val _ = change_thys (new_entry name parents (SOME deps, SOME theory)); + val _ = perform Update name; + in () end); + (* scheduling loader tasks *) +type result = theory * unit future * (unit -> unit); + datatype task = - Task of string list * (theory list -> (theory * unit future * (unit -> unit))) | + Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false @@ -163,15 +176,15 @@ local +fun finish_thy ((thy, present, commit): result) = + (Global_Theory.join_proofs thy; Future.join present; commit (); thy); + fun schedule_seq task_graph = ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab => (case Graph.get_node task_graph name of Task (parents, body) => - let - val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents); - val _ = Future.join present; - val _ = commit (); - in Symtab.update (name, thy) tab end + let val result = body (map (the o Symtab.lookup tab) parents) + in Symtab.update (name, finish_thy result) tab end | Finished thy => Symtab.update (name, thy) tab))) |> ignore; fun schedule_futures task_graph = uninterruptible (fn _ => fn () => @@ -199,10 +212,8 @@ val _ = tasks |> maps (fn name => let - val (thy, present, commit) = Future.join (the (Symtab.lookup futures name)); - val _ = Global_Theory.join_proofs thy; - val _ = Future.join present; - val _ = commit (); + val result = Future.join (the (Symtab.lookup futures name)); + val _ = finish_thy result; in [] end handle exn => [Exn.Exn exn]) |> rev |> Exn.release_all; in () end) (); @@ -226,7 +237,7 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy initiators update_time (deps: deps) text name parent_thys = +fun load_thy initiators update_time deps text name parent_thys = let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); @@ -240,13 +251,7 @@ |> Present.begin_theory update_time dir uses; val (theory, present) = Outer_Syntax.load_thy name init pos text; - - val parents = map Context.theory_name parent_thys; - fun commit () = - NAMED_CRITICAL "Thy_Info" (fn () => - (map get_theory parents; - change_thys (new_entry name parents (SOME deps, SOME theory)); - perform Update name)); + fun commit () = update_thy deps theory; in (theory, present, commit) end; fun check_deps dir name = @@ -274,13 +279,14 @@ let val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); - val dir' = Path.append dir (Path.dir path); - val _ = member (op =) initiators name andalso error (cycle_msg initiators); in (case try (Graph.get_node tasks) name of SOME task => (task_finished task, tasks) | NONE => let + val dir' = Path.append dir (Path.dir path); + val _ = member (op =) initiators name andalso error (cycle_msg initiators); + val (current, deps, imports) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ @@ -332,16 +338,12 @@ let val name = Context.theory_name theory; val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; - val parents = map Context.theory_name (Theory.parents_of theory); val imports = Thy_Load.imports_of theory; - val deps = make_deps master imports; in NAMED_CRITICAL "Thy_Info" (fn () => (kill_thy name; Output.urgent_message ("Registering theory " ^ quote name); - map get_theory parents; - change_thys (new_entry name parents (SOME deps, SOME theory)); - perform Update name)) + update_thy (make_deps master imports) theory)) end; diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/Thy/thy_info.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/thy_info.scala Mon Jul 04 16:54:58 2011 +0200 @@ -0,0 +1,59 @@ +/* Title: Pure/Thy/thy_info.scala + Author: Makarius + +Theory and file dependencies. +*/ + +package isabelle + + +class Thy_Info(thy_load: Thy_Load) +{ + /* messages */ + + private def show_path(names: List[String]): String = + names.map(quote).mkString(" via ") + + private def cycle_msg(names: List[String]): String = + "Cyclic dependency of " + show_path(names) + + private def required_by(s: String, initiators: List[String]): String = + if (initiators.isEmpty) "" + else s + "(required by " + show_path(initiators.reverse) + ")" + + + /* dependencies */ + + type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header) + + private def require_thys( + initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps = + (deps /: strs)(require_thy(initiators, dir, _, _)) + + private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps = + { + val path = Path.explode(str) + val name = path.base.implode + + if (deps.isDefinedAt(name)) deps + else { + val dir1 = dir + path.dir + try { + if (initiators.contains(name)) error(cycle_msg(initiators)) + val (text, header) = + try { thy_load.check_thy(dir1, name) } + catch { + case ERROR(msg) => + cat_error(msg, "The error(s) above occurred while examining theory " + + quote(name) + required_by("\n", initiators)) + } + require_thys(name :: initiators, dir1, + deps + (name -> Exn.Res(text, header)), header.imports) + } + catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } + } + } + + def dependencies(dir: Path, str: String): Deps = + require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??) +} diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/Thy/thy_load.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/thy_load.scala Mon Jul 04 16:54:58 2011 +0200 @@ -0,0 +1,13 @@ +/* Title: Pure/Thy/thy_load.scala + Author: Makarius + +Loading files that contribute to a theory. +*/ + +package isabelle + +abstract class Thy_Load +{ + def check_thy(dir: Path, name: String): (String, Thy_Header.Header) +} + diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Mon Jul 04 16:54:58 2011 +0200 @@ -99,7 +99,7 @@ /** text edits **/ - def text_edits(session: Session, previous: Document.Version, + def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version, edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) = { /* phase 1: edit individual command source */ @@ -147,7 +147,7 @@ commands.iterator(first).takeWhile(_ != last).toList ::: List(last) val sources = range.flatMap(_.span.map(_.source)) - val spans0 = parse_spans(session.current_syntax().scan(sources.mkString)) + val spans0 = parse_spans(syntax.scan(sources.mkString)) val (before_edit, spans1) = if (!spans0.isEmpty && first.is_command && first.span == spans0.head) @@ -159,7 +159,7 @@ (Some(last), spans1.take(spans1.length - 1)) else (commands.next(last), spans1) - val inserted = spans2.map(span => new Command(session.new_id(), span)) + val inserted = spans2.map(span => new Command(new_id(), span)) val new_commands = commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) recover_spans(new_commands) @@ -195,7 +195,7 @@ doc_edits += (name -> Some(cmd_edits)) nodes += (name -> new Document.Node(commands2)) } - (doc_edits.toList, new Document.Version(session.new_id(), nodes)) + (doc_edits.toList, new Document.Version(new_id(), nodes)) } } } diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/build-jars --- a/src/Pure/build-jars Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/build-jars Mon Jul 04 16:54:58 2011 +0200 @@ -50,6 +50,8 @@ Thy/completion.scala Thy/html.scala Thy/thy_header.scala + Thy/thy_info.scala + Thy/thy_load.scala Thy/thy_syntax.scala library.scala package.scala diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/library.ML --- a/src/Pure/library.ML Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/library.ML Mon Jul 04 16:54:58 2011 +0200 @@ -28,7 +28,7 @@ val funpow: int -> ('a -> 'a) -> 'a -> 'a val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a - (*errors*) + (*user errors*) exception ERROR of string val error: string -> 'a val cat_error: string -> string -> 'a @@ -260,7 +260,7 @@ | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::; -(* errors *) +(* user errors *) exception ERROR of string; fun error msg = raise ERROR msg; diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/library.scala --- a/src/Pure/library.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/library.scala Mon Jul 04 16:54:58 2011 +0200 @@ -18,6 +18,27 @@ object Library { + /* user errors */ + + object ERROR + { + def apply(message: String): Throwable = new RuntimeException(message) + def unapply(exn: Throwable): Option[String] = + exn match { + case e: RuntimeException => + val msg = e.getMessage + Some(if (msg == null) "" else msg) + case _ => None + } + } + + def error(message: String): Nothing = throw ERROR(message) + + def cat_error(msg1: String, msg2: String): Nothing = + if (msg1 == "") error(msg1) + else error(msg1 + "\n" + msg2) + + /* lists */ def separate[A](s: A, list: List[A]): List[A] = @@ -41,6 +62,37 @@ } + /* iterate over chunks (cf. space_explode) */ + + def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence] + { + private val end = source.length + private def next_chunk(i: Int): Option[(CharSequence, Int)] = + { + if (i < end) { + var j = i; do j += 1 while (j < end && source.charAt(j) != sep) + Some((source.subSequence(i + 1, j), j)) + } + else None + } + private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) + + def hasNext(): Boolean = state.isDefined + def next(): CharSequence = + state match { + case Some((s, i)) => { state = next_chunk(i); s } + case None => Iterator.empty.next() + } + } + + def first_line(source: CharSequence): String = + { + val lines = chunks(source) + if (lines.hasNext) lines.next.toString + else "" + } + + /* strings */ def quote(s: String): String = "\"" + s + "\"" @@ -73,37 +125,6 @@ } - /* iterate over chunks (cf. space_explode/split_lines in ML) */ - - def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence] - { - private val end = source.length - private def next_chunk(i: Int): Option[(CharSequence, Int)] = - { - if (i < end) { - var j = i; do j += 1 while (j < end && source.charAt(j) != sep) - Some((source.subSequence(i + 1, j), j)) - } - else None - } - private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) - - def hasNext(): Boolean = state.isDefined - def next(): CharSequence = - state match { - case Some((s, i)) => { state = next_chunk(i); s } - case None => Iterator.empty.next() - } - } - - def first_line(source: CharSequence): String = - { - val lines = chunks(source) - if (lines.hasNext) lines.next.toString - else "" - } - - /* simple dialogs */ private def simple_dialog(kind: Int, default_title: String) @@ -160,3 +181,17 @@ Exn.release(result) } } + + +class Basic_Library +{ + val space_explode = Library.space_explode _ + + val quote = Library.quote _ + val commas = Library.commas _ + val commas_quote = Library.commas_quote _ + + val ERROR = Library.ERROR + val error = Library.error _ + val cat_error = Library.cat_error _ +} diff -r 0d96ec6ec33b -r 67d82d94a076 src/Pure/package.scala --- a/src/Pure/package.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Pure/package.scala Mon Jul 04 16:54:58 2011 +0200 @@ -4,8 +4,7 @@ Toplevel isabelle package. */ -package object isabelle +package object isabelle extends isabelle.Basic_Library { - def error(message: String): Nothing = throw new RuntimeException(message) } diff -r 0d96ec6ec33b -r 67d82d94a076 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Mon Jul 04 16:54:58 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 */ - object pending_edits // owned by Swing thread + 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 0d96ec6ec33b -r 67d82d94a076 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Mon Jul 04 16:54:58 2011 +0200 @@ -78,7 +78,7 @@ Swing_Thread.require() if (model.buffer == text_area.getBuffer) body else { - Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model")) + Log.log(Log.ERROR, this, ERROR("Inconsistent document model")) default } } diff -r 0d96ec6ec33b -r 67d82d94a076 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Jul 04 10:23:46 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Jul 04 16:54:58 2011 +0200 @@ -10,14 +10,14 @@ import isabelle._ import java.lang.System -import java.io.{FileInputStream, IOException} +import java.io.{File, FileInputStream, IOException} import java.awt.Font import scala.collection.mutable import scala.swing.ComboBox import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, - Buffer, EditPane, ServiceManager, View} + Buffer, EditPane, MiscUtilities, ServiceManager, View} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider} @@ -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 } } @@ -314,15 +314,30 @@ class Plugin extends EBPlugin { - /* session management */ + /* editor file store */ + + private val file_store = new Session.File_Store + { + def read(path: Path): String = + { + val platform_path = Isabelle.system.platform_path(path) + val canonical_path = MiscUtilities.resolveSymlinks(platform_path) - @volatile private var session_ready = false + Isabelle.jedit_buffers().find(buffer => + MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match { + case Some(buffer) => Isabelle.buffer_text(buffer) + case None => Standard_System.read_file(new File(platform_path)) + } + } + } + + + /* session manager */ private val session_manager = actor { loop { react { case phase: Session.Phase => - session_ready = phase == Session.Ready phase match { case Session.Failed => Swing_Thread.now { @@ -335,7 +350,6 @@ case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model) case _ => } - case bad => System.err.println("session_manager: ignoring bad message " + bad) } } @@ -357,7 +371,7 @@ if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => val buffer = msg.getBuffer - if (buffer != null && session_ready) + if (buffer != null && Isabelle.session.is_ready) Isabelle.init_model(buffer) case msg: EditPaneUpdate @@ -373,7 +387,7 @@ if (buffer != null && text_area != null) { if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || msg.getWhat == EditPaneUpdate.CREATED) { - if (session_ready) + if (Isabelle.session.is_ready) Isabelle.init_view(buffer, text_area) } else Isabelle.exit_view(buffer, text_area) @@ -393,7 +407,7 @@ Isabelle.setup_tooltips() Isabelle.system = new Isabelle_System Isabelle.system.install_fonts() - Isabelle.session = new Session(Isabelle.system) + Isabelle.session = new Session(Isabelle.system, file_store) SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols)) if (ModeProvider.instance.isInstanceOf[ModeProvider]) ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)