# HG changeset patch # User wenzelm # Date 1483991265 -3600 # Node ID 5e9bf964510a4308f112f282008a051c998b23a9 # Parent 8fcc23e8e1d974390e33b482e3ade9ed1beb82c3 clarified modules; tuned; diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Pure/PIDE/resources.scala --- 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) diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Pure/Thy/sessions.scala --- 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( diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Pure/Tools/build.scala --- 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 */ diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Tools/VSCode/src/server.scala --- 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) diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Tools/VSCode/src/vscode_resources.scala --- 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()) diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Tools/jEdit/src/jedit_resources.scala --- 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 */ diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Tools/jEdit/src/jedit_sessions.scala --- 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(_)))) } diff -r 8fcc23e8e1d9 -r 5e9bf964510a src/Tools/jEdit/src/plugin.scala --- 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) {