--- a/src/Pure/PIDE/batch_session.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/PIDE/batch_session.scala Mon Jan 09 20:26:59 2017 +0100
@@ -29,11 +29,7 @@
new RuntimeException
val deps = Build.dependencies(verbose = verbose, tree = session_tree)
- val resources =
- {
- val content = deps(parent_session)
- new Resources(content.loaded_theories, content.known_theories, content.syntax)
- }
+ val resources = new Resources(deps(parent_session))
val progress = new Console_Progress(verbose = verbose)
--- a/src/Pure/PIDE/document.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/PIDE/document.scala Mon Jan 09 20:26:59 2017 +0100
@@ -488,7 +488,7 @@
case None =>
List(
Document.Node.Deps(
- if (session.resources.loaded_theories(node_name.theory))
+ if (session.resources.base.loaded_theories(node_name.theory))
node_header.error("Cannot update finished theory " + quote(node_name.theory))
else node_header),
Document.Node.Edits(text_edits), perspective)
--- a/src/Pure/PIDE/resources.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Mon Jan 09 20:26:59 2017 +0100
@@ -17,14 +17,10 @@
{
def thy_path(path: Path): Path = path.ext("thy")
- val empty: Resources = new Resources(Set.empty, Map.empty, Outer_Syntax.empty)
+ val empty: Resources = new Resources(Build.Session_Content.empty)
}
-class Resources(
- val loaded_theories: Set[String],
- val known_theories: Map[String, Document.Node.Name],
- val base_syntax: Outer_Syntax,
- val log: Logger = No_Logger)
+class Resources(val base: Build.Session_Content, val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
@@ -94,10 +90,10 @@
val no_qualifier = "" // FIXME
val thy1 = Thy_Header.base_name(s)
val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
- (known_theories.get(thy1) orElse
- known_theories.get(thy2) orElse
- known_theories.get(Long_Name.base_name(thy1))) match {
- case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory)
+ (base.known_theories.get(thy1) orElse
+ base.known_theories.get(thy2) orElse
+ base.known_theories.get(Long_Name.base_name(thy1))) match {
+ case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
case Some(name) => name
case None =>
val path = Path.explode(s)
@@ -164,7 +160,7 @@
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
(for {
(node_name, node) <- nodes.iterator
- if !loaded_theories(node_name.theory)
+ if !base.loaded_theories(node_name.theory)
cmd <- node.load_commands.iterator
name <- cmd.blobs_undefined.iterator
} yield name).toList
--- a/src/Pure/PIDE/session.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/PIDE/session.scala Mon Jan 09 20:26:59 2017 +0100
@@ -239,7 +239,7 @@
def recent_syntax(name: Document.Node.Name): Outer_Syntax =
global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
- resources.base_syntax
+ resources.base.syntax
/* pipelined change parsing */
--- a/src/Pure/Thy/thy_header.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala Mon Jan 09 20:26:59 2017 +0100
@@ -37,7 +37,7 @@
val AND = "and"
val BEGIN = "begin"
- private val bootstrap_header: Keywords =
+ val bootstrap_header: Keywords =
List(
("%", Keyword.no_spec),
("(", Keyword.no_spec),
--- a/src/Pure/Thy/thy_info.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/Thy/thy_info.scala Mon Jan 09 20:26:59 2017 +0100
@@ -71,7 +71,7 @@
val import_errors =
(for {
(theory, names) <- seen_names.iterator_list
- if !resources.loaded_theories(theory)
+ if !resources.base.loaded_theories(theory)
if names.length > 1
} yield
"Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -83,10 +83,10 @@
}
lazy val syntax: Outer_Syntax =
- resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+ resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
def loaded_theories: Set[String] =
- (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
+ (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
def loaded_files: List[Path] =
{
@@ -118,7 +118,7 @@
required_by(initiators) + Position.here(require_pos)
val required1 = required + thy
- if (required.seen(name) || resources.loaded_theories(name.theory)) required1
+ if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
--- a/src/Pure/Thy/thy_syntax.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Mon Jan 09 20:26:59 2017 +0100
@@ -101,7 +101,7 @@
else {
val header = node.header
val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
- Some((resources.base_syntax /: imports_syntax)(_ ++ _)
+ Some((resources.base.syntax /: imports_syntax)(_ ++ _)
.add_keywords(header.keywords).add_abbrevs(header.abbrevs))
}
nodes += (name -> node.update_syntax(syntax))
@@ -297,7 +297,7 @@
doc_blobs.get(name) orElse previous.nodes(name).get_blob
def can_import(name: Document.Node.Name): Boolean =
- resources.loaded_theories(name.theory) || nodes0(name).has_header
+ resources.base.loaded_theories(name.theory) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -321,7 +321,7 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
- val syntax = node.syntax getOrElse resources.base_syntax
+ val syntax = node.syntax getOrElse resources.base.syntax
val commands = node.commands
val node1 =
--- a/src/Pure/Tools/build.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Pure/Tools/build.scala Mon Jan 09 20:26:59 2017 +0100
@@ -98,7 +98,12 @@
object Session_Content
{
def empty: Session_Content =
- Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty, Nil, Graph_Display.empty_graph)
+ Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
+ Nil, Graph_Display.empty_graph)
+
+ def 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(
@@ -128,15 +133,12 @@
if (progress.stopped) throw Exn.Interrupt()
try {
- val (loaded_theories0, known_theories0, syntax0) =
- info.parent.map(deps(_)) match {
- case None =>
- (Set.empty[String], Map.empty[String, Document.Node.Name],
- Thy_Header.bootstrap_syntax)
- case Some(parent) =>
- (parent.loaded_theories, parent.known_theories, parent.syntax)
+ val base =
+ info.parent match {
+ case None => Session_Content.bootstrap
+ case Some(parent) => deps(parent)
}
- val resources = new Resources(loaded_theories0, known_theories0, syntax0)
+ val resources = new Resources(base)
if (verbose || list_files) {
val groups =
@@ -163,7 +165,7 @@
}
val known_theories =
- (known_theories0 /: thy_deps.deps)({ case (known, dep) =>
+ (base.known_theories /: thy_deps.deps)({ case (known, dep) =>
val name = dep.name
known.get(name.theory) match {
case Some(name1) if name != name1 =>
@@ -201,7 +203,7 @@
val sources = all_files.map(p => (p, SHA1.digest(p.file)))
val session_graph =
- Present.session_graph(info.parent getOrElse "", loaded_theories0, thy_deps.deps)
+ Present.session_graph(info.parent getOrElse "", base.loaded_theories, thy_deps.deps)
val content =
Session_Content(loaded_theories, known_theories, keywords, syntax,
--- a/src/Tools/VSCode/src/server.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Mon Jan 09 20:26:59 2017 +0100
@@ -199,10 +199,10 @@
}
}
- val content = Build.session_content(options, false, session_dirs, session_name)
val resources =
- new VSCode_Resources(options, text_length, content.loaded_theories,
- content.known_theories, content.syntax, log) {
+ new VSCode_Resources(options, text_length,
+ Build.session_content(options, false, session_dirs, session_name), log)
+ {
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
delay_load.invoke()
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Jan 09 20:26:59 2017 +0100
@@ -33,13 +33,10 @@
}
class VSCode_Resources(
- val options: Options,
- val text_length: Text.Length,
- loaded_theories: Set[String],
- known_theories: Map[String, Document.Node.Name],
- base_syntax: Outer_Syntax,
- log: Logger = No_Logger)
- extends Resources(loaded_theories, known_theories, base_syntax, log)
+ val options: Options,
+ val text_length: Text.Length,
+ base: Build.Session_Content,
+ log: Logger = No_Logger) extends Resources(base, log)
{
private val state = Synchronized(VSCode_Resources.State())
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jan 09 20:26:59 2017 +0100
@@ -50,7 +50,7 @@
def mode_syntax(mode: String): Option[Outer_Syntax] =
mode match {
- case "isabelle" => Some(PIDE.resources.base_syntax)
+ case "isabelle" => Some(PIDE.resources.base.syntax)
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Sessions.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Jan 09 20:26:59 2017 +0100
@@ -23,15 +23,10 @@
object JEdit_Resources
{
- val empty: JEdit_Resources =
- new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
+ val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
}
-class JEdit_Resources(
- loaded_theories: Set[String],
- known_theories: Map[String, Document.Node.Name],
- base_syntax: Outer_Syntax)
- extends Resources(loaded_theories, known_theories, base_syntax)
+class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
{
/* document node name */
--- a/src/Tools/jEdit/src/plugin.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Mon Jan 09 20:26:59 2017 +0100
@@ -386,9 +386,7 @@
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
- val content = JEdit_Sessions.session_content(false)
- val resources =
- new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
+ val resources = new JEdit_Resources(JEdit_Sessions.session_content(false))
PIDE.session.stop()
PIDE.session = new Session(resources) {
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Jan 09 20:26:59 2017 +0100
@@ -188,7 +188,7 @@
}
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- if (!name.is_theory || PIDE.resources.loaded_theories(name.theory) || node.is_empty)
+ if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
status
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
--- a/src/Tools/jEdit/src/timing_dockable.scala Mon Jan 09 19:34:16 2017 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Jan 09 20:26:59 2017 +0100
@@ -187,7 +187,7 @@
}
val nodes_timing1 =
(nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.resources.loaded_theories(name.theory)) timing1
+ if (PIDE.resources.base.loaded_theories(name.theory)) timing1
else {
val node_timing =
Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)