diff --git a/src/Pure/PIDE/resources.scala b/src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala +++ b/src/Pure/PIDE/resources.scala @@ -1,447 +1,447 @@ /* Title: Pure/PIDE/resources.scala Author: Makarius Resources for theories and auxiliary files. */ package isabelle import scala.util.parsing.input.Reader import java.io.{File => JFile} class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, val log: Logger = No_Logger, command_timings: List[Properties.T] = Nil) { resources => /* init session */ def init_session_yxml: String = { import XML.Encode._ YXML.string_of_body( pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), pair(list(properties), pair(list(pair(string, properties)), pair(list(pair(string, string)), list(string))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, (sessions_structure.bibtex_entries, (command_timings, (Scala.functions.map(fun => (fun.name, fun.position)), (session_base.global_theories.toList, session_base.loaded_theories.keys))))))))) } /* file formats */ def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name)) def make_theory_content(thy_name: Document.Node.Name): Option[String] = File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot)) def is_hidden(name: Document.Node.Name): Boolean = !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) def thy_path(path: Path): Path = path.ext("thy") /* file-system operations */ def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).expand.implode def append(node_name: Document.Node.Name, source_path: Path): String = append(node_name.master_dir, source_path) def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name = { val node = append(dir, file) val master_dir = append(dir, file.dir) Document.Node.Name(node, master_dir, theory) } def loaded_theory_node(theory: String): Document.Node.Name = Document.Node.Name(theory, "", theory) /* source files of Isabelle/ML bootstrap */ def source_file(raw_name: String): Option[String] = { if (Path.is_wellformed(raw_name)) { if (Path.is_valid(raw_name)) { def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None val path = Path.explode(raw_name) val path1 = if (path.is_absolute || path.is_current) check(path) else { check(Path.explode("~~/src/Pure") + path) orElse (if (Isabelle_System.getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) } Some(File.platform_path(path1 getOrElse path)) } else None } else Some(raw_name) } /* theory files */ def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = { val (is_utf8, raw_text) = with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) () => { if (syntax.has_load_commands(raw_text)) { val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)) val spans = syntax.parse_spans(text) val dir = Path.explode(name.master_dir) (for { span <- spans.iterator file <- span.loaded_files(syntax).files } yield (dir + Path.explode(file)).expand).toList } else Nil } } def pure_files(syntax: Outer_Syntax): List[Path] = { val pure_dir = Path.explode("~~/src/Pure") val roots = for { (name, _) <- Thy_Header.ml_roots } yield (pure_dir + Path.explode(name)).expand val files = for { (path, (_, theory)) <- roots zip Thy_Header.ml_roots file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))() } yield file roots ::: files } def theory_name(qualifier: String, theory: String): String = if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(qualifier, theory) def find_theory_node(theory: String): Option[Document.Node.Name] = { val thy_file = thy_path(Path.basic(Long_Name.base_name(theory))) val session = session_base.theory_qualifier(theory) val dirs = sessions_structure.get(session) match { case Some(info) => info.dirs case None => Nil } dirs.collectFirst({ case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) }) } def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = { val theory = theory_name(qualifier, Thy_Header.import_name(s)) def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory) if (!Thy_Header.is_base_name(s)) theory_node else if (session_base.loaded_theory(theory)) loaded_theory_node(theory) else { find_theory_node(theory) match { case Some(node_name) => node_name case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node } } } def import_name(name: Document.Node.Name, s: String): Document.Node.Name = import_name(session_base.theory_qualifier(name), name.master_dir, s) def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) def find_theory(file: JFile): Option[Document.Node.Name] = { for { qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) theory_base <- proper_string(Thy_Header.theory_name(file.getName)) theory = theory_name(qualifier, theory_base) theory_node <- find_theory_node(theory) if File.eq(theory_node.path.file, file) } yield theory_node } def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = { val context_session = session_base.theory_qualifier(context_name) val context_dir = try { Some(context_name.master_dir_path) } catch { case ERROR(_) => None } (for { (session, (info, _)) <- sessions_structure.imports_graph.iterator dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator theory <- Thy_Header.try_read_dir(dir).iterator if Completion.completed(s)(theory) } yield { if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(session, theory) }).toList.sorted } def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val path = name.path if (path.is_file) using(Scan.byte_reader(path.file))(f) else if (name.node == name.theory) error("Cannot load theory " + quote(name.theory)) else error ("Cannot load theory file " + path) } def check_thy(node_name: Document.Node.Name, reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header = { if (node_name.is_theory && reader.source.length > 0) { try { - val header = Thy_Header.read(reader, start, strict).check_keywords + val header = Thy_Header.read(reader, start, strict) val base_name = node_name.theory_base_name if (Long_Name.is_qualified(header.name)) { error("Bad theory name " + quote(header.name) + " with qualification" + Position.here(header.pos)) } if (base_name != header.name) { error("Bad theory name " + quote(header.name) + " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) + Completion.report_theories(header.pos, List(base_name))) } val imports_pos = header.imports_pos.map({ case (s, pos) => val name = import_name(node_name, s) if (Sessions.exclude_theory(name.theory_base_name)) error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos)) (name, pos) }) Document.Node.Header(imports_pos, header.keywords, header.abbrevs) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } } else Document.Node.no_header } /* special header */ def special_header(name: Document.Node.Name): Option[Document.Node.Header] = { val imports = if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name)) else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE)) else Nil if (imports.isEmpty) None else Some(Document.Node.Header(imports.map((_, Position.none)))) } /* blobs */ def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = (for { (node_name, node) <- nodes.iterator if !session_base.loaded_theory(node_name) cmd <- node.load_commands.iterator name <- cmd.blobs_undefined.iterator } yield name).toList /* document changes */ def parse_change( reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change) { } /* theory and file dependencies */ def dependencies( thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress): Dependencies[Unit] = Dependencies.empty[Unit].require_thys((), thys, progress = progress) def session_dependencies(info: Sessions.Info, progress: Progress = new Progress) : Dependencies[Options] = { (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) => dependencies.require_thys(options, for { (thy, pos) <- thys } yield (import_name(info, thy), pos), progress = progress) }) } object Dependencies { def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty) private def show_path(names: List[Document.Node.Name]): String = names.map(name => quote(name.theory)).mkString(" via ") private def cycle_msg(names: List[Document.Node.Name]): String = "Cyclic dependency of " + show_path(names) private def required_by(initiators: List[Document.Node.Name]): String = if (initiators.isEmpty) "" else "\n(required by " + show_path(initiators.reverse) + ")" } final class Dependencies[A] private( rev_entries: List[Document.Node.Entry], seen: Map[Document.Node.Name, A]) { private def cons(entry: Document.Node.Entry): Dependencies[A] = new Dependencies[A](entry :: rev_entries, seen) def require_thy(adjunct: A, thy: (Document.Node.Name, Position.T), initiators: List[Document.Node.Name] = Nil, progress: Progress = new Progress): Dependencies[A] = { val (name, pos) = thy def message: String = "The error(s) above occurred for theory " + quote(name.theory) + Dependencies.required_by(initiators) + Position.here(pos) if (seen.isDefinedAt(name)) this else { val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct)) if (session_base.loaded_theory(name)) dependencies1 else { try { if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators)) progress.expose_interrupt() val header = try { val start = Token.Pos.file(name.node) with_thy_reader(name, check_thy(name, _, start = start)).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } val entry = Document.Node.Entry(name, header) dependencies1.require_thys(adjunct, header.imports_pos, initiators = name :: initiators, progress = progress).cons(entry) } catch { case e: Throwable => dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e)))) } } } } def require_thys(adjunct: A, thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress, initiators: List[Document.Node.Name] = Nil): Dependencies[A] = (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) def entries: List[Document.Node.Entry] = rev_entries.reverse def theories: List[Document.Node.Name] = entries.map(_.name) def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name))) def errors: List[String] = entries.flatMap(_.header.errors) def check_errors: Dependencies[A] = errors match { case Nil => this case errs => error(cat_lines(errs)) } lazy val theory_graph: Document.Node.Name.Graph[Unit] = { val regular = theories.toSet val irregular = (for { entry <- entries.iterator imp <- entry.header.imports if !regular(imp) } yield imp).toSet Document.Node.Name.make_graph( irregular.toList.map(name => ((name, ()), Nil)) ::: entries.map(entry => ((entry.name, ()), entry.header.imports))) } lazy val loaded_theories: Graph[String, Outer_Syntax] = (session_base.loaded_theories /: entries)({ case (graph, entry) => val name = entry.name.theory val imports = entry.header.imports.map(_.theory) val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty)) val graph2 = (graph1 /: imports)(_.add_edge(_, name)) val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header graph2.map_node(name, _ => syntax) }) def loaded_files(pure: Boolean): List[(String, List[Path])] = { val loaded_files = theories.map(_.theory) zip Par_List.map((e: () => List[Path]) => e(), theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) if (pure) { val pure_files = resources.pure_files(overall_syntax) loaded_files.map({ case (name, files) => (name, if (name == Thy_Header.PURE) pure_files ::: files else files) }) } else loaded_files } def imported_files: List[Path] = { val base_theories = loaded_theories.all_preds(theories.map(_.theory)). filter(session_base.loaded_theories.defined) base_theories.map(theory => session_base.known_theories(theory).name.path) ::: base_theories.flatMap(session_base.known_loaded_files(_)) } lazy val overall_syntax: Outer_Syntax = Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node)) override def toString: String = entries.toString } } diff --git a/src/Pure/Thy/thy_header.scala b/src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala +++ b/src/Pure/Thy/thy_header.scala @@ -1,258 +1,258 @@ /* Title: Pure/Thy/thy_header.scala Author: Makarius Static theory header information. */ package isabelle import scala.util.parsing.input.Reader import scala.util.matching.Regex object Thy_Header { /* bootstrap keywords */ type Keywords = List[(String, Keyword.Spec)] type Abbrevs = List[(String, String)] val CHAPTER = "chapter" val SECTION = "section" val SUBSECTION = "subsection" val SUBSUBSECTION = "subsubsection" val PARAGRAPH = "paragraph" val SUBPARAGRAPH = "subparagraph" val TEXT = "text" val TXT = "txt" val TEXT_RAW = "text_raw" val THEORY = "theory" val IMPORTS = "imports" val KEYWORDS = "keywords" val ABBREVS = "abbrevs" val AND = "and" val BEGIN = "begin" val bootstrap_header: Keywords = List( ("%", Keyword.Spec()), ("(", Keyword.Spec()), (")", Keyword.Spec()), (",", Keyword.Spec()), ("::", Keyword.Spec()), ("=", Keyword.Spec()), (AND, Keyword.Spec()), (BEGIN, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), (IMPORTS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), (KEYWORDS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), (ABBREVS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)), (CHAPTER, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), (SECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), (SUBSECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), (SUBSUBSECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), (PARAGRAPH, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), (SUBPARAGRAPH, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)), (TEXT, Keyword.Spec(kind = Keyword.DOCUMENT_BODY)), (TXT, Keyword.Spec(kind = Keyword.DOCUMENT_BODY)), (TEXT_RAW, Keyword.Spec(kind = Keyword.DOCUMENT_RAW)), (THEORY, Keyword.Spec(kind = Keyword.THY_BEGIN, tags = List("theory"))), ("ML", Keyword.Spec(kind = Keyword.THY_DECL, tags = List("ML")))) private val bootstrap_keywords = Keyword.Keywords.empty.add_keywords(bootstrap_header) val bootstrap_syntax: Outer_Syntax = Outer_Syntax.empty.add_keywords(bootstrap_header) /* file name vs. theory name */ val PURE = "Pure" val ML_BOOTSTRAP = "ML_Bootstrap" val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root") val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a)) val bootstrap_global_theories = (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE) private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""") private val File_Name = new Regex(""".*?([^/\\:]+)""") def is_base_name(s: String): Boolean = s != "" && !s.exists("/\\:".contains(_)) def split_file_name(s: String): Option[(String, String)] = s match { case Split_File_Name(s1, s2) => Some((s1, s2)) case _ => None } def import_name(s: String): String = s match { case File_Name(name) if !name.endsWith(".thy") => name case _ => error("Malformed theory import: " + quote(s)) } def theory_name(s: String): String = s match { case Thy_File_Name(name) => bootstrap_name(name) case File_Name(name) => if (name == Sessions.root_name) name else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") case _ => "" } def is_ml_root(theory: String): Boolean = ml_roots.exists({ case (_, b) => b == theory }) def is_bootstrap(theory: String): Boolean = bootstrap_thys.exists({ case (_, b) => b == theory }) def bootstrap_name(theory: String): String = bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory) def try_read_dir(dir: Path): List[String] = { val files = try { File.read_dir(dir) } catch { case ERROR(_) => Nil } for { Thy_File_Name(name) <- files } yield name } /* parser */ trait Parser extends Parse.Parser { val header: Parser[Thy_Header] = { val load_command = ($$$("(") ~! (position(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(("", Position.none)) val keyword_kind = atom("outer syntax keyword specification", _.is_name) val keyword_spec = position(keyword_kind) ~ load_command ~ tags ^^ { case (a, b) ~ c ~ d => Keyword.Spec(kind = a, kind_pos = b, load_command = c._1, load_command_pos = c._2, tags = d) } val keyword_decl = rep1(string) ~ opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec()))) } val keyword_decls = keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ { case xs ~ yss => (xs :: yss).flatten } val abbrevs = rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^ { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) } val args = position(theory_name) ~ (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(ABBREVS) ~! abbrevs) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a, b, c, d).map(Symbol.decode) } val heading = (command(CHAPTER) | command(SECTION) | command(SUBSECTION) | command(SUBSUBSECTION) | command(PARAGRAPH) | command(SUBPARAGRAPH) | command(TEXT) | command(TXT) | command(TEXT_RAW)) ~ annotation ~! document_source (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x } } } /* read -- lazy scanning */ private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) = { val token = Token.Parsers.token(bootstrap_keywords) def make_tokens(in: Reader[Char]): Stream[Token] = token(in) match { case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) case _ => Stream.empty } val all_tokens = make_tokens(reader) val drop_tokens = if (strict) Nil else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList val tokens = all_tokens.drop(drop_tokens.length) val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList (drop_tokens, tokens1 ::: tokens2) } private object Parser extends Parser { def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header = parse(commit(header), Token.reader(tokens, pos)) match { case Success(result, _) => result case bad => error(bad.toString) } } def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = { val (_, tokens0) = read_tokens(reader, true) val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0)) val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) val pos = (start /: drop_tokens)(_.advance(_)) - Parser.parse_header(tokens, pos) + Parser.parse_header(tokens, pos).check_keywords } } sealed case class Thy_Header( name_pos: (String, Position.T), imports_pos: List[(String, Position.T)], keywords: Thy_Header.Keywords, abbrevs: Thy_Header.Abbrevs) { def name: String = name_pos._1 def pos: Position.T = name_pos._2 def imports: List[String] = imports_pos.map(_._1) def map(f: String => String): Thy_Header = Thy_Header((f(name), pos), imports_pos.map({ case (a, b) => (f(a), b) }), keywords.map({ case (a, spec) => (f(a), spec.map(f)) }), abbrevs.map({ case (a, b) => (f(a), f(b)) })) def check_keywords: Thy_Header = { for ((_, spec) <- keywords) { if (spec.kind != Keyword.THY_LOAD && spec.load_command.nonEmpty) { error("Illegal load command specification for kind: " + quote(spec.kind) + Position.here(spec.kind_pos)) } if (!Command_Span.load_commands.exists(_.name == spec.load_command)) { error("Unknown load command specification: " + quote(spec.load_command) + Position.here(spec.load_command_pos)) } } this } }