synthesize session with all required theories from other session imports;
authorwenzelm
Tue Oct 31 20:57:44 2017 +0100 (19 months ago)
changeset 66967e365c91c72a9
parent 66966 f3f9a492bee6
child 66968 9991671c98aa
synthesize session with all required theories from other session imports;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 19:29:24 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 20:57:44 2017 +0100
     1.3 @@ -123,8 +123,9 @@
     1.4      def platform_path: Base = copy(known = known.platform_path)
     1.5      def standard_path: Base = copy(known = known.standard_path)
     1.6  
     1.7 -    def theory_qualifier(name: Document.Node.Name): String =
     1.8 -      global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     1.9 +    def theory_qualifier(name: String): String =
    1.10 +      global_theories.getOrElse(name, Long_Name.qualifier(name))
    1.11 +    def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
    1.12  
    1.13      def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
    1.14      def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
    1.15 @@ -349,6 +350,42 @@
    1.16  
    1.17      def errors: List[String] = deps.errors
    1.18      def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    1.19 +
    1.20 +    def imported_session: Option[Info] =
    1.21 +    {
    1.22 +      val info = sessions(session)
    1.23 +
    1.24 +      val parent_loaded =
    1.25 +        info.parent match {
    1.26 +          case Some(parent) => deps(parent).loaded_theories.defined(_)
    1.27 +          case None => (_: String) => false
    1.28 +        }
    1.29 +      val imported_theories =
    1.30 +        for {
    1.31 +          thy <- base.loaded_theories.keys
    1.32 +          if !parent_loaded(thy) && base.theory_qualifier(thy) != session
    1.33 +        }
    1.34 +        yield (List.empty[Options.Spec], List(((thy, Position.none), false)))
    1.35 +
    1.36 +      if (imported_theories.isEmpty) None
    1.37 +      else
    1.38 +        Some(
    1.39 +          make_info(info.options,
    1.40 +            dir_selected = false,
    1.41 +            dir = info.dir,
    1.42 +            chapter = info.chapter,
    1.43 +            Session_Entry(
    1.44 +              pos = info.pos,
    1.45 +              name = info.name + "(base)",
    1.46 +              groups = info.groups,
    1.47 +              path = ".",
    1.48 +              parent = info.parent,
    1.49 +              description = "All required theories from other session imports",
    1.50 +              options = Nil,
    1.51 +              imports = info.imports,
    1.52 +              theories = imported_theories,
    1.53 +              document_files = Nil)))
    1.54 +    }
    1.55    }
    1.56  
    1.57  
    1.58 @@ -375,6 +412,53 @@
    1.59      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    1.60    }
    1.61  
    1.62 +  def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String,
    1.63 +    entry: Session_Entry): Info =
    1.64 +  {
    1.65 +    try {
    1.66 +      val name = entry.name
    1.67 +
    1.68 +      if (name == "" || name == DRAFT) error("Bad session name")
    1.69 +      if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    1.70 +      if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    1.71 +
    1.72 +      val session_options = options ++ entry.options
    1.73 +
    1.74 +      val theories =
    1.75 +        entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
    1.76 +
    1.77 +      val global_theories =
    1.78 +        for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
    1.79 +        yield {
    1.80 +          val thy_name = Path.explode(thy).expand.base_name
    1.81 +          if (Long_Name.is_qualified(thy_name))
    1.82 +            error("Bad qualified name for global theory " +
    1.83 +              quote(thy_name) + Position.here(pos))
    1.84 +          else thy_name
    1.85 +        }
    1.86 +
    1.87 +      val conditions =
    1.88 +        theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
    1.89 +          map(x => (x, Isabelle_System.getenv(x) != ""))
    1.90 +
    1.91 +      val document_files =
    1.92 +        entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.93 +
    1.94 +      val meta_digest =
    1.95 +        SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
    1.96 +          entry.theories_no_position, conditions, entry.document_files).toString)
    1.97 +
    1.98 +      Info(name, chapter, dir_selected, entry.pos, entry.groups,
    1.99 +        dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
   1.100 +        entry.imports, theories, global_theories, document_files, meta_digest)
   1.101 +    }
   1.102 +    catch {
   1.103 +      case ERROR(msg) =>
   1.104 +        error(msg + "\nThe error(s) above occurred in session entry " +
   1.105 +          quote(entry.name) + Position.here(entry.pos))
   1.106 +    }
   1.107 +  }
   1.108 +
   1.109    object Selection
   1.110    {
   1.111      val empty: Selection = Selection()
   1.112 @@ -641,57 +725,12 @@
   1.113  
   1.114    def read_root(options: Options, select: Boolean, path: Path): List[Info] =
   1.115    {
   1.116 -    def make_info(entry_chapter: String, entry: Session_Entry): Info =
   1.117 -    {
   1.118 -      try {
   1.119 -        val name = entry.name
   1.120 -
   1.121 -        if (name == "" || name == DRAFT) error("Bad session name")
   1.122 -        if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
   1.123 -        if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
   1.124 -
   1.125 -        val session_options = options ++ entry.options
   1.126 -
   1.127 -        val theories =
   1.128 -          entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
   1.129 -
   1.130 -        val global_theories =
   1.131 -          for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
   1.132 -          yield {
   1.133 -            val thy_name = Path.explode(thy).expand.base_name
   1.134 -            if (Long_Name.is_qualified(thy_name))
   1.135 -              error("Bad qualified name for global theory " +
   1.136 -                quote(thy_name) + Position.here(pos))
   1.137 -            else thy_name
   1.138 -          }
   1.139 -
   1.140 -        val conditions =
   1.141 -          theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
   1.142 -            map(x => (x, Isabelle_System.getenv(x) != ""))
   1.143 -
   1.144 -        val document_files =
   1.145 -          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   1.146 -
   1.147 -        val meta_digest =
   1.148 -          SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
   1.149 -            entry.theories_no_position, conditions, entry.document_files).toString)
   1.150 -
   1.151 -        Info(name, entry_chapter, select, entry.pos, entry.groups,
   1.152 -          path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
   1.153 -          entry.imports, theories, global_theories, document_files, meta_digest)
   1.154 -      }
   1.155 -      catch {
   1.156 -        case ERROR(msg) =>
   1.157 -          error(msg + "\nThe error(s) above occurred in session entry " +
   1.158 -            quote(entry.name) + Position.here(entry.pos))
   1.159 -      }
   1.160 -    }
   1.161 -
   1.162      var entry_chapter = "Unsorted"
   1.163      val infos = new mutable.ListBuffer[Info]
   1.164      parse_root(path).foreach {
   1.165        case Chapter(name) => entry_chapter = name
   1.166 -      case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   1.167 +      case entry: Session_Entry =>
   1.168 +        infos += make_info(options, select, path.dir, entry_chapter, entry)
   1.169      }
   1.170      infos.toList
   1.171    }