src/Pure/PIDE/resources.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 69575 f71eb0cf8da7
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm@56208
     1
/*  Title:      Pure/PIDE/resources.scala
wenzelm@43651
     2
    Author:     Makarius
wenzelm@43651
     3
wenzelm@56208
     4
Resources for theories and auxiliary files.
wenzelm@43651
     5
*/
wenzelm@43651
     6
wenzelm@43651
     7
package isabelle
wenzelm@43651
     8
wenzelm@44953
     9
wenzelm@48885
    10
import scala.annotation.tailrec
wenzelm@56823
    11
import scala.util.parsing.input.Reader
wenzelm@48885
    12
wenzelm@48409
    13
import java.io.{File => JFile}
wenzelm@44953
    14
wenzelm@44953
    15
wenzelm@65359
    16
class Resources(
wenzelm@65361
    17
  val session_base: Sessions.Base,
wenzelm@65359
    18
  val log: Logger = No_Logger)
wenzelm@43651
    19
{
wenzelm@66959
    20
  resources =>
wenzelm@64839
    21
wenzelm@69260
    22
wenzelm@69260
    23
  /* file formats */
wenzelm@69260
    24
wenzelm@69260
    25
  val file_formats: File_Format.Environment = File_Format.environment()
wenzelm@69260
    26
wenzelm@69260
    27
  def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
wenzelm@69260
    28
    file_formats.get(name).flatMap(_.make_theory_name(resources, name))
wenzelm@69260
    29
wenzelm@69260
    30
  def make_theory_content(thy_name: Document.Node.Name): Option[String] =
wenzelm@69260
    31
    file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
wenzelm@69260
    32
wenzelm@69260
    33
  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
wenzelm@69260
    34
    file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
wenzelm@69260
    35
wenzelm@69260
    36
  def is_hidden(name: Document.Node.Name): Boolean =
wenzelm@69260
    37
    !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name)
wenzelm@69260
    38
wenzelm@65250
    39
  def thy_path(path: Path): Path = path.ext("thy")
wenzelm@65250
    40
wenzelm@64839
    41
wenzelm@44953
    42
  /* file-system operations */
wenzelm@44953
    43
wenzelm@44953
    44
  def append(dir: String, source_path: Path): String =
wenzelm@48711
    45
    (Path.explode(dir) + source_path).expand.implode
wenzelm@44953
    46
wenzelm@65488
    47
  def append(node_name: Document.Node.Name, source_path: Path): String =
wenzelm@65488
    48
    append(node_name.master_dir, source_path)
wenzelm@65488
    49
wenzelm@46737
    50
wenzelm@64657
    51
  /* source files of Isabelle/ML bootstrap */
wenzelm@64657
    52
wenzelm@64657
    53
  def source_file(raw_name: String): Option[String] =
wenzelm@64657
    54
  {
wenzelm@64657
    55
    if (Path.is_wellformed(raw_name)) {
wenzelm@64657
    56
      if (Path.is_valid(raw_name)) {
wenzelm@64657
    57
        def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
wenzelm@64657
    58
wenzelm@64657
    59
        val path = Path.explode(raw_name)
wenzelm@64657
    60
        val path1 =
wenzelm@64657
    61
          if (path.is_absolute || path.is_current) check(path)
wenzelm@64657
    62
          else {
wenzelm@64657
    63
            check(Path.explode("~~/src/Pure") + path) orElse
wenzelm@64657
    64
              (if (Isabelle_System.getenv("ML_SOURCES") == "") None
wenzelm@64657
    65
               else check(Path.explode("$ML_SOURCES") + path))
wenzelm@64657
    66
          }
wenzelm@64657
    67
        Some(File.platform_path(path1 getOrElse path))
wenzelm@64657
    68
      }
wenzelm@64657
    69
      else None
wenzelm@64657
    70
    }
wenzelm@64657
    71
    else Some(raw_name)
wenzelm@64657
    72
  }
wenzelm@64657
    73
wenzelm@64657
    74
wenzelm@46737
    75
  /* theory files */
wenzelm@46737
    76
wenzelm@66702
    77
  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
