# HG changeset patch # User wenzelm # Date 1506698924 -7200 # Node ID 9fc4e144693c7b6b3aec49014bf775124530a18c # Parent afba7ffd64926d19aa28d3f6ccd99e4bdb99af11 tuned signature; diff -r afba7ffd6492 -r 9fc4e144693c src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Sep 29 17:03:33 2017 +0200 +++ b/src/Pure/PIDE/document.scala Fri Sep 29 17:28:44 2017 +0200 @@ -126,6 +126,11 @@ def map_theory(f: String => String): Name = copy(node, master_dir, f(theory)) } + sealed case class Entry(name: Node.Name, header: Node.Header) + { + override def toString: String = name.toString + } + /* node overlays */ diff -r afba7ffd6492 -r 9fc4e144693c src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Sep 29 17:03:33 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Sep 29 17:28:44 2017 +0200 @@ -205,7 +205,7 @@ val syntax = thy_deps.syntax - val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) + val theory_files = thy_deps.entries.map(entry => Path.explode(entry.name.node)) val loaded_files = if (inlined_files) { if (Sessions.is_pure(info.name)) { @@ -251,18 +251,18 @@ val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_)) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) - (graph0 /: thy_deps.deps)( - { case (g, dep) => - val a = node(dep.name) + (graph0 /: thy_deps.entries)( + { case (g, entry) => + val a = node(entry.name) val bs = - dep.header.imports.map({ case (name, _) => node(name) }). + entry.header.imports.map({ case (name, _) => node(name) }). filterNot(_ == a) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) } val known = Known.make(info.dir, List(imports_base), - theories = thy_deps.deps.map(_.name), + theories = thy_deps.entries.map(_.name), loaded_files = loaded_files) val sources = diff -r afba7ffd6492 -r 9fc4e144693c src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Fri Sep 29 17:03:33 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Fri Sep 29 17:28:44 2017 +0200 @@ -7,18 +7,6 @@ package isabelle -object Thy_Info -{ - /* dependencies */ - - sealed case class Dep( - name: Document.Node.Name, - header: Document.Node.Header) - { - override def toString: String = name.toString - } -} - class Thy_Info(resources: Resources) { /* messages */ @@ -42,36 +30,39 @@ } final class Dependencies private( - rev_deps: List[Thy_Info.Dep], + rev_entries: List[Document.Node.Entry], val keywords: Thy_Header.Keywords, val abbrevs: Thy_Header.Abbrevs, val seen: Set[Document.Node.Name]) { - def :: (dep: Thy_Info.Dep): Dependencies = + def :: (entry: Document.Node.Entry): Dependencies = new Dependencies( - dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs, seen) + entry :: rev_entries, + entry.header.keywords ::: keywords, + entry.header.abbrevs ::: abbrevs, + seen) def + (name: Document.Node.Name): Dependencies = - new Dependencies(rev_deps, keywords, abbrevs, seen + name) + new Dependencies(rev_entries, keywords, abbrevs, seen + name) - def deps: List[Thy_Info.Dep] = rev_deps.reverse + def entries: List[Document.Node.Entry] = rev_entries.reverse - def errors: List[String] = deps.flatMap(dep => dep.header.errors) + def errors: List[String] = entries.flatMap(_.header.errors) lazy val syntax: Outer_Syntax = resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs) def loaded_theories: Set[String] = - resources.session_base.loaded_theories ++ rev_deps.map(dep => dep.name.theory) + resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory) def loaded_files: List[(String, List[Path])] = { - val names = deps.map(_.name) + val names = entries.map(_.name) names.map(_.theory) zip Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _))) } - override def toString: String = deps.toString + override def toString: String = entries.toString } private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, @@ -96,11 +87,12 @@ val header = try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } - Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports) + Document.Node.Entry(name, header) :: + require_thys(name :: initiators, required1, header.imports) } catch { case e: Throwable => - Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1 + Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 } } } diff -r afba7ffd6492 -r 9fc4e144693c src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 29 17:03:33 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 29 17:28:44 2017 +0200 @@ -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).deps.map(_.name) + val thy_files = thy_info.dependencies(thys).entries.map(_.name) /* auxiliary files */ diff -r afba7ffd6492 -r 9fc4e144693c src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Fri Sep 29 17:03:33 2017 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 29 17:28:44 2017 +0200 @@ -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).deps.map(_.name).toSet + val retain = PIDE.resources.thy_info.dependencies(imports).entries.map(_.name).toSet for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits) yield edit diff -r afba7ffd6492 -r 9fc4e144693c src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Fri Sep 29 17:03:33 2017 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Fri Sep 29 17:28:44 2017 +0200 @@ -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).deps.map(_.name) + val thy_files = resources.thy_info.dependencies(thys).entries.map(_.name) val aux_files = if (options.bool("jedit_auto_resolve")) {