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;
wenzelm@43651
     1
/*  Title:      Pure/Thy/thy_load.scala
wenzelm@43651
     2
    Author:     Makarius
wenzelm@43651
     3
wenzelm@44577
     4
Primitives for loading theory files.
wenzelm@43651
     5
*/
wenzelm@43651
     6
wenzelm@43651
     7
package isabelle
wenzelm@43651
     8
wenzelm@44953
     9
wenzelm@44953
    10
import java.io.File
wenzelm@44953
    11
wenzelm@44953
    12
wenzelm@44953
    13
wenzelm@44953
    14
class Thy_Load
wenzelm@43651
    15
{
wenzelm@44953
    16
  /* loaded theories provided by prover */
wenzelm@44953
    17
wenzelm@44953
    18
  private var loaded_theories: Set[String] = Set()
wenzelm@44953
    19
wenzelm@44953
    20
  def register_thy(thy_name: String): Unit =
wenzelm@44953
    21
    synchronized { loaded_theories += thy_name }
wenzelm@44953
    22
wenzelm@44953
    23
  def is_loaded(thy_name: String): Boolean =
wenzelm@44953
    24
    synchronized { loaded_theories.contains(thy_name) }
wenzelm@44953
    25
wenzelm@44953
    26
wenzelm@44953
    27
  /* file-system operations */
wenzelm@44953
    28
wenzelm@44953
    29
  def append(dir: String, source_path: Path): String =
wenzelm@44953
    30
    (Path.explode(dir) + source_path).implode
wenzelm@44953
    31
wenzelm@44953
    32
  def check_thy(name: Document.Node.Name): Thy_Header =
wenzelm@44953
    33
  {
wenzelm@44953
    34
    val file = new File(name.node)
wenzelm@44953
    35
    if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
wenzelm@44953
    36
    Thy_Header.read(file)
wenzelm@44953
    37
  }
wenzelm@43651
    38
}
wenzelm@43651
    39