clarified modules;
authorwenzelm
Mon Jan 09 20:47:45 2017 +0100 (2017-01-09)
changeset 648565e9bf964510a
parent 64855 8fcc23e8e1d9
child 64857 316d703f741d
clarified modules;
tuned;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Jan 09 20:31:00 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Jan 09 20:47:45 2017 +0100
     1.3 @@ -17,10 +17,10 @@
     1.4  {
     1.5    def thy_path(path: Path): Path = path.ext("thy")
     1.6  
     1.7 -  val empty: Resources = new Resources(Build.Session_Content.empty)
     1.8 +  val empty: Resources = new Resources(Sessions.Base.empty)
     1.9  }
    1.10  
    1.11 -class Resources(val base: Build.Session_Content, val log: Logger = No_Logger)
    1.12 +class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
    1.13  {
    1.14    val thy_info = new Thy_Info(this)
    1.15  
     2.1 --- a/src/Pure/Thy/sessions.scala	Mon Jan 09 20:31:00 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Mon Jan 09 20:47:45 2017 +0100
     2.3 @@ -29,6 +29,25 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* base info */
     2.8 +
     2.9 +  object Base
    2.10 +  {
    2.11 +    val empty: Base = Base()
    2.12 +
    2.13 +    lazy val bootstrap: Base =
    2.14 +      Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
    2.15 +  }
    2.16 +
    2.17 +  sealed case class Base(
    2.18 +    loaded_theories: Set[String] = Set.empty,
    2.19 +    known_theories: Map[String, Document.Node.Name] = Map.empty,
    2.20 +    keywords: Thy_Header.Keywords = Nil,
    2.21 +    syntax: Outer_Syntax = Outer_Syntax.empty,
    2.22 +    sources: List[(Path, SHA1.Digest)] = Nil,
    2.23 +    session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    2.24 +
    2.25 +
    2.26    /* info */
    2.27  
    2.28    sealed case class Info(
     3.1 --- a/src/Pure/Tools/build.scala	Mon Jan 09 20:31:00 2017 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Mon Jan 09 20:47:45 2017 +0100
     3.3 @@ -95,29 +95,10 @@
     3.4  
     3.5    /* source dependencies and static content */
     3.6  
     3.7 -  object Session_Content
     3.8 -  {
     3.9 -    val empty: Session_Content =
    3.10 -      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
    3.11 -        Nil, Graph_Display.empty_graph)
    3.12 -
    3.13 -    lazy val bootstrap: Session_Content =
    3.14 -      Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
    3.15 -        Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
    3.16 -  }
    3.17 -
    3.18 -  sealed case class Session_Content(
    3.19 -    loaded_theories: Set[String],
    3.20 -    known_theories: Map[String, Document.Node.Name],
    3.21 -    keywords: Thy_Header.Keywords,
    3.22 -    syntax: Outer_Syntax,
    3.23 -    sources: List[(Path, SHA1.Digest)],
    3.24 -    session_graph: Graph_Display.Graph)
    3.25 -
    3.26 -  sealed case class Deps(deps: Map[String, Session_Content])
    3.27 +  sealed case class Deps(deps: Map[String, Sessions.Base])
    3.28    {
    3.29      def is_empty: Boolean = deps.isEmpty
    3.30 -    def apply(name: String): Session_Content = deps(name)
    3.31 +    def apply(name: String): Sessions.Base = deps(name)
    3.32      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    3.33    }
    3.34  
    3.35 @@ -128,17 +109,17 @@
    3.36        list_files: Boolean = false,
    3.37        check_keywords: Set[String] = Set.empty,
    3.38        tree: Sessions.Tree): Deps =
    3.39 -    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    3.40 +    Deps((Map.empty[String, Sessions.Base] /: tree.topological_order)(
    3.41        { case (deps, (name, info)) =>
    3.42            if (progress.stopped) throw Exn.Interrupt()
    3.43  
    3.44            try {
    3.45 -            val base =
    3.46 -              info.parent match {
    3.47 -                case None => Session_Content.bootstrap
    3.48 -                case Some(parent) => deps(parent)
    3.49 -              }
    3.50 -            val resources = new Resources(base)
    3.51 +            val resources =
    3.52 +              new Resources(
    3.53 +                info.parent match {
    3.54 +                  case None => Sessions.Base.bootstrap
    3.55 +                  case Some(parent) => deps(parent)
    3.56 +                })
    3.57  
    3.58              if (verbose || list_files) {
    3.59                val groups =
    3.60 @@ -165,7 +146,7 @@
    3.61              }
    3.62  
    3.63              val known_theories =
    3.64 -              (base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    3.65 +              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    3.66                  val name = dep.name
    3.67                  known.get(name.theory) match {
    3.68                    case Some(name1) if name != name1 =>
    3.69 @@ -203,12 +184,13 @@
    3.70              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    3.71  
    3.72              val session_graph =
    3.73 -              Present.session_graph(info.parent getOrElse "", base.loaded_theories, thy_deps.deps)
    3.74 +              Present.session_graph(info.parent getOrElse "",
    3.75 +                resources.base.loaded_theories, thy_deps.deps)
    3.76  
    3.77 -            val content =
    3.78 -              Session_Content(loaded_theories, known_theories, keywords, syntax,
    3.79 -                sources, session_graph)
    3.80 -            deps + (name -> content)
    3.81 +            val base =
    3.82 +              Sessions.Base(
    3.83 +                loaded_theories, known_theories, keywords, syntax, sources, session_graph)
    3.84 +            deps + (name -> base)
    3.85            }
    3.86            catch {
    3.87              case ERROR(msg) =>
    3.88 @@ -227,17 +209,17 @@
    3.89      dependencies(inlined_files = inlined_files, tree = tree)
    3.90    }
    3.91  
    3.92 -  def session_content(
    3.93 +  def session_base(
    3.94      options: Options,
    3.95      inlined_files: Boolean,
    3.96      dirs: List[Path],
    3.97 -    session: String): Session_Content =
    3.98 +    session: String): Sessions.Base =
    3.99    {
   3.100      session_dependencies(options, inlined_files, dirs, List(session))(session)
   3.101    }
   3.102  
   3.103    def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
   3.104 -    session_content(options, false, dirs, session).syntax
   3.105 +    session_base(options, false, dirs, session).syntax
   3.106  
   3.107  
   3.108    /* jobs */
     4.1 --- a/src/Tools/VSCode/src/server.scala	Mon Jan 09 20:31:00 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Jan 09 20:47:45 2017 +0100
     4.3 @@ -199,9 +199,9 @@
     4.4            }
     4.5          }
     4.6  
     4.7 +        val base = Build.session_base(options, false, session_dirs, session_name)
     4.8          val resources =
     4.9 -          new VSCode_Resources(options, text_length,
    4.10 -            Build.session_content(options, false, session_dirs, session_name), log)
    4.11 +          new VSCode_Resources(options, text_length, base, log)
    4.12            {
    4.13              override def commit(change: Session.Change): Unit =
    4.14                if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
     5.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 09 20:31:00 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Jan 09 20:47:45 2017 +0100
     5.3 @@ -35,7 +35,7 @@
     5.4  class VSCode_Resources(
     5.5    val options: Options,
     5.6    val text_length: Text.Length,
     5.7 -  base: Build.Session_Content,
     5.8 +  base: Sessions.Base,
     5.9    log: Logger = No_Logger) extends Resources(base, log)
    5.10  {
    5.11    private val state = Synchronized(VSCode_Resources.State())
     6.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 20:31:00 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 20:47:45 2017 +0100
     6.3 @@ -23,10 +23,10 @@
     6.4  
     6.5  object JEdit_Resources
     6.6  {
     6.7 -  val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
     6.8 +  val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
     6.9  }
    6.10  
    6.11 -class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
    6.12 +class JEdit_Resources(base: Sessions.Base) extends Resources(base)
    6.13  {
    6.14    /* document node name */
    6.15  
     7.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jan 09 20:31:00 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jan 09 20:47:45 2017 +0100
     7.3 @@ -79,15 +79,12 @@
     7.4      main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
     7.5    }
     7.6  
     7.7 -  def session_content(inlined_files: Boolean): Build.Session_Content =
     7.8 +  def session_base(inlined_files: Boolean): Sessions.Base =
     7.9    {
    7.10 -    val content =
    7.11 -      try {
    7.12 -        Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
    7.13 -      }
    7.14 -      catch { case ERROR(_) => Build.Session_Content.empty }
    7.15 -    content.copy(known_theories =
    7.16 -      content.known_theories.mapValues(name => name.map(File.platform_path(_))))
    7.17 +    val base =
    7.18 +      try { Build.session_base(PIDE.options.value, inlined_files, session_dirs(), session_name()) }
    7.19 +      catch { case ERROR(_) => Sessions.Base.empty }
    7.20 +    base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
    7.21    }
    7.22  
    7.23  
     8.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 20:31:00 2017 +0100
     8.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 20:47:45 2017 +0100
     8.3 @@ -386,7 +386,7 @@
     8.4  
     8.5        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
     8.6  
     8.7 -      val resources = new JEdit_Resources(JEdit_Sessions.session_content(false))
     8.8 +      val resources = new JEdit_Resources(JEdit_Sessions.session_base(false))
     8.9  
    8.10        PIDE.session.stop()
    8.11        PIDE.session = new Session(resources) {