wenzelm@66699
    78
  {
wenzelm@66918
    79
    val (is_utf8, raw_text) =
wenzelm@66918
    80
      with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
wenzelm@66702
    81
    () => {
wenzelm@66917
    82
      if (syntax.load_commands_in(raw_text)) {
wenzelm@66918
    83
        val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
wenzelm@66702
    84
        val spans = syntax.parse_spans(text)
wenzelm@66702
    85
        val dir = Path.explode(name.master_dir)
wenzelm@66702
    86
        spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
wenzelm@66704
    87
          map(a => (dir + Path.explode(a)).expand).toList
wenzelm@66702
    88
      }
wenzelm@66702
    89
      else Nil
wenzelm@66700
    90
    }
wenzelm@66699
    91
  }
wenzelm@66699
    92
wenzelm@69574
    93
  def pure_files(syntax: Outer_Syntax): List[Path] =
wenzelm@66705
    94
  {
wenzelm@69574
    95
    val pure_dir = Path.explode("~~/src/Pure")
wenzelm@66705
    96
    val roots =
wenzelm@66705
    97
      for { (name, _) <- Thy_Header.ml_roots }
wenzelm@69574
    98
      yield (pure_dir + Path.explode(name)).expand
wenzelm@66705
    99
    val files =
wenzelm@66705
   100
      for {
wenzelm@66705
   101
        (path, (_, theory)) <- roots zip Thy_Header.ml_roots
wenzelm@66705
   102
        file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
wenzelm@66705
   103
      } yield file
wenzelm@66705
   104
    roots ::: files
wenzelm@66705
   105
  }
wenzelm@66700
   106
wenzelm@67104
   107
  def theory_name(qualifier: String, theory: String): String =
wenzelm@67104
   108
    if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
wenzelm@67104
   109
      theory
wenzelm@67104
   110
    else Long_Name.qualify(qualifier, theory)
wenzelm@65471
   111
wenzelm@65445
   112
  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
wenzelm@67104
   113
  {
wenzelm@67104
   114
    val theory = theory_name(qualifier, Thy_Header.import_name(s))
wenzelm@67104
   115
    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
wenzelm@67104
   116
    else {
wenzelm@67104
   117
      session_base.known_theory(theory) match {
wenzelm@67104
   118
        case Some(node_name) => node_name
wenzelm@67104
   119
        case None =>
wenzelm@67104
   120
          if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
wenzelm@67104
   121
            Document.Node.Name.loaded_theory(theory)
wenzelm@67104
   122
          else {
wenzelm@67104
   123
            val path = Path.explode(s)
wenzelm@67104
   124
            val node = append(dir, thy_path(path))
wenzelm@67104
   125
            val master_dir = append(dir, path.dir)
wenzelm@67104
   126
            Document.Node.Name(node, master_dir, theory)
wenzelm@67104
   127
          }
wenzelm@67104
   128
      }
wenzelm@65472
   129
    }
wenzelm@67104
   130
  }
wenzelm@51634
   131
wenzelm@65529
   132
  def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
wenzelm@66966
   133
    import_name(session_base.theory_qualifier(name), name.master_dir, s)
wenzelm@65489
   134
wenzelm@66966
   135
  def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
wenzelm@66767
   136
  {
wenzelm@66767
   137
    val name = import_name(qualifier, dir, s)
wenzelm@66767
   138
    val s1 =
wenzelm@66767
   139
      if (session_base.loaded_theory(name)) name.theory
wenzelm@66767
   140
      else {
wenzelm@66850
   141
        (try { Some(name.path) } catch { case ERROR(_) => None }) match {
wenzelm@66850
   142
          case None => s
wenzelm@66850
   143
          case Some(path) =>
wenzelm@66850
   144
            session_base.known.get_file(path.file) match {
wenzelm@66966
   145
              case Some(name1) if base.theory_qualifier(name1) != qualifier =>
wenzelm@66850
   146
                name1.theory
wenzelm@66850
   147
              case Some(name1) if Thy_Header.is_base_name(s) =>
wenzelm@66850
   148
                name1.theory_base_name
wenzelm@66850
   149
              case _ => s
wenzelm@66850
   150
            }
wenzelm@66767
   151
        }
wenzelm@66767
   152
      }
wenzelm@66767
   153
    val name2 = import_name(qualifier, dir, s1)
wenzelm@66767
   154
    if (name.node == name2.node) s1 else s
wenzelm@66767
   155
  }
