src/Pure/Thy/thy_load.scala
author wenzelm
Mon Apr 08 14:18:39 2013 +0200 (2013-04-08)
changeset 51634 553953ad8165
parent 51293 05b1bbae748d
child 54513 5545aff878b1
permissions -rw-r--r--
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
     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   /* document node names */
    27 
    28   def path_node_name(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 find_file(tokens: List[Token]): Option[String] =
    60   {
    61     def clean(toks: List[Token]): List[Token] =
    62       toks match {
    63         case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    64         case t :: ts => t :: clean(ts)
    65         case Nil => Nil
    66       }
    67     val clean_tokens = clean(tokens.filter(_.is_proper))
    68     clean_tokens.reverse.find(_.is_name).map(_.content)
    69   }
    70 
    71   def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
    72     syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    73 
    74   def body_files(syntax: Outer_Syntax, text: String): List[String] =
    75   {
    76     val thy_load_commands = syntax.thy_load_commands
    77     val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    78     spans.iterator.map({
    79       case toks @ (tok :: _) if tok.is_command =>
    80         thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
    81           case Some((_, exts)) =>
    82             find_file(toks) match {
    83               case Some(file) =>
    84                 if (exts.isEmpty) List(file)
    85                 else exts.map(ext => file + "." + ext)
    86               case None => Nil
    87             }
    88           case None => Nil
    89         }
    90       case _ => Nil
    91     }).flatten.toList
    92   }
    93 
    94   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    95   {
    96     val theory = Thy_Header.base_name(s)
    97     if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
    98     else {
    99       val path = Path.explode(s)
   100       val node = append(master.dir, Thy_Load.thy_path(path))
   101       val dir = append(master.dir, path.dir)
   102       Document.Node.Name(node, dir, theory)
   103     }
   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, _))
   117       Document.Node.Header(imports, header.keywords, Nil)
   118     }
   119     catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   120   }
   121 
   122   def check_thy(name: Document.Node.Name): Document.Node.Header =
   123     with_thy_text(name, check_thy_text(name, _))
   124 
   125 
   126   /* theory text edits */
   127 
   128   def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
   129       : (List[Document.Edit_Command], Document.Version) =
   130     Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
   131 }
   132