src/Pure/Thy/thy_load.scala
author wenzelm
Wed, 29 Feb 2012 23:09:06 +0100
changeset 46737 09ab89658a5d
parent 44953 cdfe42f1267c
child 46748 8f3ae4d04a2d
permissions -rw-r--r--
clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_load.scala
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     3
44577
96b6388d06c4 separate module for jEdit primitives for loading theory files;
wenzelm
parents: 44574
diff changeset
     4
Primitives for loading theory files.
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     5
*/
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     6
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     7
package isabelle
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     8
44953
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
     9
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    10
import java.io.File
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    11
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    12
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    13
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    14
class Thy_Load
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    15
{
44953
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    16
  /* loaded theories provided by prover */
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    17
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    18
  private var loaded_theories: Set[String] = Set()
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    19
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    20
  def register_thy(thy_name: String): Unit =
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    21
    synchronized { loaded_theories += thy_name }
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    22
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    23
  def is_loaded(thy_name: String): Boolean =
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    24
    synchronized { loaded_theories.contains(thy_name) }
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    25
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    26
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    27
  /* file-system operations */
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    28
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    29
  def append(dir: String, source_path: Path): String =
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    30
    (Path.explode(dir) + source_path).implode
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    31
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    32
  def read_header(name: Document.Node.Name): Thy_Header =
44953
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    33
  {
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    34
    val file = new File(name.node)
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    35
    if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    36
    Thy_Header.read(file)
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    37
  }
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    38
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    39
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    40
  /* theory files */
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    41
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    42
  def thy_path(path: Path): Path = path.ext("thy")
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    43
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    44
  private def import_name(dir: String, s: String): Document.Node.Name =
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    45
  {
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    46
    val theory = Thy_Header.base_name(s)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    47
    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    48
    else {
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    49
      val path = Path.explode(s)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    50
      val node = append(dir, thy_path(path))
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    51
      val dir1 = append(dir, path.dir)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    52
      Document.Node.Name(node, dir1, theory)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    53
    }
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    54
  }
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    55
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    56
  def check_thy(name: Document.Node.Name): Document.Node.Deps =
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    57
  {
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    58
    val header = read_header(name)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    59
    val name1 = header.name
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    60
    val imports = header.imports.map(import_name(name.dir, _))
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    61
    val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    62
    if (name.theory != name1)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    63
      error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    64
    Document.Node.Deps(imports, uses)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    65
  }
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    66
}
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    67