diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala +++ b/src/Pure/PIDE/command.scala @@ -1,582 +1,582 @@ /* Title: Pure/PIDE/command.scala Author: Fabian Immler, TU Munich Author: Makarius Prover commands with accumulated results from execution. */ package isabelle import scala.collection.mutable import scala.collection.immutable.SortedMap object Command { type Edit = (Option[Command], Option[Command]) sealed case class Blob( name: Document.Node.Name, src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) type Blobs_Info = (List[Exn.Result[Blob]], Int) val no_blobs: Blobs_Info = (Nil, -1) /** accumulated results from prover **/ /* results */ object Results { type Entry = (Long, XML.Tree) val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Tree]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) def get(serial: Long): Option[XML.Tree] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = if (defined(entry._1)) this else new Results(rep + entry) def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Results => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Results(", ", ", ")") } /* exports */ object Exports { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) { def is_empty: Boolean = rep.isEmpty def iterator: Iterator[Exports.Entry] = rep.iterator def + (entry: Exports.Entry): Exports = if (rep.isDefinedAt(entry._1)) this else new Exports(rep + entry) def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Exports => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Exports(", ", ", ")") } /* markups */ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { val empty: Markups = new Markups(Map.empty) def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) { def is_empty: Boolean = rep.isEmpty def apply(index: Markup_Index): Markup_Tree = rep.getOrElse(index, Markup_Tree.empty) def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) def + (entry: (Markup_Index, Markup_Tree)): Markups = { val (index, tree) = entry new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) } def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other else (this /: other.rep.iterator)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Markups => rep == other.rep case _ => false } override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") } /* state */ object State { def get_result(states: List[State], serial: Long): Option[XML.Tree] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) tree @ XML.Elem(_, body) <- get_result(states, serial) if body.nonEmpty } yield (serial -> tree) def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) def merge_exports(states: List[State]): Exports = Exports.merge(states.map(_.exports)) def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) def merge_markup(states: List[State], index: Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(states), merge_markups(states)) } sealed case class State( command: Command, status: List[Markup] = Nil, results: Results = Results.empty, exports: Exports = Exports.empty, markups: Markups = Markups.empty) { def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) lazy val maybe_consolidated: Boolean = { var touched = false var forks = 0 var runs = 0 for (markup <- status) { markup.name match { case Markup.FORKED => touched = true; forks += 1 case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 case _ => } } touched && forks == 0 && runs == 0 } lazy val document_status: Document_Status.Command_Status = { val warnings = if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = if (results.iterator.exists(p => Protocol.is_error(p._2))) List(Markup(Markup.ERROR, Nil)) else Nil Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) } def markup(index: Markup_Index): Markup_Tree = markups(index) def redirect(other_command: Command): Option[State] = { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = copy(status = st :: status) private def add_result(entry: Results.Entry): State = copy(results = results + entry) def add_export(entry: Exports.Entry): Option[State] = if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) else None private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) markups.add(Markup_Index(true, chunk_name), m) else markups copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def accumulate( self_id: Document_ID.Generic => Boolean, other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem, xml_cache: XML.Cache): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => if (command.span.is_theory) this else { (this /: msgs)((state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => state. add_status(markup). add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) case _ => Output.warning("Ignored status message: " + msg) state }) } case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => (this /: msgs)((state, msg) => { def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { case XML.Elem(Markup(name, atts1), args) => val atts = atts1 ::: atts0 command.reported_position(atts) match { case Some((id, chunk_name)) => val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) else None (target, atts) match { case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = atts.filterNot(Markup.position_property) val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state } case _ => // silently ignore excessive reports state } case _ => bad(); state } case _ => bad(); state } }) case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => val markup_message = xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) val message_markup = xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) var st = add_result(i -> markup_message) if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator range <- command.message_positions(self_id, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st case _ => Output.warning("Ignored message without serial number: " + message) this } } } /** static content **/ /* make commands */ def apply( id: Document_ID.Command, node_name: Document.Node.Name, blobs_info: Blobs_Info, span: Command_Span.Span): Command = { val (source, span1) = span.compact_source new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty) def unparsed( source: String, theory: Boolean = false, id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, results: Results = Results.empty, markups: Markups = Markups.empty): Command = { val (source1, span1) = Command_Span.unparsed(source, theory).compact_source new Command(id, node_name, no_blobs, span1, source1, results, markups) } def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = unparsed(XML.content(body), id = id, results = results, markups = Markups.init(Markup_Tree.from_XML(body))) /* perspective */ object Perspective { val empty: Perspective = Perspective(Nil) } sealed case class Perspective(commands: List[Command]) // visible commands in canonical order { def is_empty: Boolean = commands.isEmpty def same(that: Perspective): Boolean = { val cmds1 = this.commands val cmds2 = that.commands require(!cmds1.exists(_.is_undefined)) require(!cmds2.exists(_.is_undefined)) cmds1.length == cmds2.length && (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) } } /* blobs: inlined errors and auxiliary files */ def blobs_info( resources: Resources, syntax: Outer_Syntax, get_blob: Document.Node.Name => Option[Document.Blob], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span): Blobs_Info = { span.name match { // inlined errors case Thy_Header.THEORY => val reader = Scan.char_reader(Token.implode(span.content)) val header = resources.check_thy(node_name, reader) val imports_pos = header.imports_pos val raw_imports = try { - val read_imports = Thy_Header.read(reader).imports + val read_imports = Thy_Header.read(node_name, reader).imports if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case _: Throwable => List.fill(imports_pos.length)("") } val errors = for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) } yield { val completion = if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil val msg = "Bad theory import " + Markup.Path(import_name.node).markup(quote(import_name.toString)) + Position.here(pos) + Completion.report_theories(pos, completion) Exn.Exn[Command.Blob](ERROR(msg)) } (errors, -1) // auxiliary files case _ => val loaded_files = span.loaded_files(syntax) val blobs = loaded_files.files.map(file => (Exn.capture { val src_path = Path.explode(file) val name = Document.Node.Name(resources.append(node_name, src_path)) val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk)) Blob(name, src_path, content) }).user_error) (blobs, loaded_files.index) } } } final class Command private( val id: Document_ID.Command, val node_name: Document.Node.Name, val blobs_info: Command.Blobs_Info, val span: Command_Span.Span, val source: String, val init_results: Command.Results, val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString /* classification */ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY /* blobs */ def blobs: List[Exn.Result[Command.Blob]] = blobs_info._1 def blobs_index: Int = blobs_info._2 def blobs_ok: Boolean = blobs.forall({ case Exn.Res(_) => true case _ => false }) def blobs_names: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs) yield blob.name def blobs_undefined: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest) def blobs_changed(doc_blobs: Document.Blobs): Boolean = blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false }) /* source chunks */ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content) yield Symbol.Text_Chunk.File(blob.name.node) -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range val core_range: Text.Range = Text.Range(0, (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) /* reported positions */ def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] = pos match { case Position.Id(id) => val chunk_name = pos match { case Position.File(name) if name != node_name.node => Symbol.Text_Chunk.File(name) case _ => Symbol.Text_Chunk.Default } Some((id, chunk_name)) case _ => None } def message_positions( self_id: Document_ID.Generic => Boolean, chunk_name: Symbol.Text_Chunk.Name, chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = reported_position(props) match { case Some((id, name)) if self_id(id) && name == chunk_name => val opt_range = Position.Range.unapply(props) orElse { if (name == Symbol.Text_Chunk.Default) Position.Range.unapply(span.position) else None } opt_range match { case Some(symbol_range) => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set } case None => set } case _ => set } def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = t match { case XML.Wrapped_Elem(Markup(name, props), _, body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Elem(Markup(name, props), body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Text(_) => set } val set = tree(Set.empty, message) if (set.isEmpty) elem(message.markup.properties, set) else set } /* accumulated results */ val init_state: Command.State = Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } 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,434 @@ /* 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 thy_file = Thy_Header.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) + def theory_node = make_theory_node(dir, Thy_Header.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 = start, strict = 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 header = Thy_Header.read(node_name, reader, start = start, strict = strict) 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,260 +1,272 @@ /* 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 } + def thy_path(path: Path): Path = path.ext("thy") + /* 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], + def read(node_name: Document.Node.Name, reader: Reader[Char], start: Token.Pos = Token.Pos.none, 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).check_keywords + Parser.parse_header(tokens, pos).check(node_name) } } 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 = + def check(node_name: Document.Node.Name): Thy_Header = { + val base_name = node_name.theory_base_name + if (Long_Name.is_qualified(name)) { + error("Bad theory name " + quote(name) + " with qualification" + Position.here(pos)) + } + if (base_name != name) { + error("Bad theory name " + quote(name) + " for file " + + Thy_Header.thy_path(Path.basic(base_name)) + Position.here(pos) + + Completion.report_theories(pos, List(base_name))) + } + 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 } }