wenzelm@66767
   156
wenzelm@64656
   157
  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
wenzelm@64656
   158
  {
wenzelm@66771
   159
    val path = name.path
wenzelm@69403
   160
    if (path.is_file) using(Scan.byte_reader(path.file))(f)
wenzelm@66771
   161
    else if (name.node == name.theory)
wenzelm@66771
   162
      error("Cannot load theory " + quote(name.theory))
wenzelm@66771
   163
    else error ("Cannot load theory file " + path)
wenzelm@64656
   164
  }
wenzelm@64656
   165
wenzelm@65359
   166
  def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
wenzelm@65359
   167
    start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
wenzelm@46737
   168
  {
wenzelm@64826
   169
    if (node_name.is_theory && reader.source.length > 0) {
wenzelm@57615
   170
      try {
wenzelm@66713
   171
        val header = Thy_Header.read(reader, start, strict)
wenzelm@48885
   172
wenzelm@65439
   173
        val base_name = node_name.theory_base_name
wenzelm@59694
   174
        val (name, pos) = header.name
wenzelm@59694
   175
        if (base_name != name)
wenzelm@59718
   176
          error("Bad theory name " + quote(name) +
wenzelm@65250
   177
            " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
wenzelm@66766
   178
            Completion.report_theories(pos, List(base_name)))
wenzelm@48885
   179
wenzelm@67296
   180
        val imports =
wenzelm@67296
   181
          header.imports.map({ case (s, pos) =>
wenzelm@67296
   182
            val name = import_name(node_name, s)
wenzelm@67296
   183
            if (Sessions.exclude_theory(name.theory_base_name))
wenzelm@67296
   184
              error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
wenzelm@67296
   185
            (name, pos)
wenzelm@67296
   186
          })
wenzelm@63579
   187
        Document.Node.Header(imports, header.keywords, header.abbrevs)
wenzelm@57615
   188
      }
wenzelm@57615
   189
      catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
wenzelm@50414
   190
    }
wenzelm@57615
   191
    else Document.Node.no_header
wenzelm@46737
   192
  }
wenzelm@46748
   193
wenzelm@65359
   194
  def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
wenzelm@65359
   195
      strict: Boolean = true): Document.Node.Header =
wenzelm@65359
   196
    with_thy_reader(name, check_thy_reader(name, _, start, strict))
wenzelm@50566
   197
wenzelm@50566
   198
wenzelm@64673
   199
  /* special header */
wenzelm@64673
   200
wenzelm@64673
   201
  def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
wenzelm@65445
   202
  {
wenzelm@65445
   203
    val imports =
wenzelm@67215
   204
      if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
wenzelm@67215
   205
      else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
wenzelm@65489
   206
      else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
wenzelm@65445
   207
      else Nil
wenzelm@65445
   208
    if (imports.isEmpty) None
wenzelm@65445
   209
    else Some(Document.Node.Header(imports.map((_, Position.none))))
wenzelm@65445
   210
  }
wenzelm@64673
   211
wenzelm@64673
   212
wenzelm@64797
   213
  /* blobs */
wenzelm@64797
   214
wenzelm@64797
   215
  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
wenzelm@64797
   216
    (for {
wenzelm@64797
   217
      (node_name, node) <- nodes.iterator
wenzelm@65361
   218
      if !session_base.loaded_theory(node_name)
wenzelm@64797
   219
      cmd <- node.load_commands.iterator
wenzelm@64797
   220
      name <- cmd.blobs_undefined.iterator
wenzelm@64797
   221
    } yield name).toList
wenzelm@64797
   222
wenzelm@64797
   223
wenzelm@56316
   224
  /* document changes */
wenzelm@50566
   225
wenzelm@56316
   226
  def parse_change(
wenzelm@56315
   227
      reparse_limit: Int,
wenzelm@56315
   228
      previous: Document.Version,
wenzelm@56315
   229
      doc_blobs: Document.Blobs,
wenzelm@68337
   230
      edits: List[Document.Edit_Text],
wenzelm@68382
   231
      consolidate: List[Document.Node.Name]): Session.Change =
wenzelm@68337
   232
    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
wenzelm@55134
   233
