--- a/src/Pure/PIDE/document.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/PIDE/document.scala Thu Dec 28 21:45:28 2017 +0100
@@ -119,7 +119,7 @@
def path: Path = Path.explode(File.standard_path(node))
- def is_bibtex: Boolean = Bibtex.check_name(node)
+ def is_bibtex: Boolean = Bibtex.is_bibtex(node)
def is_theory: Boolean = theory.nonEmpty
--- a/src/Pure/PIDE/resources.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Dec 28 21:45:28 2017 +0100
@@ -189,7 +189,7 @@
}
def is_hidden(name: Document.Node.Name): Boolean =
- !name.is_theory || name.theory == Sessions.root_name
+ !name.is_theory || name.theory == Sessions.root_name || Bibtex.is_bibtex_theory(name)
/* blobs */
--- a/src/Pure/Thy/bibtex.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala Thu Dec 28 21:45:28 2017 +0100
@@ -7,6 +7,8 @@
package isabelle
+import java.io.{File => JFile}
+
import scala.collection.mutable
import scala.util.parsing.combinator.RegexParsers
import scala.util.parsing.input.Reader
@@ -129,7 +131,39 @@
/** document model **/
- def check_name(name: String): Boolean = name.endsWith(".bib")
+ /* bibtex files */
+
+ def is_bibtex(name: String): Boolean = name.endsWith(".bib")
+ def is_bibtex_theory(name: Document.Node.Name): Boolean = is_bibtex(name.theory)
+
+ private val node_suffix: String = "bibtex_file"
+
+ def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
+ {
+ Thy_Header.file_name(name.node) match {
+ case Some(bib_name) if is_bibtex(bib_name) =>
+ val thy_node = resources.append(name.node, Path.explode(node_suffix))
+ Some(Document.Node.Name(thy_node, name.master_dir, bib_name))
+ case _ => None
+ }
+ }
+
+ def make_theory_content(bib_name: String): Option[String] =
+ if (is_bibtex(bib_name)) {
+ Some("""theory "bib" imports Pure begin bibtex_file """ + quote(bib_name) + """ end""")
+ }
+ else None
+
+ def make_theory_content(file: JFile): Option[String] =
+ if (file.getName == node_suffix) {
+ val parent = file.getParentFile
+ if (parent != null && is_bibtex(parent.getName)) make_theory_content(parent.getName)
+ else None
+ }
+ else None
+
+
+ /* entries */
def entries(text: String): List[Text.Info[String]] =
{
--- a/src/Pure/Thy/sessions.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Dec 28 21:45:28 2017 +0100
@@ -30,7 +30,7 @@
def exclude_session(name: String): Boolean = name == "" || name == DRAFT
def exclude_theory(name: String): Boolean =
- name == root_name || name == "README" || name == "index"
+ name == root_name || name == "README" || name == "index" || name == "bib"
/* base info and source dependencies */
--- a/src/Pure/Thy/thy_header.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala Thu Dec 28 21:45:28 2017 +0100
@@ -85,6 +85,12 @@
def is_base_name(s: String): Boolean =
s != "" && !s.exists("/\\:".contains(_))
+ def file_name(s: String): Option[String] =
+ s match {
+ case File_Name(s) => Some(s)
+ case _ => None
+ }
+
def import_name(s: String): String =
s match {
case File_Name(name) if !name.endsWith(".thy") => name
--- a/src/Tools/jEdit/src/jedit_bibtex.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala Thu Dec 28 21:45:28 2017 +0100
@@ -35,7 +35,7 @@
case text_area: TextArea =>
text_area.getBuffer match {
case buffer: Buffer
- if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
+ if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
val menu = new JMenu("BibTeX entries")
for (entry <- Bibtex.known_entries) {
val item = new JMenuItem(entry.kind)
--- a/src/Tools/jEdit/src/jedit_resources.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Dec 28 21:45:28 2017 +0100
@@ -46,7 +46,7 @@
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else {
- val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
+ val master_dir = vfs.getParentOfPath(path)
Document.Node.Name(node, master_dir, theory)
}
}
@@ -80,14 +80,16 @@
def read_file_content(node_name: Document.Node.Name): Option[String] =
{
- val name = node_name.node
- try {
- val text =
- if (Url.is_wellformed(name)) Url.read(Url(name))
- else File.read(new JFile(name))
- Some(Symbol.decode(Line.normalize(text)))
+ Bibtex.make_theory_content(node_name.theory) orElse {
+ val name = node_name.node
+ try {
+ val text =
+ if (Url.is_wellformed(name)) Url.read(Url(name))
+ else File.read(new JFile(name))
+ Some(Symbol.decode(Line.normalize(text)))
+ }
+ catch { case ERROR(_) => None }
}
- catch { case ERROR(_) => None }
}
def get_file_content(node_name: Document.Node.Name): Option[String] =
--- a/src/Tools/jEdit/src/plugin.scala Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Dec 28 21:45:28 2017 +0100
@@ -126,7 +126,13 @@
val thys =
(for ((node_name, model) <- models.iterator if model.is_theory)
yield (node_name, Position.none)).toList
- val thy_files = resources.dependencies(thys).theories
+ val thy_files1 = resources.dependencies(thys).theories
+
+ val thy_files2 =
+ (for {
+ (name, _) <- models.iterator if name.is_bibtex
+ thy_name <- Bibtex.make_theory_name(resources, name)
+ } yield thy_name).toList
val aux_files =
if (options.bool("jedit_auto_resolve")) {
@@ -141,7 +147,7 @@
}
else Nil
- (thy_files ::: aux_files).filterNot(models.isDefinedAt(_))
+ (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt(_))
}
if (required_files.nonEmpty) {
try {