--- a/src/Pure/PIDE/document.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/PIDE/document.scala Mon Apr 03 17:00:36 2017 +0200
@@ -504,7 +504,7 @@
case None =>
List(
Node.Deps(
- if (session.resources.base.loaded_theory(node_name))
+ if (session.resources.session_base.loaded_theory(node_name))
node_header.error("Cannot update finished theory " + quote(node_name.theory))
else node_header),
Node.Edits(text_edits), perspective)
--- a/src/Pure/PIDE/resources.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 03 17:00:36 2017 +0200
@@ -15,7 +15,7 @@
class Resources(
val session_name: String,
- val base: Sessions.Base,
+ val session_base: Sessions.Base,
val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
@@ -81,10 +81,10 @@
{
val thy1 = Thy_Header.base_name(s)
val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
- (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_theory(name) => Document.Node.Name.theory(name.theory)
+ (session_base.known_theories.get(thy1) orElse
+ session_base.known_theories.get(thy2) orElse
+ session_base.known_theories.get(Long_Name.base_name(thy1))) match {
+ case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
case Some(name) => name
case None =>
val path = Path.explode(s)
@@ -150,7 +150,7 @@
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
(for {
(node_name, node) <- nodes.iterator
- if !base.loaded_theory(node_name)
+ if !session_base.loaded_theory(node_name)
cmd <- node.load_commands.iterator
name <- cmd.blobs_undefined.iterator
} yield name).toList
--- a/src/Pure/PIDE/session.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/PIDE/session.scala Mon Apr 03 17:00:36 2017 +0200
@@ -191,7 +191,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.session_base.syntax
/* pipelined change parsing */
--- a/src/Pure/Thy/thy_info.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Mon Apr 03 17:00:36 2017 +0200
@@ -71,7 +71,7 @@
val import_errors =
(for {
(theory, names) <- seen_names.iterator_list
- if !resources.base.loaded_theories(theory)
+ if !resources.session_base.loaded_theories(theory)
if names.length > 1
} yield
"Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -83,10 +83,12 @@
}
lazy val syntax: Outer_Syntax =
- resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+ resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
def loaded_theories: Set[String] =
- (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
+ (resources.session_base.loaded_theories /: rev_deps) {
+ case (loaded, dep) => loaded + dep.name.theory
+ }
def loaded_files: List[Path] =
{
@@ -118,7 +120,7 @@
required_by(initiators) + Position.here(require_pos)
val required1 = required + thy
- if (required.seen(name) || resources.base.loaded_theory(name)) required1
+ if (required.seen(name) || resources.session_base.loaded_theory(name)) required1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
--- a/src/Pure/Thy/thy_syntax.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Apr 03 17:00:36 2017 +0200
@@ -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.session_base.syntax /: imports_syntax)(_ ++ _)
.add_keywords(header.keywords).add_abbrevs(header.abbrevs))
}
nodes += (name -> node.update_syntax(syntax))
@@ -300,7 +300,7 @@
doc_blobs.get(name) orElse previous.nodes(name).get_blob
def can_import(name: Document.Node.Name): Boolean =
- resources.base.loaded_theory(name) || nodes0(name).has_header
+ resources.session_base.loaded_theory(name) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -324,7 +324,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.session_base.syntax
val commands = node.commands
val node1 =
--- a/src/Tools/VSCode/src/server.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Mon Apr 03 17:00:36 2017 +0200
@@ -225,8 +225,8 @@
}
}
- val base = Sessions.session_base(options, session_name, session_dirs)
- val resources = new VSCode_Resources(options, base, log)
+ val session_base = Sessions.session_base(options, session_name, session_dirs)
+ val resources = new VSCode_Resources(options, session_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 Apr 03 16:50:44 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Apr 03 17:00:36 2017 +0200
@@ -40,9 +40,10 @@
}
class VSCode_Resources(
- val options: Options,
- base: Sessions.Base,
- log: Logger = No_Logger) extends Resources(session_name = "", base, log)
+ val options: Options,
+ session_base: Sessions.Base,
+ log: Logger = No_Logger)
+ extends Resources(session_name = "", session_base, log)
{
private val state = Synchronized(VSCode_Resources.State())
--- a/src/Tools/jEdit/src/isabelle.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Apr 03 17:00:36 2017 +0200
@@ -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.session_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 Apr 03 16:50:44 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 03 17:00:36 2017 +0200
@@ -21,7 +21,8 @@
import org.gjt.sp.jedit.bufferio.BufferIORequest
-class JEdit_Resources(base: Sessions.Base) extends Resources(session_name = "", base)
+class JEdit_Resources(session_base: Sessions.Base)
+ extends Resources(session_name = "", session_base)
{
/* document node name */
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 03 17:00:36 2017 +0200
@@ -192,7 +192,7 @@
}
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- if (!name.is_theory || PIDE.resources.base.loaded_theory(name) || node.is_empty)
+ if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
status
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
--- a/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 17:00:36 2017 +0200
@@ -187,7 +187,7 @@
}
val nodes_timing1 =
(nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.resources.base.loaded_theory(name)) timing1
+ if (PIDE.resources.session_base.loaded_theory(name)) timing1
else {
val node_timing =
Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)