src/Pure/Thy/sessions.scala
changeset 66571 0fdeb24e535e
parent 66243 453f9cabddb5
child 66573 a6401a6417cf
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Aug 31 11:42:10 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Aug 31 16:30:46 2017 +0200
     1.3 @@ -100,6 +100,7 @@
     1.4    }
     1.5  
     1.6    sealed case class Base(
     1.7 +    pos: Position.T = Position.none,
     1.8      imports: Option[Base] = None,
     1.9      global_theories: Map[String, String] = Map.empty,
    1.10      loaded_theories: Map[String, String] = Map.empty,
    1.11 @@ -107,7 +108,8 @@
    1.12      keywords: Thy_Header.Keywords = Nil,
    1.13      syntax: Outer_Syntax = Outer_Syntax.empty,
    1.14      sources: List[(Path, SHA1.Digest)] = Nil,
    1.15 -    session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    1.16 +    session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    1.17 +    errors: List[String] = Nil)
    1.18    {
    1.19      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.20  
    1.21 @@ -129,6 +131,20 @@
    1.22      def is_empty: Boolean = session_bases.isEmpty
    1.23      def apply(name: String): Base = session_bases(name)
    1.24      def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2)
    1.25 +
    1.26 +    def errors: List[String] =
    1.27 +      (for {
    1.28 +        (name, base) <- session_bases.iterator
    1.29 +        if base.errors.nonEmpty
    1.30 +      } yield cat_lines(base.errors) +
    1.31 +          "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
    1.32 +      ).toList
    1.33 +
    1.34 +    def check_errors: Deps =
    1.35 +      errors match {
    1.36 +        case Nil => this
    1.37 +        case errs => error(cat_lines(errs))
    1.38 +      }
    1.39    }
    1.40  
    1.41    def deps(sessions: T,
    1.42 @@ -171,12 +187,7 @@
    1.43                    thys.map({ case (thy, pos) =>
    1.44                      (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
    1.45                  })
    1.46 -              val thy_deps = resources.thy_info.dependencies(root_theories)
    1.47 -
    1.48 -              thy_deps.errors match {
    1.49 -                case Nil => thy_deps
    1.50 -                case errs => error(cat_lines(errs))
    1.51 -              }
    1.52 +              resources.thy_info.dependencies(root_theories)
    1.53              }
    1.54  
    1.55              val syntax = thy_deps.syntax
    1.56 @@ -242,14 +253,17 @@
    1.57              }
    1.58  
    1.59              val base =
    1.60 -              Base(imports = Some(imports_base),
    1.61 +              Base(
    1.62 +                pos = info.pos,
    1.63 +                imports = Some(imports_base),
    1.64                  global_theories = global_theories,
    1.65                  loaded_theories = thy_deps.loaded_theories,
    1.66                  known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.67                  keywords = thy_deps.keywords,
    1.68                  syntax = syntax,
    1.69                  sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.70 -                session_graph = session_graph)
    1.71 +                session_graph = session_graph,
    1.72 +                errors = thy_deps.errors)
    1.73  
    1.74              session_bases + (info.name -> base)
    1.75            }
    1.76 @@ -265,11 +279,11 @@
    1.77        else Known.empty)
    1.78    }
    1.79  
    1.80 -  def session_base(
    1.81 +  def session_base_errors(
    1.82      options: Options,
    1.83      session: String,
    1.84      dirs: List[Path] = Nil,
    1.85 -    all_known: Boolean = false): Base =
    1.86 +    all_known: Boolean = false): (List[String], Base) =
    1.87    {
    1.88      val full_sessions = load(options, dirs = dirs)
    1.89      val global_theories = full_sessions.global_theories
    1.90 @@ -278,10 +292,25 @@
    1.91      if (all_known) {
    1.92        val deps =
    1.93          Sessions.deps(full_sessions, global_theories = global_theories, all_known = all_known)
    1.94 -      deps(session).copy(known = deps.all_known)
    1.95 +      (deps.errors, deps(session).copy(known = deps.all_known))
    1.96 +    }
    1.97 +    else {
    1.98 +      val deps =
    1.99 +        Sessions.deps(selected_sessions, global_theories = global_theories)
   1.100 +      (deps.errors, deps(session))
   1.101      }
   1.102 -    else
   1.103 -      deps(selected_sessions, global_theories = global_theories)(session)
   1.104 +  }
   1.105 +
   1.106 +  def session_base(
   1.107 +    options: Options,
   1.108 +    session: String,
   1.109 +    dirs: List[Path] = Nil,
   1.110 +    all_known: Boolean = false): Base =
   1.111 +  {
   1.112 +    session_base_errors(options, session, dirs = dirs, all_known = all_known) match {
   1.113 +      case (Nil, base) => base
   1.114 +      case (errs, _) => error(cat_lines(errs))
   1.115 +    }
   1.116    }
   1.117  
   1.118