wenzelm@56316
   234
  def commit(change: Session.Change) { }
wenzelm@66959
   235
wenzelm@66959
   236
wenzelm@66959
   237
  /* theory and file dependencies */
wenzelm@66959
   238
wenzelm@69007
   239
  def dependencies(
wenzelm@69007
   240
      thys: List[(Document.Node.Name, Position.T)],
wenzelm@69008
   241
      progress: Progress = No_Progress): Dependencies[Unit] =
wenzelm@69008
   242
    Dependencies.empty[Unit].require_thys((), thys, progress = progress)
wenzelm@69008
   243
wenzelm@69008
   244
  def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress)
wenzelm@69008
   245
    : Dependencies[Options] =
wenzelm@69008
   246
  {
wenzelm@69008
   247
    val qualifier = info.name
wenzelm@69008
   248
    val dir = info.dir.implode
wenzelm@69008
   249
wenzelm@69008
   250
    (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
wenzelm@69008
   251
      dependencies.require_thys(options,
wenzelm@69008
   252
        for { (thy, pos) <- thys } yield (import_name(qualifier, dir, thy), pos),
wenzelm@69008
   253
        progress = progress)
wenzelm@69008
   254
    })
wenzelm@69008
   255
  }
wenzelm@69007
   256
wenzelm@66959
   257
  object Dependencies
wenzelm@66959
   258
  {
wenzelm@69008
   259
    def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty)
wenzelm@69007
   260
wenzelm@69007
   261
    private def show_path(names: List[Document.Node.Name]): String =
wenzelm@69007
   262
      names.map(name => quote(name.theory)).mkString(" via ")
wenzelm@69007
   263
wenzelm@69007
   264
    private def cycle_msg(names: List[Document.Node.Name]): String =
wenzelm@69007
   265
      "Cyclic dependency of " + show_path(names)
wenzelm@69007
   266
wenzelm@69007
   267
    private def required_by(initiators: List[Document.Node.Name]): String =
wenzelm@69007
   268
      if (initiators.isEmpty) ""
wenzelm@69007
   269
      else "\n(required by " + show_path(initiators.reverse) + ")"
wenzelm@66959
   270
  }
wenzelm@66959
   271
wenzelm@69008
   272
  final class Dependencies[A] private(
wenzelm@66959
   273
    rev_entries: List[Document.Node.Entry],
wenzelm@69008
   274
    seen: Map[Document.Node.Name, A])
wenzelm@66959
   275
  {
wenzelm@69008
   276
    private def cons(entry: Document.Node.Entry): Dependencies[A] =
wenzelm@69008
   277
      new Dependencies[A](entry :: rev_entries, seen)
wenzelm@66959
   278
wenzelm@69008
   279
    def require_thy(adjunct: A,
wenzelm@69007
   280
      thy: (Document.Node.Name, Position.T),
wenzelm@69007
   281
      initiators: List[Document.Node.Name] = Nil,
wenzelm@69008
   282
      progress: Progress = No_Progress): Dependencies[A] =
wenzelm@69007
   283
    {
wenzelm@69007
   284
      val (name, pos) = thy
wenzelm@69007
   285
wenzelm@69007
   286
      def message: String =
wenzelm@69007
   287
        "The error(s) above occurred for theory " + quote(name.theory) +
wenzelm@69007
   288
          Dependencies.required_by(initiators) + Position.here(pos)
wenzelm@69007
   289
wenzelm@69008
   290
      if (seen.isDefinedAt(name)) this
wenzelm@69007
   291
      else {
wenzelm@69008
   292
        val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
wenzelm@69007
   293
        if (session_base.loaded_theory(name)) dependencies1
wenzelm@69007
   294
        else {
wenzelm@69007
   295
          try {
wenzelm@69007
   296
            if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators))
wenzelm@69007
   297
wenzelm@69007
   298
            progress.expose_interrupt()
wenzelm@69007
   299
            val header =
wenzelm@69007
   300
              try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
wenzelm@69007
   301
              catch { case ERROR(msg) => cat_error(msg, message) }
wenzelm@69007
   302
            val entry = Document.Node.Entry(name, header)
wenzelm@69008
   303
            dependencies1.require_thys(adjunct, header.imports,
wenzelm@69008
   304
              initiators = name :: initiators, progress = progress).cons(entry)
wenzelm@69007
   305
          }
wenzelm@69007
   306
          catch {
wenzelm@69007
   307
            case e: Throwable =>
wenzelm@69007
   308
              dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))))
