discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
--- a/src/Pure/PIDE/document.ML Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/document.ML Wed Feb 27 16:27:44 2013 +0100
@@ -83,7 +83,7 @@
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
-val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
val no_perspective = make_perspective [];
val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
@@ -102,9 +102,9 @@
fun read_header node span =
let
- val (dir, {name = (name, _), imports, keywords, files}) = get_header node;
+ val (dir, {name = (name, _), imports, keywords}) = get_header node;
val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
- in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end;
+ in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
--- a/src/Pure/PIDE/document.scala Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/document.scala Wed Feb 27 16:27:44 2013 +0100
@@ -40,13 +40,12 @@
sealed case class Header(
imports: List[Name],
keywords: Thy_Header.Keywords,
- files: List[String],
errors: List[String] = Nil)
{
def error(msg: String): Header = copy(errors = errors ::: List(msg))
}
- def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
+ def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
object Name
{
--- a/src/Pure/PIDE/protocol.ML Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML Wed Feb 27 16:27:44 2013 +0100
@@ -37,17 +37,14 @@
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
let
- val (master, (name, (imports, (keywords, (files, errors))))) =
+ val (master, (name, (imports, (keywords, errors)))) =
pair string (pair string (pair (list string)
(pair (list (pair string
(option (pair (pair string (list string)) (list string)))))
- (pair (list string) (list string))))) a;
+ (list string)))) a;
val imports' = map (rpair Position.none) imports;
- val (files', errors') =
- (map Path.explode files, errors)
- handle ERROR msg => ([], errors @ [msg]);
- val header = Thy_Header.make (name, Position.none) imports' keywords files';
- in Document.Deps (master, header, errors') end,
+ val header = Thy_Header.make (name, Position.none) imports' keywords;
+ in Document.Deps (master, header, errors) end,
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
--- a/src/Pure/PIDE/protocol.scala Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Feb 27 16:27:44 2013 +0100
@@ -289,14 +289,12 @@
val dir = Isabelle_System.posix_path(name.dir)
val imports = header.imports.map(_.node)
val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
- // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
- val files = header.files
(Nil,
pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
pair(list(pair(Encode.string,
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
- pair(list(Encode.string), list(Encode.string))))))(
- (dir, (name.theory, (imports, (keywords, (files, header.errors))))))) },
+ list(Encode.string)))))(
+ (dir, (name.theory, (imports, (keywords, header.errors)))))) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
--- a/src/Pure/Thy/thy_header.ML Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Feb 27 16:27:44 2013 +0100
@@ -10,9 +10,8 @@
type header =
{name: string * Position.T,
imports: (string * Position.T) list,
- keywords: keywords,
- files: Path.T list}
- val make: string * Position.T -> (string * Position.T) list -> keywords -> Path.T list -> header
+ keywords: keywords}
+ val make: string * Position.T -> (string * Position.T) list -> keywords -> header
val define_keywords: header -> unit
val declare_keyword: string * Keyword.spec option -> theory -> theory
val the_keyword: theory -> string -> Keyword.spec option
@@ -29,11 +28,10 @@
type header =
{name: string * Position.T,
imports: (string * Position.T) list,
- keywords: keywords,
- files: Path.T list};
+ keywords: keywords};
-fun make name imports keywords files : header =
- {name = name, imports = imports, keywords = keywords, files = files};
+fun make name imports keywords : header =
+ {name = name, imports = imports, keywords = keywords};
@@ -111,7 +109,7 @@
Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
Parse.$$$ beginN >>
- (fn ((name, imports), keywords) => make name imports keywords []);
+ (fn ((name, imports), keywords) => make name imports keywords);
end;
--- a/src/Pure/Thy/thy_header.scala Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_header.scala Wed Feb 27 16:27:44 2013 +0100
@@ -12,8 +12,6 @@
import scala.util.parsing.input.{Reader, CharSequenceReader}
import scala.util.matching.Regex
-import java.io.{File => JFile}
-
object Thy_Header extends Parse.Parser
{
@@ -72,7 +70,7 @@
(opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
(opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
keyword(BEGIN) ^^
- { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) }
+ { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
(keyword(HEADER) ~ tags) ~!
((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
@@ -117,10 +115,9 @@
sealed case class Thy_Header(
name: String,
imports: List[String],
- keywords: Thy_Header.Keywords,
- files: List[String])
+ keywords: Thy_Header.Keywords)
{
def map(f: String => String): Thy_Header =
- Thy_Header(f(name), imports.map(f), keywords, files.map(f))
+ Thy_Header(f(name), imports.map(f), keywords)
}
--- a/src/Pure/Thy/thy_info.ML Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Feb 27 16:27:44 2013 +0100
@@ -243,7 +243,7 @@
val {master = (thy_path, _), imports} = deps;
val dir = Path.dir thy_path;
- val header = Thy_Header.make (name, pos) imports keywords [];
+ val header = Thy_Header.make (name, pos) imports keywords;
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
--- a/src/Pure/Thy/thy_info.scala Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala Wed Feb 27 16:27:44 2013 +0100
@@ -29,10 +29,15 @@
sealed case class Dep(
name: Document.Node.Name,
- header0: Document.Node.Header,
- future_header: JFuture[Exn.Result[Document.Node.Header]])
+ header: Document.Node.Header)
{
- def join_header: Document.Node.Header = Exn.release(future_header.get)
+ def load_files(syntax: Outer_Syntax): List[String] =
+ {
+ val string = thy_load.with_thy_text(name, _.toString)
+ if (thy_load.body_files_test(syntax, string))
+ thy_load.body_files(syntax, string)
+ else Nil
+ }
}
object Dependencies
@@ -46,24 +51,33 @@
val seen: Set[Document.Node.Name])
{
def :: (dep: Dep): Dependencies =
- new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen)
+ new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, seen)
def + (name: Document.Node.Name): Dependencies =
new Dependencies(rev_deps, keywords, seen = seen + name)
def deps: List[Dep] = rev_deps.reverse
+ lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
+
def loaded_theories: Set[String] =
(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)
+ def load_files: List[Path] =
+ {
+ // FIXME par.map (!?)
+ ((Nil: List[Path]) /: rev_deps) {
+ case (files, dep) =>
+ dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a)) ::: files
+ }
+ }
}
- private def require_thys(files: Boolean, initiators: List[Document.Node.Name],
+ private def require_thys(initiators: List[Document.Node.Name],
required: Dependencies, names: List[Document.Node.Name]): Dependencies =
- (required /: names)(require_thy(files, initiators, _, _))
+ (required /: names)(require_thy(initiators, _, _))
- private def require_thy(files: Boolean, initiators: List[Document.Node.Name],
+ private def require_thy(initiators: List[Document.Node.Name],
required: Dependencies, name: Document.Node.Name): Dependencies =
{
if (required.seen(name)) required
@@ -75,46 +89,18 @@
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
- val syntax = required.make_syntax
-
- val header0 =
+ val header =
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)
- val syntax0 = syntax.add_keywords(header0.keywords)
-
- if (thy_load.body_files_test(syntax0, string)) {
- /* FIXME
- unstable in scala-2.9.2 on multicore hardware -- spurious NPE
- OK in scala-2.10.0.RC3 */
- // default_thread_pool.submit(() =>
- Library.future_value(Exn.capture {
- try {
- val files = thy_load.body_files(syntax0, string)
- header0.copy(files = header0.files ::: files)
- }
- catch { case ERROR(msg) => err(msg) }
- })
- //)
- }
- else Library.future_value(Exn.Res(header0))
- }
- else Library.future_value(Exn.Res(header0))
-
- Dep(name, header0, future_header) ::
- require_thys(files, name :: initiators, required + name, header0.imports)
+ Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
}
catch {
case e: Throwable =>
- val bad_header = Document.Node.bad_header(Exn.message(e))
- Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name)
+ Dep(name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
}
}
}
- def dependencies(inlined_files: Boolean, names: List[Document.Node.Name]): Dependencies =
- require_thys(inlined_files, Nil, Dependencies.empty, names)
+ def dependencies(names: List[Document.Node.Name]): Dependencies =
+ require_thys(Nil, Dependencies.empty, names)
}
--- a/src/Pure/Thy/thy_load.ML Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Wed Feb 27 16:27:44 2013 +0100
@@ -132,7 +132,7 @@
val master_file = check_file dir path;
val text = File.read master_file;
- val {name = (name, pos), imports, files = [], keywords} =
+ val {name = (name, pos), imports, keywords} =
Thy_Header.read (Path.position master_file) text;
val _ = thy_name <> name andalso
error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
@@ -207,7 +207,7 @@
(* load_thy *)
-fun begin_theory master_dir {name, imports, keywords, files = []} parents =
+fun begin_theory master_dir {name, imports, keywords} parents =
Theory.begin_theory name parents
|> put_deps master_dir imports
|> fold Thy_Header.declare_keyword keywords
@@ -238,7 +238,7 @@
let
val time = ! Toplevel.timing;
- val {name = (name, _), files = [], ...} = header;
+ val {name = (name, _), ...} = header;
val _ = Thy_Header.define_keywords header;
val _ = Present.init_theory name;
fun init () =
--- a/src/Pure/Tools/build.scala Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Tools/build.scala Wed Feb 27 16:27:44 2013 +0100
@@ -407,20 +407,18 @@
}
val thy_deps =
- thy_info.dependencies(inlined_files,
+ thy_info.dependencies(
info.theories.map(_._2).flatten.
map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
val loaded_theories = thy_deps.loaded_theories
- val syntax = thy_deps.make_syntax
+ val syntax = thy_deps.syntax
+
+ val body_files = if (inlined_files) thy_deps.load_files else Nil
val all_files =
- (thy_deps.deps.map({ case dep =>
- val thy = Path.explode(dep.name.node)
- val files = dep.join_header.files.map(file =>
- Path.explode(dep.name.dir) + Path.explode(file))
- thy :: files
- }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
+ (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
+ info.files.map(file => info.dir + file)).map(_.expand)
if (list_files)
progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
@@ -432,7 +430,7 @@
error(msg + "\nThe error(s) above occurred in session " +
quote(name) + Position.here(info.pos))
}
- val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
+ val errors = parent_errors
deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
}))
--- a/src/Tools/jEdit/src/plugin.scala Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Feb 27 16:27:44 2013 +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(_.name.node).
+ val files = thy_info.dependencies(thys).deps.map(_.name.node).
filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
if (!files.isEmpty) {