# HG changeset patch # User wenzelm # Date 1354883912 -3600 # Node ID e17a1f179bb02a28abb2962f592e5867a94c676c # Parent bf01be7d1a44c97710950214fa4b3a3c81b07ea9 explore theory_body_files via future, for improved performance; further internalization of header errors; diff -r bf01be7d1a44 -r e17a1f179bb0 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Thu Dec 06 23:07:10 2012 +0100 +++ b/src/Pure/System/build.scala Fri Dec 07 13:38:32 2012 +0100 @@ -376,9 +376,10 @@ val syntax = thy_deps.make_syntax val all_files = - (thy_deps.deps.map({ case (n, h) => - val thy = Path.explode(n.node) - val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1)) + (thy_deps.deps.map({ case dep => + val thy = Path.explode(dep.name.node) + val uses = dep.join_header.uses.map(p => + Path.explode(dep.name.dir) + Path.explode(p._1)) thy :: uses }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand) @@ -392,7 +393,7 @@ error(msg + "\nThe error(s) above occurred in session " + quote(name) + Position.here(info.pos)) } - val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten + val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten deps + (name -> Session_Content(loaded_theories, syntax, sources, errors)) })) diff -r bf01be7d1a44 -r e17a1f179bb0 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Dec 06 23:07:10 2012 +0100 +++ b/src/Pure/Thy/thy_info.scala Fri Dec 07 13:38:32 2012 +0100 @@ -7,6 +7,9 @@ package isabelle +import java.util.concurrent.{Future => JFuture} + + class Thy_Info(thy_load: Thy_Load) { /* messages */ @@ -24,7 +27,13 @@ /* dependencies */ - type Dep = (Document.Node.Name, Document.Node.Header) + sealed case class Dep( + name: Document.Node.Name, + header0: Document.Node.Header, + future_header: JFuture[Exn.Result[Document.Node.Header]]) + { + def join_header: Document.Node.Header = Exn.release(future_header.get) + } object Dependencies { @@ -37,7 +46,7 @@ val seen: Set[Document.Node.Name]) { def :: (dep: Dep): Dependencies = - new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen) + new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen) def + (name: Document.Node.Name): Dependencies = new Dependencies(rev_deps, keywords, seen = seen + name) @@ -45,7 +54,7 @@ def deps: List[Dep] = rev_deps.reverse def loaded_theories: Set[String] = - (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory } + (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) } @@ -60,24 +69,41 @@ if (required.seen(name)) required else if (thy_load.loaded_theories(name.theory)) required + name else { + def err(msg: String): Nothing = + cat_error(msg, "The error(s) above occurred while examining theory " + + quote(name.theory) + required_by(initiators)) + try { if (initiators.contains(name)) error(cycle_msg(initiators)) val syntax = required.make_syntax - val header = - try { - if (files) thy_load.check_thy_files(syntax, name) - else thy_load.check_thy(name) + + val header0 = + try { thy_load.check_thy(name) } + catch { case ERROR(msg) => err(msg) } + + val future_header: JFuture[Exn.Result[Document.Node.Header]] = + if (files) { + val string = thy_load.with_thy_text(name, _.toString) + default_thread_pool.submit(() => + Exn.capture { + try { + val syntax0 = syntax.add_keywords(header0.keywords) + val files = thy_load.theory_body_files(syntax0, string) + header0.copy(uses = header0.uses ::: files.map((_, false))) + } + catch { case ERROR(msg) => err(msg) } + } + ) } - catch { - case ERROR(msg) => - cat_error(msg, "The error(s) above occurred while examining theory " + - quote(name.theory) + required_by(initiators)) - } - (name, header) :: require_thys(files, name :: initiators, required + name, header.imports) + else Library.future_value(Exn.Res(header0)) + + Dep(name, header0, future_header) :: + require_thys(files, name :: initiators, required + name, header0.imports) } catch { case e: Throwable => - (name, Document.Node.bad_header(Exn.message(e))) :: (required + name) + val bad_header = Document.Node.bad_header(Exn.message(e)) + Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name) } } } diff -r bf01be7d1a44 -r e17a1f179bb0 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Thu Dec 06 23:07:10 2012 +0100 +++ b/src/Pure/Thy/thy_load.scala Fri Dec 07 13:38:32 2012 +0100 @@ -80,7 +80,7 @@ clean_tokens.reverse.find(_.is_name).map(_.content) } - def find_files(syntax: Outer_Syntax, text: String): List[String] = + def theory_body_files(syntax: Outer_Syntax, text: String): List[String] = { val thy_load_commands = syntax.thy_load_commands if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) { @@ -105,28 +105,22 @@ def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = { - val header = Thy_Header.read(text) + try { + val header = Thy_Header.read(text) - val name1 = header.name - if (name.theory != name1) - error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + - " for theory " + quote(name1)) + val name1 = header.name + if (name.theory != name1) + error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + + " for theory " + quote(name1)) - val imports = header.imports.map(import_name(name.dir, _)) - val uses = header.uses - Document.Node.Header(imports, header.keywords, uses) + val imports = header.imports.map(import_name(name.dir, _)) + val uses = header.uses + Document.Node.Header(imports, header.keywords, uses) + } + catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) } } def check_thy(name: Document.Node.Name): Document.Node.Header = with_thy_text(name, check_thy_text(name, _)) - - def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header = - with_thy_text(name, text => - { - val string = text.toString - val header = check_thy_text(name, string) - val more_uses = find_files(syntax.add_keywords(header.keywords), string) - header.copy(uses = header.uses ::: more_uses.map((_, false))) - }) } diff -r bf01be7d1a44 -r e17a1f179bb0 src/Pure/library.scala --- a/src/Pure/library.scala Thu Dec 06 23:07:10 2012 +0100 +++ b/src/Pure/library.scala Fri Dec 07 13:38:32 2012 +0100 @@ -10,6 +10,7 @@ import java.lang.System import java.util.Locale +import java.util.concurrent.{Future => JFuture, TimeUnit} import java.awt.Component import javax.swing.JOptionPane @@ -187,6 +188,18 @@ selection.index = 3 prototypeDisplayValue = Some("00000%") } + + + /* Java futures */ + + def future_value[A](x: A) = new JFuture[A] + { + def cancel(may_interrupt: Boolean): Boolean = false + def isCancelled(): Boolean = false + def isDone(): Boolean = true + def get(): A = x + def get(timeout: Long, time_unit: TimeUnit): A = x + } } diff -r bf01be7d1a44 -r e17a1f179bb0 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Dec 06 23:07:10 2012 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Fri Dec 07 13:38:32 2012 +0100 @@ -157,7 +157,7 @@ val thy_info = new Thy_Info(PIDE.thy_load) // FIXME avoid I/O in Swing thread!?! - val files = thy_info.dependencies(true, thys).deps.map(_._1.node). + val files = thy_info.dependencies(true, thys).deps.map(_.name.node). filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file)) if (!files.isEmpty) {