tuned signature;
authorwenzelm
Sun Nov 12 12:41:05 2017 +0100 (18 months ago)
changeset 67052caf87d4b9b61
parent 67051 e7e54a0b9197
child 67053 57c37ee49c39
tuned signature;
src/Pure/Admin/afp.scala
src/Pure/ML/ml_process.scala
src/Pure/System/isabelle_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Sat Nov 11 18:41:08 2017 +0000
     1.2 +++ b/src/Pure/Admin/afp.scala	Sun Nov 12 12:41:05 2017 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5    val sessions: List[String] = entries.flatMap(_.sessions)
     1.6  
     1.7 -  val sessions_structure: Sessions.T =
     1.8 +  val sessions_structure: Sessions.Structure =
     1.9      Sessions.load_structure(options, dirs = List(main_dir)).
    1.10        selection(Sessions.Selection(sessions = sessions.toList))
    1.11  
     2.1 --- a/src/Pure/ML/ml_process.scala	Sat Nov 11 18:41:08 2017 +0000
     2.2 +++ b/src/Pure/ML/ml_process.scala	Sun Nov 12 12:41:05 2017 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4      redirect: Boolean = false,
     2.5      cleanup: () => Unit = () => (),
     2.6      channel: Option[System_Channel] = None,
     2.7 -    sessions: Option[Sessions.T] = None,
     2.8 +    sessions: Option[Sessions.Structure] = None,
     2.9      session_base: Option[Sessions.Base] = None,
    2.10      store: Sessions.Store = Sessions.store()): Bash.Process =
    2.11    {
     3.1 --- a/src/Pure/System/isabelle_process.scala	Sat Nov 11 18:41:08 2017 +0000
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Nov 12 12:41:05 2017 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4      modes: List[String] = Nil,
     3.5      cwd: JFile = null,
     3.6      env: Map[String, String] = Isabelle_System.settings(),
     3.7 -    sessions: Option[Sessions.T] = None,
     3.8 +    sessions: Option[Sessions.Structure] = None,
     3.9      store: Sessions.Store = Sessions.store(),
    3.10      phase_changed: Session.Phase => Unit = null)
    3.11    {
    3.12 @@ -43,7 +43,7 @@
    3.13      env: Map[String, String] = Isabelle_System.settings(),
    3.14      receiver: Prover.Receiver = Console.println(_),
    3.15      xml_cache: XML.Cache = new XML.Cache(),
    3.16 -    sessions: Option[Sessions.T] = None,
    3.17 +    sessions: Option[Sessions.Structure] = None,
    3.18      store: Sessions.Store = Sessions.store()): Prover =
    3.19    {
    3.20      val channel = System_Channel()
     4.1 --- a/src/Pure/Thy/sessions.scala	Sat Nov 11 18:41:08 2017 +0000
     4.2 +++ b/src/Pure/Thy/sessions.scala	Sun Nov 12 12:41:05 2017 +0100
     4.3 @@ -175,7 +175,7 @@
     4.4        }
     4.5    }
     4.6  
     4.7 -  def deps(sessions_structure: T,
     4.8 +  def deps(sessions_structure: Structure,
     4.9        global_theories: Map[String, String],
    4.10        progress: Progress = No_Progress,
    4.11        inlined_files: Boolean = false,
    4.12 @@ -330,7 +330,7 @@
    4.13  
    4.14    sealed case class Base_Info(
    4.15      session: String,
    4.16 -    sessions_structure: T,
    4.17 +    sessions_structure: Structure,
    4.18      errors: List[String],
    4.19      base: Base,
    4.20      infos: List[Info])
    4.21 @@ -542,7 +542,7 @@
    4.22      }
    4.23    }
    4.24  
    4.25 -  def make(infos: List[Info]): T =
    4.26 +  def make(infos: List[Info]): Structure =
    4.27    {
    4.28      def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
    4.29        : Graph[String, Info] =
    4.30 @@ -577,10 +577,10 @@
    4.31      val graph1 = add_edges(graph0, "parent", _.parent)
    4.32      val graph2 = add_edges(graph1, "imports", _.imports)
    4.33  
    4.34 -    new T(graph1, graph2)
    4.35 +    new Structure(graph1, graph2)
    4.36    }
    4.37  
    4.38 -  final class T private[Sessions](
    4.39 +  final class Structure private[Sessions](
    4.40        val build_graph: Graph[String, Info],
    4.41        val imports_graph: Graph[String, Info])
    4.42    {
    4.43 @@ -606,7 +606,7 @@
    4.44                }
    4.45            })
    4.46  
    4.47 -    def selection(sel: Selection): T =
    4.48 +    def selection(sel: Selection): Structure =
    4.49      {
    4.50        val bad_sessions =
    4.51          SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
    4.52 @@ -622,7 +622,7 @@
    4.53          graph.restrict(graph.all_preds(sessions).toSet)
    4.54        }
    4.55  
    4.56 -      new T(restrict(build_graph), restrict(imports_graph))
    4.57 +      new Structure(restrict(build_graph), restrict(imports_graph))
    4.58      }
    4.59  
    4.60      def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
    4.61 @@ -636,7 +636,7 @@
    4.62      def imports_topological_order: List[String] = imports_graph.topological_order
    4.63  
    4.64      override def toString: String =
    4.65 -      imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
    4.66 +      imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
    4.67    }
    4.68  
    4.69  
    4.70 @@ -788,7 +788,7 @@
    4.71    def load_structure(options: Options,
    4.72      dirs: List[Path] = Nil,
    4.73      select_dirs: List[Path] = Nil,
    4.74 -    infos: List[Info] = Nil): T =
    4.75 +    infos: List[Info] = Nil): Structure =
    4.76    {
    4.77      def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
    4.78        load_root(select, dir) ::: load_roots(select, dir)
     5.1 --- a/src/Pure/Tools/build.scala	Sat Nov 11 18:41:08 2017 +0000
     5.2 +++ b/src/Pure/Tools/build.scala	Sun Nov 12 12:41:05 2017 +0100
     5.3 @@ -71,7 +71,7 @@
     5.4        }
     5.5      }
     5.6  
     5.7 -    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
     5.8 +    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
     5.9      {
    5.10        val graph = sessions.build_graph
    5.11        val names = graph.keys
    5.12 @@ -178,7 +178,7 @@
    5.13    private class Job(progress: Progress,
    5.14      name: String,
    5.15      val info: Sessions.Info,
    5.16 -    sessions: Sessions.T,
    5.17 +    sessions: Sessions.Structure,
    5.18      deps: Sessions.Deps,
    5.19      store: Sessions.Store,
    5.20      do_output: Boolean,