src/Pure/Thy/thy_load.scala
author wenzelm
Wed, 22 Aug 2012 16:10:23 +0200
changeset 48883 04cd2fddb4d9
parent 48882 61dc7d5d150a
child 48885 d5fdaf7dd1f8
permissions -rw-r--r--
pass syntax through check_thy;
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
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 46938
diff changeset
    10
import java.io.{File => JFile}
44953
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
48422
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    13
object Thy_Load
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    14
{
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    15
  def thy_path(path: Path): Path = path.ext("thy")
48484
70898d016538 more explicit checks during parsing;
wenzelm
parents: 48422
diff changeset
    16
70898d016538 more explicit checks during parsing;
wenzelm
parents: 48422
diff changeset
    17
  def is_ok(str: String): Boolean =
70898d016538 more explicit checks during parsing;
wenzelm
parents: 48422
diff changeset
    18
    try { thy_path(Path.explode(str)); true }
70898d016538 more explicit checks during parsing;
wenzelm
parents: 48422
diff changeset
    19
    catch { case ERROR(_) => false }
48422
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    20
}
44953
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    21
48422
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    22
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48827
diff changeset
    23
class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    24
{
44953
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    25
  /* file-system operations */
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
  def append(dir: String, source_path: Path): String =
48711
8d381fdef898 need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
wenzelm
parents: 48710
diff changeset
    28
    (Path.explode(dir) + source_path).expand.implode
44953
cdfe42f1267c sane default for class Thy_Load;
wenzelm
parents: 44616
diff changeset
    29
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    30
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    31
  /* theory files */
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    32
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    33
  private def import_name(dir: String, s: String): Document.Node.Name =
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    34
  {
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    35
    val theory = Thy_Header.base_name(s)
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48827
diff changeset
    36
    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    37
    else {
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    38
      val path = Path.explode(s)
48422
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    39
      val node = append(dir, Thy_Load.thy_path(path))
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    40
      val dir1 = append(dir, path.dir)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    41
      Document.Node.Name(node, dir1, theory)
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    42
    }
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    43
  }
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    44
48883
04cd2fddb4d9 pass syntax through check_thy;
wenzelm
parents: 48882
diff changeset
    45
  def check_thy_text(syntax: Outer_Syntax, name: Document.Node.Name, text: CharSequence)
04cd2fddb4d9 pass syntax through check_thy;
wenzelm
parents: 48882
diff changeset
    46
    : Document.Node.Header =
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    47
  {
48882
61dc7d5d150a use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm
parents: 48870
diff changeset
    48
    val header = Thy_Header.read(text)
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    49
    val name1 = header.name
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    50
    val imports = header.imports.map(import_name(name.dir, _))
46770
44c28a33c461 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents: 46748
diff changeset
    51
    // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
48883
04cd2fddb4d9 pass syntax through check_thy;
wenzelm
parents: 48882
diff changeset
    52
    // FIXME find files in text
46770
44c28a33c461 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents: 46748
diff changeset
    53
    val uses = header.uses
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    54
    if (name.theory != name1)
48422
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    55
      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48409
diff changeset
    56
        " for theory " + quote(name1))
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48484
diff changeset
    57
    Document.Node.Header(imports, header.keywords, uses)
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 44953
diff changeset
    58
  }
46748
8f3ae4d04a2d refined node_header -- more direct buffer access (again);
wenzelm
parents: 46737
diff changeset
    59
48883
04cd2fddb4d9 pass syntax through check_thy;
wenzelm
parents: 48882
diff changeset
    60
  def check_thy(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
48882
61dc7d5d150a use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm
parents: 48870
diff changeset
    61
  {
61dc7d5d150a use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm
parents: 48870
diff changeset
    62
    val path = Path.explode(name.node)
61dc7d5d150a use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm
parents: 48870
diff changeset
    63
    if (!path.is_file) error("No such file: " + path.toString)
48883
04cd2fddb4d9 pass syntax through check_thy;
wenzelm
parents: 48882
diff changeset
    64
    check_thy_text(syntax, name, File.read(path))
48882
61dc7d5d150a use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm
parents: 48870
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