src/Pure/Thy/thy_load.scala
author wenzelm
Fri Dec 07 13:38:32 2012 +0100 (2012-12-07 ago)
changeset 50414 e17a1f179bb0
parent 50291 674893679352
child 50415 0d60de55c58a
permissions -rw-r--r--
explore theory_body_files via future, for improved performance;
further internalization of header errors;
     1 /*  Title:      Pure/Thy/thy_load.scala
     2     Author:     Makarius
     3 
     4 Primitives for loading theory files.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.annotation.tailrec
    11 
    12 import java.io.{File => JFile}
    13 
    14 
    15 object Thy_Load
    16 {
    17   /* paths */
    18 
    19   def thy_path(path: Path): Path = path.ext("thy")
    20 
    21   def is_ok(str: String): Boolean =
    22     try { thy_path(Path.explode(str)); true }
    23     catch { case ERROR(_) => false }
    24 
    25 
    26   /* node names */
    27 
    28   def external_node(raw_path: Path): Document.Node.Name =
    29   {
    30     val path = raw_path.expand
    31     val node = path.implode
    32     val dir = path.dir.implode
    33     val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    34     Document.Node.Name(node, dir, theory)
    35   }
    36 }
    37 
    38 
    39 class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
    40 {
    41   /* file-system operations */
    42 
    43   def append(dir: String, source_path: Path): String =
    44     (Path.explode(dir) + source_path).expand.implode
    45 
    46   def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    47   {
    48     val path = Path.explode(name.node)
    49     if (!path.is_file) error("No such file: " + path.toString)
    50 
    51     val text = File.read(path)
    52     Symbol.decode_strict(text)
    53     f(text)
    54   }
    55 
    56 
    57   /* theory files */
    58 
    59   private def import_name(dir: String, s: String): Document.Node.Name =
    60   {
    61     val theory = Thy_Header.base_name(s)
    62     if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
    63     else {
    64       val path = Path.explode(s)
    65       val node = append(dir, Thy_Load.thy_path(path))
    66       val dir1 = append(dir, path.dir)
    67       Document.Node.Name(node, dir1, theory)
    68     }
    69   }
    70 
    71   private def find_file(tokens: List[Token]): Option[String] =
    72   {
    73     def clean(toks: List[Token]): List[Token] =
    74       toks match {
    75         case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    76         case t :: ts => t :: clean(ts)
    77         case Nil => Nil
    78       }
    79     val clean_tokens = clean(tokens.filter(_.is_proper))
    80     clean_tokens.reverse.find(_.is_name).map(_.content)
    81   }
    82 
    83   def theory_body_files(syntax: Outer_Syntax, text: String): List[String] =
    84   {
    85     val thy_load_commands = syntax.thy_load_commands
    86     if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    87       val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    88       spans.iterator.map({
    89         case toks @ (tok :: _) if tok.is_command =>
    90           thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
    91             case Some((_, exts)) =>
    92               find_file(toks) match {
    93                 case Some(file) =>
    94                   if (exts.isEmpty) List(file)
    95                   else exts.map(ext => file + "." + ext)
    96                 case None => Nil
    97               }
    98             case None => Nil
    99           }
   100         case _ => Nil
   101       }).flatten.toList
   102     }
   103     else Nil
   104   }
   105 
   106   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   107   {
   108     try {
   109       val header = Thy_Header.read(text)
   110 
   111       val name1 = header.name
   112       if (name.theory != name1)
   113         error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
   114           " for theory " + quote(name1))
   115 
   116       val imports = header.imports.map(import_name(name.dir, _))
   117       val uses = header.uses
   118       Document.Node.Header(imports, header.keywords, uses)
   119     }
   120     catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
   121   }
   122 
   123   def check_thy(name: Document.Node.Name): Document.Node.Header =
   124     with_thy_text(name, check_thy_text(name, _))
   125 }
   126