# HG changeset patch # User wenzelm # Date 1509461750 -3600 # Node ID 015d47486fc8a727eac8ba8fb68deaf909a37e79 # Parent 86bc3f1ec97e45b620fadd0b6a54e4b8e50a4f7b clarified modules; diff -r 86bc3f1ec97e -r 015d47486fc8 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Oct 31 15:36:50 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Tue Oct 31 15:55:50 2017 +0100 @@ -17,7 +17,7 @@ val session_base: Sessions.Base, val log: Logger = No_Logger) { - val thy_info = new Thy_Info(this) + resources => def thy_path(path: Path): Path = path.ext("thy") @@ -213,7 +213,113 @@ previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Session.Change = - Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) + Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits) def commit(change: Session.Change) { } + + + /* theory and file dependencies */ + + object Dependencies + { + val empty = new Dependencies(Nil, Set.empty) + } + + final class Dependencies private( + rev_entries: List[Document.Node.Entry], + val seen: Set[Document.Node.Name]) + { + def :: (entry: Document.Node.Entry): Dependencies = + new Dependencies(entry :: rev_entries, seen) + + def + (name: Document.Node.Name): Dependencies = + new Dependencies(rev_entries, seen + name) + + def entries: List[Document.Node.Entry] = rev_entries.reverse + def names: List[Document.Node.Name] = entries.map(_.name) + + def errors: List[String] = entries.flatMap(_.header.errors) + + 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(p => p._1.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: List[(String, List[Path])] = + { + names.map(_.theory) zip + Par_List.map((e: () => List[Path]) => e(), + names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) + } + + def imported_files: List[Path] = + { + val base_theories = + loaded_theories.all_preds(names.map(_.theory)). + filter(session_base.loaded_theories.defined(_)) + + base_theories.map(theory => session_base.known.theories(theory).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 + } + + 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) + ")" + + private def require_thy(initiators: List[Document.Node.Name], required: Dependencies, + thy: (Document.Node.Name, Position.T)): Dependencies = + { + val (name, pos) = thy + + def message: String = + "The error(s) above occurred for theory " + quote(name.theory) + + required_by(initiators) + Position.here(pos) + + val required1 = required + name + if (required.seen(name)) required + else if (session_base.loaded_theory(name)) required1 + else { + try { + if (initiators.contains(name)) error(cycle_msg(initiators)) + val header = + try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } + catch { case ERROR(msg) => cat_error(msg, message) } + Document.Node.Entry(name, header) :: + require_thys(name :: initiators, required1, header.imports) + } + catch { + case e: Throwable => + Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 + } + } + } + + private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, + thys: List[(Document.Node.Name, Position.T)]): Dependencies = + (required /: thys)(require_thy(initiators, _, _)) + + def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = + require_thys(Nil, Dependencies.empty, thys) } diff -r 86bc3f1ec97e -r 015d47486fc8 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Oct 31 15:36:50 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Oct 31 15:55:50 2017 +0100 @@ -222,7 +222,7 @@ } val thy_deps = - resources.thy_info.dependencies( + resources.dependencies( for { (_, thys) <- info.theories; (thy, pos) <- thys } yield (resources.import_name(info.name, info.dir.implode, thy), pos)) diff -r 86bc3f1ec97e -r 015d47486fc8 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Tue Oct 31 15:36:50 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,120 +0,0 @@ -/* Title: Pure/Thy/thy_info.scala - Author: Makarius - -Theory and file dependencies. -*/ - -package isabelle - - -class Thy_Info(resources: Resources) -{ - /* messages */ - - 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) + ")" - - - /* dependencies */ - - object Dependencies - { - val empty = new Dependencies(Nil, Set.empty) - } - - final class Dependencies private( - rev_entries: List[Document.Node.Entry], - val seen: Set[Document.Node.Name]) - { - def :: (entry: Document.Node.Entry): Dependencies = - new Dependencies(entry :: rev_entries, seen) - - def + (name: Document.Node.Name): Dependencies = - new Dependencies(rev_entries, seen + name) - - def entries: List[Document.Node.Entry] = rev_entries.reverse - def names: List[Document.Node.Name] = entries.map(_.name) - - def errors: List[String] = entries.flatMap(_.header.errors) - - lazy val loaded_theories: Graph[String, Outer_Syntax] = - (resources.session_base.loaded_theories /: entries)({ case (graph, entry) => - val name = entry.name.theory - val imports = entry.header.imports.map(p => p._1.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: List[(String, List[Path])] = - { - names.map(_.theory) zip - Par_List.map((e: () => List[Path]) => e(), - names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) - } - - def imported_files: List[Path] = - { - val base = resources.session_base - val base_theories = - loaded_theories.all_preds(names.map(_.theory)). - filter(base.loaded_theories.defined(_)) - - base_theories.map(theory => base.known.theories(theory).path) ::: - base_theories.flatMap(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 - } - - private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, - thys: List[(Document.Node.Name, Position.T)]): Dependencies = - (required /: thys)(require_thy(initiators, _, _)) - - private def require_thy(initiators: List[Document.Node.Name], required: Dependencies, - thy: (Document.Node.Name, Position.T)): Dependencies = - { - val (name, pos) = thy - - def message: String = - "The error(s) above occurred for theory " + quote(name.theory) + - required_by(initiators) + Position.here(pos) - - val required1 = required + name - if (required.seen(name)) required - else if (resources.session_base.loaded_theory(name)) required1 - else { - try { - if (initiators.contains(name)) error(cycle_msg(initiators)) - val header = - try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } - catch { case ERROR(msg) => cat_error(msg, message) } - Document.Node.Entry(name, header) :: - require_thys(name :: initiators, required1, header.imports) - } - catch { - case e: Throwable => - Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 - } - } - } - - def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = - require_thys(Nil, Dependencies.empty, thys) -} diff -r 86bc3f1ec97e -r 015d47486fc8 src/Pure/build-jars --- a/src/Pure/build-jars Tue Oct 31 15:36:50 2017 +0100 +++ b/src/Pure/build-jars Tue Oct 31 15:55:50 2017 +0100 @@ -129,7 +129,6 @@ Thy/present.scala Thy/sessions.scala Thy/thy_header.scala - Thy/thy_info.scala Thy/thy_syntax.scala Tools/bibtex.scala Tools/build.scala diff -r 86bc3f1ec97e -r 015d47486fc8 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Tue Oct 31 15:36:50 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Oct 31 15:55:50 2017 +0100 @@ -216,7 +216,7 @@ (for ((_, model) <- st.models.iterator if model.is_theory) yield (model.node_name, Position.none)).toList - val thy_files = thy_info.dependencies(thys).names + val thy_files = dependencies(thys).names /* auxiliary files */ diff -r 86bc3f1ec97e -r 015d47486fc8 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Oct 31 15:36:50 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Oct 31 15:55:50 2017 +0100 @@ -253,7 +253,7 @@ val pending_nodes = for ((node_name, None) <- purged) yield node_name (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) } - val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet + val retain = PIDE.resources.dependencies(imports).names.toSet for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits) yield edit diff -r 86bc3f1ec97e -r 015d47486fc8 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Oct 31 15:36:50 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Oct 31 15:55:50 2017 +0100 @@ -126,7 +126,7 @@ val thys = (for ((node_name, model) <- models.iterator if model.is_theory) yield (node_name, Position.none)).toList - val thy_files = resources.thy_info.dependencies(thys).names + val thy_files = resources.dependencies(thys).names val aux_files = if (options.bool("jedit_auto_resolve")) {