src/Pure/PIDE/resources.scala
author wenzelm
Thu Apr 03 20:17:12 2014 +0200 (2014-04-03)
changeset 56392 bc118a32a870
parent 56387 d92eb5c3960d
child 56393 22f533e6a049
permissions -rw-r--r--
tuned signature (see also 0850d43cb355);
     1 /*  Title:      Pure/PIDE/resources.scala
     2     Author:     Makarius
     3 
     4 Resources for theories and auxiliary files.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.annotation.tailrec
    11 
    12 import java.io.{File => JFile}
    13 
    14 
    15 object Resources
    16 {
    17   def thy_path(path: Path): Path = path.ext("thy")
    18 }
    19 
    20 
    21 class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
    22 {
    23   /* document node names */
    24 
    25   def node_name(raw_path: Path): Document.Node.Name =
    26   {
    27     val path = raw_path.expand
    28     val node = path.implode
    29     val theory = Thy_Header.thy_name(node).getOrElse("")
    30     val master_dir = if (theory == "") "" else path.dir.implode
    31     Document.Node.Name(node, master_dir, theory)
    32   }
    33 
    34 
    35   /* file-system operations */
    36 
    37   def append(dir: String, source_path: Path): String =
    38     (Path.explode(dir) + source_path).expand.implode
    39 
    40   def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    41   {
    42     val path = Path.explode(name.node)
    43     if (!path.is_file) error("No such file: " + path.toString)
    44 
    45     val text = File.read(path)
    46     Symbol.decode_strict(text)
    47     f(text)
    48   }
    49 
    50 
    51   /* theory files */
    52 
    53   def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
    54   {
    55     if (syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    56       val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    57       spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    58     }
    59     else Nil
    60   }
    61 
    62   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    63   {
    64     val theory = Thy_Header.base_name(s)
    65     if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
    66     else {
    67       val path = Path.explode(s)
    68       val node = append(master.master_dir, Resources.thy_path(path))
    69       val master_dir = append(master.master_dir, path.dir)
    70       Document.Node.Name(node, master_dir, theory)
    71     }
    72   }
    73 
    74   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
    75   {
    76     try {
    77       val header = Thy_Header.read(text)
    78 
    79       val name1 = header.name
    80       if (name.theory != name1)
    81         error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) +
    82           " for theory " + quote(name1))
    83 
    84       val imports = header.imports.map(import_name(name, _))
    85       Document.Node.Header(imports, header.keywords, Nil)
    86     }
    87     catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    88   }
    89 
    90   def check_thy(name: Document.Node.Name): Document.Node.Header =
    91     with_thy_text(name, check_thy_text(name, _))
    92 
    93 
    94   /* document changes */
    95 
    96   def parse_change(
    97       reparse_limit: Int,
    98       previous: Document.Version,
    99       doc_blobs: Document.Blobs,
   100       edits: List[Document.Edit_Text]): Session.Change =
   101     Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
   102 
   103   def commit(change: Session.Change) { }
   104 
   105 
   106   /* prover process */
   107 
   108   def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
   109     new Isabelle_Process(receiver, args) with Protocol
   110 }
   111