src/Pure/PIDE/resources.scala
author wenzelm
Sat Mar 29 09:34:51 2014 +0100 (2014-03-29)
changeset 56314 9a513737a0b2
parent 56209 3c89e21d9be2
child 56315 c20053f67093
permissions -rw-r--r--
tuned signature;
     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 body_files_test(syntax: Outer_Syntax, text: String): Boolean =
    54     syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    55 
    56   def body_files(syntax: Outer_Syntax, text: String): List[String] =
    57   {
    58     val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    59     spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    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   /* theory text edits */
    95 
    96   def text_edits(
    97     reparse_limit: Int,
    98     previous: Document.Version,
    99     doc_blobs: Document.Blobs,
   100     edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
   101     Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
   102 
   103   def syntax_changed() { }
   104 }
   105