src/Pure/Thy/thy_load.scala
changeset 44953 cdfe42f1267c
parent 44616 4beeaf2a226d
child 46737 09ab89658a5d
equal deleted inserted replaced
44952:28a11f5fd3b8 44953:cdfe42f1267c
     4 Primitives for loading theory files.
     4 Primitives for loading theory files.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 abstract class Thy_Load
     9 
       
    10 import java.io.File
       
    11 
       
    12 
       
    13 
       
    14 class Thy_Load
    10 {
    15 {
    11   def register_thy(thy_name: String)
    16   /* loaded theories provided by prover */
    12   def is_loaded(thy_name: String): Boolean
    17 
    13   def append(dir: String, path: Path): String
    18   private var loaded_theories: Set[String] = Set()
    14   def check_thy(node_name: Document.Node.Name): Thy_Header
    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   }
    15 }
    38 }
    16 
    39