--- a/src/Pure/PIDE/resources.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Mon Jan 09 20:47:45 2017 +0100
@@ -17,10 +17,10 @@
{
def thy_path(path: Path): Path = path.ext("thy")
- val empty: Resources = new Resources(Build.Session_Content.empty)
+ val empty: Resources = new Resources(Sessions.Base.empty)
}
-class Resources(val base: Build.Session_Content, val log: Logger = No_Logger)
+class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
--- a/src/Pure/Thy/sessions.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Jan 09 20:47:45 2017 +0100
@@ -29,6 +29,25 @@
}
+ /* base info */
+
+ object Base
+ {
+ val empty: Base = Base()
+
+ lazy val bootstrap: Base =
+ Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
+ }
+
+ sealed case class Base(
+ loaded_theories: Set[String] = Set.empty,
+ known_theories: Map[String, Document.Node.Name] = Map.empty,
+ keywords: Thy_Header.Keywords = Nil,
+ syntax: Outer_Syntax = Outer_Syntax.empty,
+ sources: List[(Path, SHA1.Digest)] = Nil,
+ session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+
+
/* info */
sealed case class Info(
--- a/src/Pure/Tools/build.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Pure/Tools/build.scala Mon Jan 09 20:47:45 2017 +0100
@@ -95,29 +95,10 @@
/* source dependencies and static content */
- object Session_Content
- {
- val empty: Session_Content =
- Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
- Nil, Graph_Display.empty_graph)
-
- lazy val bootstrap: Session_Content =
- Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
- Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
- }
-
- sealed case class Session_Content(
- loaded_theories: Set[String],
- known_theories: Map[String, Document.Node.Name],
- keywords: Thy_Header.Keywords,
- syntax: Outer_Syntax,
- sources: List[(Path, SHA1.Digest)],
- session_graph: Graph_Display.Graph)
-
- sealed case class Deps(deps: Map[String, Session_Content])
+ sealed case class Deps(deps: Map[String, Sessions.Base])
{
def is_empty: Boolean = deps.isEmpty
- def apply(name: String): Session_Content = deps(name)
+ def apply(name: String): Sessions.Base = deps(name)
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
@@ -128,17 +109,17 @@
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
tree: Sessions.Tree): Deps =
- Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
+ Deps((Map.empty[String, Sessions.Base] /: tree.topological_order)(
{ case (deps, (name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
try {
- val base =
- info.parent match {
- case None => Session_Content.bootstrap
- case Some(parent) => deps(parent)
- }
- val resources = new Resources(base)
+ val resources =
+ new Resources(
+ info.parent match {
+ case None => Sessions.Base.bootstrap
+ case Some(parent) => deps(parent)
+ })
if (verbose || list_files) {
val groups =
@@ -165,7 +146,7 @@
}
val known_theories =
- (base.known_theories /: thy_deps.deps)({ case (known, dep) =>
+ (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
val name = dep.name
known.get(name.theory) match {
case Some(name1) if name != name1 =>
@@ -203,12 +184,13 @@
val sources = all_files.map(p => (p, SHA1.digest(p.file)))
val session_graph =
- Present.session_graph(info.parent getOrElse "", base.loaded_theories, thy_deps.deps)
+ Present.session_graph(info.parent getOrElse "",
+ resources.base.loaded_theories, thy_deps.deps)
- val content =
- Session_Content(loaded_theories, known_theories, keywords, syntax,
- sources, session_graph)
- deps + (name -> content)
+ val base =
+ Sessions.Base(
+ loaded_theories, known_theories, keywords, syntax, sources, session_graph)
+ deps + (name -> base)
}
catch {
case ERROR(msg) =>
@@ -227,17 +209,17 @@
dependencies(inlined_files = inlined_files, tree = tree)
}
- def session_content(
+ def session_base(
options: Options,
inlined_files: Boolean,
dirs: List[Path],
- session: String): Session_Content =
+ session: String): Sessions.Base =
{
session_dependencies(options, inlined_files, dirs, List(session))(session)
}
def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
- session_content(options, false, dirs, session).syntax
+ session_base(options, false, dirs, session).syntax
/* jobs */
--- a/src/Tools/VSCode/src/server.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Mon Jan 09 20:47:45 2017 +0100
@@ -199,9 +199,9 @@
}
}
+ val base = Build.session_base(options, false, session_dirs, session_name)
val resources =
- new VSCode_Resources(options, text_length,
- Build.session_content(options, false, session_dirs, session_name), log)
+ new VSCode_Resources(options, text_length, base, log)
{
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Jan 09 20:47:45 2017 +0100
@@ -35,7 +35,7 @@
class VSCode_Resources(
val options: Options,
val text_length: Text.Length,
- base: Build.Session_Content,
+ base: Sessions.Base,
log: Logger = No_Logger) extends Resources(base, log)
{
private val state = Synchronized(VSCode_Resources.State())
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Jan 09 20:47:45 2017 +0100
@@ -23,10 +23,10 @@
object JEdit_Resources
{
- val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
+ val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
}
-class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
+class JEdit_Resources(base: Sessions.Base) extends Resources(base)
{
/* document node name */
--- a/src/Tools/jEdit/src/jedit_sessions.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Mon Jan 09 20:47:45 2017 +0100
@@ -79,15 +79,12 @@
main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
}
- def session_content(inlined_files: Boolean): Build.Session_Content =
+ def session_base(inlined_files: Boolean): Sessions.Base =
{
- val content =
- try {
- Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
- }
- catch { case ERROR(_) => Build.Session_Content.empty }
- content.copy(known_theories =
- content.known_theories.mapValues(name => name.map(File.platform_path(_))))
+ val base =
+ try { Build.session_base(PIDE.options.value, inlined_files, session_dirs(), session_name()) }
+ catch { case ERROR(_) => Sessions.Base.empty }
+ base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
}
--- a/src/Tools/jEdit/src/plugin.scala Mon Jan 09 20:31:00 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Mon Jan 09 20:47:45 2017 +0100
@@ -386,7 +386,7 @@
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
- val resources = new JEdit_Resources(JEdit_Sessions.session_content(false))
+ val resources = new JEdit_Resources(JEdit_Sessions.session_base(false))
PIDE.session.stop()
PIDE.session = new Session(resources) {