# HG changeset patch # User wenzelm # Date 1491231636 -7200 # Node ID ecefb68dc21d31c5304c37c4298a68c906b9de4a # Parent 3ff88fece1f680c07764130ea1088266594449e7 tuned signature; diff -r 3ff88fece1f6 -r ecefb68dc21d src/Pure/PIDE/document.scala --- 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) diff -r 3ff88fece1f6 -r ecefb68dc21d src/Pure/PIDE/resources.scala --- 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 diff -r 3ff88fece1f6 -r ecefb68dc21d src/Pure/PIDE/session.scala --- 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 */ diff -r 3ff88fece1f6 -r ecefb68dc21d src/Pure/Thy/thy_info.scala --- 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)) diff -r 3ff88fece1f6 -r ecefb68dc21d src/Pure/Thy/thy_syntax.scala --- 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 = diff -r 3ff88fece1f6 -r ecefb68dc21d src/Tools/VSCode/src/server.scala --- 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) diff -r 3ff88fece1f6 -r ecefb68dc21d src/Tools/VSCode/src/vscode_resources.scala --- 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()) diff -r 3ff88fece1f6 -r ecefb68dc21d src/Tools/jEdit/src/isabelle.scala --- 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) diff -r 3ff88fece1f6 -r ecefb68dc21d src/Tools/jEdit/src/jedit_resources.scala --- 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 */ diff -r 3ff88fece1f6 -r ecefb68dc21d src/Tools/jEdit/src/theories_dockable.scala --- 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)) }) diff -r 3ff88fece1f6 -r ecefb68dc21d src/Tools/jEdit/src/timing_dockable.scala --- 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)