tuned signature;
authorwenzelm
Tue Nov 07 16:50:26 2017 +0100 (18 months ago)
changeset 67026687c822ee5e3
parent 67025 961285f581e6
child 67027 d4f245bea081
tuned signature;
src/Pure/Admin/afp.scala
src/Pure/Admin/build_doc.scala
src/Pure/ML/ml_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Tue Nov 07 16:44:25 2017 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Tue Nov 07 16:50:26 2017 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val sessions: List[String] = entries.flatMap(_.sessions)
     1.5  
     1.6    val sessions_structure: Sessions.T =
     1.7 -    Sessions.load(options, dirs = List(main_dir)).
     1.8 +    Sessions.load_structure(options, dirs = List(main_dir)).
     1.9        selection(Sessions.Selection(sessions = sessions.toList))
    1.10  
    1.11  
     2.1 --- a/src/Pure/Admin/build_doc.scala	Tue Nov 07 16:44:25 2017 +0100
     2.2 +++ b/src/Pure/Admin/build_doc.scala	Tue Nov 07 16:50:26 2017 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4      system_mode: Boolean = false,
     2.5      docs: List[String] = Nil): Int =
     2.6    {
     2.7 -    val sessions_structure = Sessions.load(options)
     2.8 +    val sessions_structure = Sessions.load_structure(options)
     2.9      val selection =
    2.10        for {
    2.11          name <- sessions_structure.build_topological_order
     3.1 --- a/src/Pure/ML/ml_process.scala	Tue Nov 07 16:44:25 2017 +0100
     3.2 +++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 16:50:26 2017 +0100
     3.3 @@ -33,7 +33,7 @@
     3.4        else {
     3.5          val selection = Sessions.Selection(sessions = List(logic_name))
     3.6          val selected_sessions =
     3.7 -          sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
     3.8 +          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
     3.9          selected_sessions.build_requirements(List(logic_name)).
    3.10            map(a => File.platform_path(store.heap(a)))
    3.11        }
     4.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 16:44:25 2017 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 16:50:26 2017 +0100
     4.3 @@ -345,7 +345,7 @@
     4.4      focus_session: Boolean = false,
     4.5      required_session: Boolean = false): Base_Info =
     4.6    {
     4.7 -    val full_sessions = load(options, dirs = dirs)
     4.8 +    val full_sessions = load_structure(options, dirs = dirs)
     4.9      val global_theories = full_sessions.global_theories
    4.10  
    4.11      val selected_sessions =
    4.12 @@ -400,7 +400,7 @@
    4.13  
    4.14      val full_sessions1 =
    4.15        if (infos1.isEmpty) full_sessions
    4.16 -      else load(options, dirs = dirs, infos = infos1)
    4.17 +      else load_structure(options, dirs = dirs, infos = infos1)
    4.18  
    4.19      val select_sessions1 =
    4.20        if (focus_session) full_sessions1.imports_descendants(List(session1))
    4.21 @@ -784,7 +784,7 @@
    4.22      (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    4.23    }
    4.24  
    4.25 -  def load(options: Options,
    4.26 +  def load_structure(options: Options,
    4.27      dirs: List[Path] = Nil,
    4.28      select_dirs: List[Path] = Nil,
    4.29      infos: List[Info] = Nil): T =
     5.1 --- a/src/Pure/Tools/build.scala	Tue Nov 07 16:44:25 2017 +0100
     5.2 +++ b/src/Pure/Tools/build.scala	Tue Nov 07 16:50:26 2017 +0100
     5.3 @@ -382,7 +382,7 @@
     5.4      /* session selection and dependencies */
     5.5  
     5.6      val full_sessions =
     5.7 -      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
     5.8 +      Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
     5.9  
    5.10      def sources_stamp(deps: Sessions.Deps, name: String): String =
    5.11      {
     6.1 --- a/src/Pure/Tools/imports.scala	Tue Nov 07 16:44:25 2017 +0100
     6.2 +++ b/src/Pure/Tools/imports.scala	Tue Nov 07 16:50:26 2017 +0100
     6.3 @@ -99,7 +99,7 @@
     6.4      select_dirs: List[Path] = Nil,
     6.5      verbose: Boolean = false) =
     6.6    {
     6.7 -    val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
     6.8 +    val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
     6.9      val selected_sessions = full_sessions.selection(selection)
    6.10  
    6.11      val deps =
    6.12 @@ -312,8 +312,8 @@
    6.13            verbose = verbose)
    6.14        }
    6.15        else if (operation_update && incremental_update) {
    6.16 -        Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection).
    6.17 -          imports_topological_order.foreach(name =>
    6.18 +        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
    6.19 +          selection(selection).imports_topological_order.foreach(name =>
    6.20              {
    6.21                imports(options, operation_update = operation_update, progress = progress,
    6.22                  update_message = " for session " + quote(name),
     7.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 16:44:25 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 16:50:26 2017 +0100
     7.3 @@ -45,7 +45,10 @@
     7.4    def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
     7.5  
     7.6    def logic_info(options: Options): Option[Sessions.Info] =
     7.7 -    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
     7.8 +    try {
     7.9 +      Sessions.load_structure(session_options(options), dirs = session_dirs()).
    7.10 +        get(logic_name(options))
    7.11 +    }
    7.12      catch { case ERROR(_) => None }
    7.13  
    7.14    def logic_root(options: Options): Position.T =
    7.15 @@ -68,7 +71,7 @@
    7.16  
    7.17      val session_list =
    7.18      {
    7.19 -      val sessions_structure = Sessions.load(options.value, dirs = session_dirs())
    7.20 +      val sessions_structure = Sessions.load_structure(options.value, dirs = session_dirs())
    7.21        val (main_sessions, other_sessions) =
    7.22          sessions_structure.imports_topological_order.
    7.23            partition(name => sessions_structure(name).groups.contains("main"))