wenzelm@69007
   309
          }
wenzelm@69007
   310
        }
wenzelm@69007
   311
      }
wenzelm@69007
   312
    }
wenzelm@69007
   313
wenzelm@69008
   314
    def require_thys(adjunct: A,
wenzelm@69007
   315
        thys: List[(Document.Node.Name, Position.T)],
wenzelm@69007
   316
        progress: Progress = No_Progress,
wenzelm@69008
   317
        initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
wenzelm@69008
   318
      (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
wenzelm@66959
   319
wenzelm@66959
   320
    def entries: List[Document.Node.Entry] = rev_entries.reverse
wenzelm@69008
   321
wenzelm@67059
   322
    def theories: List[Document.Node.Name] = entries.map(_.name)
wenzelm@69008
   323
    def adjunct_theories: List[(A, Document.Node.Name)] = theories.map(name => (seen(name), name))
wenzelm@66959
   324
wenzelm@66959
   325
    def errors: List[String] = entries.flatMap(_.header.errors)
wenzelm@66959
   326
wenzelm@69008
   327
    def check_errors: Dependencies[A] =
wenzelm@67056
   328
      errors match {
wenzelm@67056
   329
        case Nil => this
wenzelm@67056
   330
        case errs => error(cat_lines(errs))
wenzelm@67056
   331
      }
wenzelm@67056
   332
wenzelm@66959
   333
    lazy val loaded_theories: Graph[String, Outer_Syntax] =
wenzelm@66959
   334
      (session_base.loaded_theories /: entries)({ case (graph, entry) =>
wenzelm@66959
   335
        val name = entry.name.theory
wenzelm@66959
   336
        val imports = entry.header.imports.map(p => p._1.theory)
wenzelm@66959
   337
wenzelm@66959
   338
        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
wenzelm@66959
   339
        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
wenzelm@66959
   340
wenzelm@66959
   341
        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
wenzelm@66959
   342
        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
wenzelm@66959
   343
        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
wenzelm@66959
   344
wenzelm@66959
   345
        graph2.map_node(name, _ => syntax)
wenzelm@66959
   346
      })
wenzelm@66959
   347
wenzelm@69575
   348
    def loaded_files(pure: Boolean): List[(String, List[Path])] =
wenzelm@66959
   349
    {
wenzelm@69574
   350
      val loaded_files =
wenzelm@69574
   351
        theories.map(_.theory) zip
wenzelm@69574
   352
          Par_List.map((e: () => List[Path]) => e(),
wenzelm@69574
   353
            theories.map(name =>
wenzelm@69574
   354
              resources.loaded_files(loaded_theories.get_node(name.theory), name)))
wenzelm@69574
   355
wenzelm@69575
   356
      if (pure) {
wenzelm@69574
   357
        val pure_files = resources.pure_files(overall_syntax)
wenzelm@69574
   358
        loaded_files.map({ case (name, files) =>
wenzelm@69574
   359
          (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
wenzelm@69574
   360
      }
wenzelm@69574
   361
      else loaded_files
wenzelm@66959
   362
    }
wenzelm@66959
   363
wenzelm@66959
   364
    def imported_files: List[Path] =
wenzelm@66959
   365
    {
wenzelm@66959
   366
      val base_theories =
wenzelm@67059
   367
        loaded_theories.all_preds(theories.map(_.theory)).
wenzelm@66959
   368
          filter(session_base.loaded_theories.defined(_))
wenzelm@66959
   369
wenzelm@68307
   370
      base_theories.map(theory => session_base.known.theories(theory).name.path) :::
wenzelm@66959
   371
      base_theories.flatMap(session_base.known.loaded_files(_))
wenzelm@66959
   372
    }
wenzelm@66959
   373
wenzelm@66959
   374
    lazy val overall_syntax: Outer_Syntax =
wenzelm@66959
   375
      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
wenzelm@66959
   376
wenzelm@66959
   377
    override def toString: String = entries.toString
wenzelm@66959
   378
  }
wenzelm@43651
   379
}