src/Pure/Thy/thy_load.scala
changeset 48422 9613780a805b
parent 48409 0d2114eb412a
child 48484 70898d016538
equal deleted inserted replaced
48421:c4d337782de4 48422:9613780a805b
     8 
     8 
     9 
     9 
    10 import java.io.{File => JFile}
    10 import java.io.{File => JFile}
    11 
    11 
    12 
    12 
       
    13 object Thy_Load
       
    14 {
       
    15   def thy_path(path: Path): Path = path.ext("thy")
       
    16 }
    13 
    17 
    14 class Thy_Load
    18 
       
    19 class Thy_Load(preloaded: Set[String] = Set.empty)
    15 {
    20 {
    16   /* loaded theories provided by prover */
    21   /* loaded theories provided by prover */
    17 
    22 
    18   private var loaded_theories: Set[String] = Set()
    23   private var loaded_theories: Set[String] = preloaded
    19 
    24 
    20   def register_thy(thy_name: String): Unit =
    25   def register_thy(thy_name: String): Unit =
    21     synchronized { loaded_theories += thy_name }
    26     synchronized { loaded_theories += thy_name }
    22 
    27 
    23   def is_loaded(thy_name: String): Boolean =
    28   def is_loaded(thy_name: String): Boolean =
    37   }
    42   }
    38 
    43 
    39 
    44 
    40   /* theory files */
    45   /* theory files */
    41 
    46 
    42   def thy_path(path: Path): Path = path.ext("thy")
       
    43 
       
    44   private def import_name(dir: String, s: String): Document.Node.Name =
    47   private def import_name(dir: String, s: String): Document.Node.Name =
    45   {
    48   {
    46     val theory = Thy_Header.base_name(s)
    49     val theory = Thy_Header.base_name(s)
    47     if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
    50     if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
    48     else {
    51     else {
    49       val path = Path.explode(s)
    52       val path = Path.explode(s)
    50       val node = append(dir, thy_path(path))
    53       val node = append(dir, Thy_Load.thy_path(path))
    51       val dir1 = append(dir, path.dir)
    54       val dir1 = append(dir, path.dir)
    52       Document.Node.Name(node, dir1, theory)
    55       Document.Node.Name(node, dir1, theory)
    53     }
    56     }
    54   }
    57   }
    55 
    58 
    58     val name1 = header.name
    61     val name1 = header.name
    59     val imports = header.imports.map(import_name(name.dir, _))
    62     val imports = header.imports.map(import_name(name.dir, _))
    60     // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
    63     // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
    61     val uses = header.uses
    64     val uses = header.uses
    62     if (name.theory != name1)
    65     if (name.theory != name1)
    63       error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
    66       error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
       
    67         " for theory " + quote(name1))
    64     Document.Node.Deps(imports, header.keywords, uses)
    68     Document.Node.Deps(imports, header.keywords, uses)
    65   }
    69   }
    66 
    70 
    67   def check_thy(name: Document.Node.Name): Document.Node.Deps =
    71   def check_thy(name: Document.Node.Name): Document.Node.Deps =
    68     check_header(name, read_header(name))
    72     check_header(name, read_header(name))