tuned;
authorwenzelm
Sun Nov 12 12:55:10 2017 +0100 (20 months ago)
changeset 6705357c37ee49c39
parent 67052 caf87d4b9b61
child 67054 9498b7522a99
tuned;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Nov 12 12:41:05 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 12:55:10 2017 +0100
     1.3 @@ -310,21 +310,23 @@
     1.4        "The error(s) above occurred for theory " + quote(name.theory) +
     1.5          required_by(initiators) + Position.here(pos)
     1.6  
     1.7 -    val required1 = required + name
     1.8      if (required.seen(name)) required
     1.9 -    else if (session_base.loaded_theory(name)) required1
    1.10      else {
    1.11 -      try {
    1.12 -        if (initiators.contains(name)) error(cycle_msg(initiators))
    1.13 -        val header =
    1.14 -          try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
    1.15 -          catch { case ERROR(msg) => cat_error(msg, message) }
    1.16 -        Document.Node.Entry(name, header) ::
    1.17 -          require_thys(name :: initiators, required1, header.imports)
    1.18 -      }
    1.19 -      catch {
    1.20 -        case e: Throwable =>
    1.21 -          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
    1.22 +      val required1 = required + name
    1.23 +      if (session_base.loaded_theory(name)) required1
    1.24 +      else {
    1.25 +        try {
    1.26 +          if (initiators.contains(name)) error(cycle_msg(initiators))
    1.27 +          val header =
    1.28 +            try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
    1.29 +            catch { case ERROR(msg) => cat_error(msg, message) }
    1.30 +          Document.Node.Entry(name, header) ::
    1.31 +            require_thys(name :: initiators, required1, header.imports)
    1.32 +        }
    1.33 +        catch {
    1.34 +          case e: Throwable =>
    1.35 +            Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
    1.36 +        }
    1.37        }
    1.38      }
    1.39    }
     2.1 --- a/src/Pure/Thy/sessions.scala	Sun Nov 12 12:41:05 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sun Nov 12 12:55:10 2017 +0100
     2.3 @@ -227,21 +227,21 @@
     2.4                progress.echo("Session " + info.chapter + "/" + info.name + groups)
     2.5              }
     2.6  
     2.7 -            val thy_deps =
     2.8 +            val dependencies =
     2.9                resources.dependencies(
    2.10                  for { (_, thys) <- info.theories; (thy, pos) <- thys }
    2.11                  yield (resources.import_name(info.name, info.dir.implode, thy), pos))
    2.12  
    2.13 -            val overall_syntax = thy_deps.overall_syntax
    2.14 +            val overall_syntax = dependencies.overall_syntax
    2.15  
    2.16 -            val theory_files = thy_deps.names.map(_.path)
    2.17 +            val theory_files = dependencies.names.map(_.path)
    2.18              val loaded_files =
    2.19                if (inlined_files) {
    2.20                  if (Sessions.is_pure(info.name)) {
    2.21                    (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
    2.22 -                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    2.23 +                    dependencies.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    2.24                  }
    2.25 -                else thy_deps.loaded_files
    2.26 +                else dependencies.loaded_files
    2.27                }
    2.28                else Nil
    2.29  
    2.30 @@ -249,7 +249,7 @@
    2.31                (theory_files ::: loaded_files.flatMap(_._2) :::
    2.32                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    2.33  
    2.34 -            val imported_files = if (inlined_files) thy_deps.imported_files else Nil
    2.35 +            val imported_files = if (inlined_files) dependencies.imported_files else Nil
    2.36  
    2.37              if (list_files)
    2.38                progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
    2.39 @@ -283,7 +283,7 @@
    2.40                        val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
    2.41                        ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    2.42  
    2.43 -              (graph0 /: thy_deps.entries)(
    2.44 +              (graph0 /: dependencies.entries)(
    2.45                  { case (g, entry) =>
    2.46                      val a = node(entry.name)
    2.47                      val bs =
    2.48 @@ -294,7 +294,7 @@
    2.49  
    2.50              val known =
    2.51                Known.make(info.dir, List(imports_base),
    2.52 -                theories = thy_deps.names,
    2.53 +                theories = dependencies.names,
    2.54                  loaded_files = loaded_files)
    2.55  
    2.56              val sources_errors =
    2.57 @@ -304,13 +304,13 @@
    2.58                Base(
    2.59                  pos = info.pos,
    2.60                  global_theories = global_theories,
    2.61 -                loaded_theories = thy_deps.loaded_theories,
    2.62 +                loaded_theories = dependencies.loaded_theories,
    2.63                  known = known,
    2.64                  overall_syntax = overall_syntax,
    2.65                  imported_sources = check_sources(imported_files),
    2.66                  sources = check_sources(session_files),
    2.67                  session_graph_display = session_graph_display,
    2.68 -                errors = thy_deps.errors ::: sources_errors,
    2.69 +                errors = dependencies.errors ::: sources_errors,
    2.70                  imports = Some(imports_base))
    2.71  
    2.72              session_bases + (info.name -> base)