# HG changeset patch # User wenzelm # Date 1345651470 -7200 # Node ID d5fdaf7dd1f83b3977fcd33909da1c34ee3f95fd # Parent 963b50ec6d73267a2c3e8de1abe2d3d8c2dc3a98 find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy; diff -r 963b50ec6d73 -r d5fdaf7dd1f8 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Wed Aug 22 16:24:52 2012 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Wed Aug 22 18:04:30 2012 +0200 @@ -58,8 +58,8 @@ def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name) def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1) - def thy_load_commands: List[String] = - (for ((name, (Keyword.THY_LOAD, _)) <- keywords.iterator) yield name).toList + def thy_load_commands: List[(String, List[String])] = + (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax = new Outer_Syntax( diff -r 963b50ec6d73 -r d5fdaf7dd1f8 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Aug 22 16:24:52 2012 +0200 +++ b/src/Pure/Thy/thy_info.scala Wed Aug 22 18:04:30 2012 +0200 @@ -64,7 +64,7 @@ if (initiators.contains(name)) error(cycle_msg(initiators)) val syntax = required.make_syntax val header = - try { thy_load.check_thy(syntax, name) } + try { thy_load.check_thy_files(syntax, name) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred while examining theory " + diff -r 963b50ec6d73 -r d5fdaf7dd1f8 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Wed Aug 22 16:24:52 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Wed Aug 22 18:04:30 2012 +0200 @@ -7,6 +7,8 @@ package isabelle +import scala.annotation.tailrec + import java.io.{File => JFile} @@ -27,6 +29,13 @@ def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).expand.implode + def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = + { + val path = Path.explode(name.node) + if (!path.is_file) error("No such file: " + path.toString) + f(File.read(path)) + } + /* theory files */ @@ -42,26 +51,65 @@ } } - def check_thy_text(syntax: Outer_Syntax, name: Document.Node.Name, text: CharSequence) - : Document.Node.Header = + private def find_file(tokens: List[Token]): Option[String] = + { + def clean(toks: List[Token]): List[Token] = + toks match { + case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts) + case t :: ts => t :: clean(ts) + case Nil => Nil + } + val clean_tokens = clean(tokens.filter(_.is_proper)) + clean_tokens.reverse.find(_.is_name).map(_.content) + } + + def find_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) })) { + val spans = Thy_Syntax.parse_spans(syntax.scan(text)) + spans.iterator.map({ + case toks @ (tok :: _) if tok.is_command => + thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match { + case Some((_, exts)) => + find_file(toks) match { + case Some(file) => + if (exts.isEmpty) List(file) + else exts.map(ext => file + "." + ext) + case None => Nil + } + case None => Nil + } + case _ => Nil + }).flatten.toList + } + else Nil + } + + def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = { val header = Thy_Header.read(text) + val name1 = header.name - val imports = header.imports.map(import_name(name.dir, _)) - // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) - // FIXME find files in text - val uses = header.uses 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) } - def check_thy(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header = - { - val path = Path.explode(name.node) - if (!path.is_file) error("No such file: " + path.toString) - check_thy_text(syntax, name, File.read(path)) - } + 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, string) + header.copy(uses = header.uses ::: more_uses.map((_, false))) + }) } diff -r 963b50ec6d73 -r d5fdaf7dd1f8 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Aug 22 16:24:52 2012 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 22 18:04:30 2012 +0200 @@ -68,8 +68,7 @@ Swing_Thread.require() Isabelle.buffer_lock(buffer) { Exn.capture { - val text = buffer.getSegment(0, buffer.getLength) - Isabelle.thy_load.check_thy_text(session.recent_syntax, name, text) + Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength)) } match { case Exn.Res(header) => header case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) diff -r 963b50ec6d73 -r d5fdaf7dd1f8 src/Tools/jEdit/src/jedit_thy_load.scala --- a/src/Tools/jEdit/src/jedit_thy_load.scala Wed Aug 22 16:24:52 2012 +0200 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala Wed Aug 22 18:04:30 2012 +0200 @@ -33,6 +33,23 @@ } } + override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = + { + Swing_Thread.now { + Isabelle.jedit_buffer(name.node) match { + case Some(buffer) => + Isabelle.buffer_lock(buffer) { + Some(f(buffer.getSegment(0, buffer.getLength))) + } + case None => None + } + } getOrElse { + val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?) + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) + f(File.read(file)) + } + } + def check_file(view: View, path: String): Boolean = { val vfs = VFSManager.getVFSForPath(path) @@ -52,23 +69,5 @@ catch { case _: IOException => } } } - - override def check_thy(syntax: Outer_Syntax, name: Document.Node.Name) - : Document.Node.Header = - { - Swing_Thread.now { - Isabelle.jedit_buffer(name.node) match { - case Some(buffer) => - Isabelle.buffer_lock(buffer) { - Some(check_thy_text(syntax, name, buffer.getSegment(0, buffer.getLength))) - } - case None => None - } - } getOrElse { - val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?) - if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) - check_thy_text(syntax, name, File.read(file)) - } - } }