src/Pure/Thy/thy_load.scala
author wenzelm
Sat Sep 17 17:55:39 2011 +0200 (2011-09-17)
changeset 44953 cdfe42f1267c
parent 44616 4beeaf2a226d
child 46737 09ab89658a5d
permissions -rw-r--r--
sane default for class Thy_Load;
     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 java.io.File
    11 
    12 
    13 
    14 class Thy_Load
    15 {
    16   /* loaded theories provided by prover */
    17 
    18   private var loaded_theories: Set[String] = Set()
    19 
    20   def register_thy(thy_name: String): Unit =
    21     synchronized { loaded_theories += thy_name }
    22 
    23   def is_loaded(thy_name: String): Boolean =
    24     synchronized { loaded_theories.contains(thy_name) }
    25 
    26 
    27   /* file-system operations */
    28 
    29   def append(dir: String, source_path: Path): String =
    30     (Path.explode(dir) + source_path).implode
    31 
    32   def check_thy(name: Document.Node.Name): Thy_Header =
    33   {
    34     val file = new File(name.node)
    35     if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    36     Thy_Header.read(file)
    37   }
    38 }
    39