clarified signature;
authorwenzelm
Tue Oct 31 19:29:24 2017 +0100 (18 months ago)
changeset 66966f3f9a492bee6
parent 66965 9cec50354099
child 66967 e365c91c72a9
clarified signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Oct 31 18:56:24 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Oct 31 19:29:24 2017 +0100
     1.3 @@ -452,12 +452,16 @@
     1.4              val completion =
     1.5                if (Thy_Header.is_base_name(s)) {
     1.6                  val completed = Completion.completed(import_name.theory_base_name)
     1.7 -                val qualifier = resources.theory_qualifier(node_name)
     1.8 +                val qualifier = resources.session_base.theory_qualifier(node_name)
     1.9                  val dir = node_name.master_dir
    1.10                  for {
    1.11                    (_, known_name) <- resources.session_base.known.theories.toList
    1.12                    if completed(known_name.theory_base_name)
    1.13 -                } yield resources.standard_import(resources, qualifier, dir, known_name.theory)
    1.14 +                }
    1.15 +                yield {
    1.16 +                  resources.standard_import(
    1.17 +                    resources.session_base, qualifier, dir, known_name.theory)
    1.18 +                }
    1.19                }.sorted
    1.20                else Nil
    1.21              val msg =
     2.1 --- a/src/Pure/PIDE/resources.scala	Tue Oct 31 18:56:24 2017 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Tue Oct 31 19:29:24 2017 +0100
     2.3 @@ -86,9 +86,6 @@
     2.4      roots ::: files
     2.5    }
     2.6  
     2.7 -  def theory_qualifier(name: Document.Node.Name): String =
     2.8 -    session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     2.9 -
    2.10    def theory_name(qualifier: String, theory: String): (Boolean, String) =
    2.11      if (session_base.loaded_theory(theory)) (true, theory)
    2.12      else {
    2.13 @@ -118,10 +115,9 @@
    2.14      }
    2.15  
    2.16    def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
    2.17 -    import_name(theory_qualifier(name), name.master_dir, s)
    2.18 +    import_name(session_base.theory_qualifier(name), name.master_dir, s)
    2.19  
    2.20 -  def standard_import(session_resources: Resources,
    2.21 -    qualifier: String, dir: String, s: String): String =
    2.22 +  def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
    2.23    {
    2.24      val name = import_name(qualifier, dir, s)
    2.25      val s1 =
    2.26 @@ -131,7 +127,7 @@
    2.27            case None => s
    2.28            case Some(path) =>
    2.29              session_base.known.get_file(path.file) match {
    2.30 -              case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    2.31 +              case Some(name1) if base.theory_qualifier(name1) != qualifier =>
    2.32                  name1.theory
    2.33                case Some(name1) if Thy_Header.is_base_name(s) =>
    2.34                  name1.theory_base_name
     3.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 18:56:24 2017 +0100
     3.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 19:29:24 2017 +0100
     3.3 @@ -123,6 +123,9 @@
     3.4      def platform_path: Base = copy(known = known.platform_path)
     3.5      def standard_path: Base = copy(known = known.standard_path)
     3.6  
     3.7 +    def theory_qualifier(name: Document.Node.Name): String =
     3.8 +      global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     3.9 +
    3.10      def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
    3.11      def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
    3.12  
    3.13 @@ -260,7 +263,7 @@
    3.14  
    3.15                def node(name: Document.Node.Name): Graph_Display.Node =
    3.16                {
    3.17 -                val qualifier = resources.theory_qualifier(name)
    3.18 +                val qualifier = imports_base.theory_qualifier(name)
    3.19                  if (qualifier == info.name)
    3.20                    Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    3.21                  else session_node(qualifier)
     4.1 --- a/src/Pure/Tools/imports.scala	Tue Oct 31 18:56:24 2017 +0100
     4.2 +++ b/src/Pure/Tools/imports.scala	Tue Oct 31 19:29:24 2017 +0100
     4.3 @@ -113,24 +113,23 @@
     4.4        {
     4.5          val info = selected_sessions(session_name)
     4.6          val session_base = deps(session_name)
     4.7 -        val session_resources = new Resources(session_base)
     4.8  
     4.9          val declared_imports =
    4.10            selected_sessions.imports_requirements(List(session_name)).toSet
    4.11  
    4.12          val extra_imports =
    4.13            (for {
    4.14 -            (_, a) <- session_resources.session_base.known.theories.iterator
    4.15 -            if session_resources.theory_qualifier(a) == info.name
    4.16 +            (_, a) <- session_base.known.theories.iterator
    4.17 +            if session_base.theory_qualifier(a) == info.name
    4.18              b <- deps.all_known.get_file(a.path.file)
    4.19 -            qualifier = session_resources.theory_qualifier(b)
    4.20 +            qualifier = session_base.theory_qualifier(b)
    4.21              if !declared_imports.contains(qualifier)
    4.22            } yield qualifier).toSet
    4.23  
    4.24          val loaded_imports =
    4.25            selected_sessions.imports_requirements(
    4.26              session_base.loaded_theories.keys.map(a =>
    4.27 -              session_resources.theory_qualifier(session_base.known.theories(a))))
    4.28 +              session_base.theory_qualifier(session_base.known.theories(a))))
    4.29            .toSet - session_name
    4.30  
    4.31          val minimal_imports =
    4.32 @@ -182,7 +181,7 @@
    4.33            val imports_resources = new Resources(imports_base)
    4.34  
    4.35            def standard_import(qualifier: String, dir: String, s: String): String =
    4.36 -            imports_resources.standard_import(session_resources, qualifier, dir, s)
    4.37 +            imports_resources.standard_import(session_base, qualifier, dir, s)
    4.38  
    4.39            val updates_root =
    4.40              for {
    4.41 @@ -193,10 +192,10 @@
    4.42            val updates_theories =
    4.43              for {
    4.44                (_, name) <- session_base.known.theories_local.toList
    4.45 -              if session_resources.theory_qualifier(name) == info.name
    4.46 +              if session_base.theory_qualifier(name) == info.name
    4.47                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    4.48                upd <- update_name(session_base.overall_syntax.keywords, pos,
    4.49 -                standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
    4.50 +                standard_import(session_base.theory_qualifier(name), name.master_dir, _))
    4.51              } yield upd
    4.52  
    4.53            updates_root ::: updates_theories