clarified modules;
authorwenzelm
Tue Oct 31 15:55:50 2017 +0100 (19 months ago)
changeset 66959015d47486fc8
parent 66958 86bc3f1ec97e
child 66960 d62f1f03868a
clarified modules;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
src/Pure/build-jars
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Oct 31 15:36:50 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Oct 31 15:55:50 2017 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4    val session_base: Sessions.Base,
     1.5    val log: Logger = No_Logger)
     1.6  {
     1.7 -  val thy_info = new Thy_Info(this)
     1.8 +  resources =>
     1.9  
    1.10    def thy_path(path: Path): Path = path.ext("thy")
    1.11  
    1.12 @@ -213,7 +213,113 @@
    1.13        previous: Document.Version,
    1.14        doc_blobs: Document.Blobs,
    1.15        edits: List[Document.Edit_Text]): Session.Change =
    1.16 -    Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
    1.17 +    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits)
    1.18  
    1.19    def commit(change: Session.Change) { }
    1.20 +
    1.21 +
    1.22 +  /* theory and file dependencies */
    1.23 +
    1.24 +  object Dependencies
    1.25 +  {
    1.26 +    val empty = new Dependencies(Nil, Set.empty)
    1.27 +  }
    1.28 +
    1.29 +  final class Dependencies private(
    1.30 +    rev_entries: List[Document.Node.Entry],
    1.31 +    val seen: Set[Document.Node.Name])
    1.32 +  {
    1.33 +    def :: (entry: Document.Node.Entry): Dependencies =
    1.34 +      new Dependencies(entry :: rev_entries, seen)
    1.35 +
    1.36 +    def + (name: Document.Node.Name): Dependencies =
    1.37 +      new Dependencies(rev_entries, seen + name)
    1.38 +
    1.39 +    def entries: List[Document.Node.Entry] = rev_entries.reverse
    1.40 +    def names: List[Document.Node.Name] = entries.map(_.name)
    1.41 +
    1.42 +    def errors: List[String] = entries.flatMap(_.header.errors)
    1.43 +
    1.44 +    lazy val loaded_theories: Graph[String, Outer_Syntax] =
    1.45 +      (session_base.loaded_theories /: entries)({ case (graph, entry) =>
    1.46 +        val name = entry.name.theory
    1.47 +        val imports = entry.header.imports.map(p => p._1.theory)
    1.48 +
    1.49 +        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
    1.50 +        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
    1.51 +
    1.52 +        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
    1.53 +        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
    1.54 +        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
    1.55 +
    1.56 +        graph2.map_node(name, _ => syntax)
    1.57 +      })
    1.58 +
    1.59 +    def loaded_files: List[(String, List[Path])] =
    1.60 +    {
    1.61 +      names.map(_.theory) zip
    1.62 +        Par_List.map((e: () => List[Path]) => e(),
    1.63 +          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
    1.64 +    }
    1.65 +
    1.66 +    def imported_files: List[Path] =
    1.67 +    {
    1.68 +      val base_theories =
    1.69 +        loaded_theories.all_preds(names.map(_.theory)).
    1.70 +          filter(session_base.loaded_theories.defined(_))
    1.71 +
    1.72 +      base_theories.map(theory => session_base.known.theories(theory).path) :::
    1.73 +      base_theories.flatMap(session_base.known.loaded_files(_))
    1.74 +    }
    1.75 +
    1.76 +    lazy val overall_syntax: Outer_Syntax =
    1.77 +      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
    1.78 +
    1.79 +    override def toString: String = entries.toString
    1.80 +  }
    1.81 +
    1.82 +  private def show_path(names: List[Document.Node.Name]): String =
    1.83 +    names.map(name => quote(name.theory)).mkString(" via ")
    1.84 +
    1.85 +  private def cycle_msg(names: List[Document.Node.Name]): String =
    1.86 +    "Cyclic dependency of " + show_path(names)
    1.87 +
    1.88 +  private def required_by(initiators: List[Document.Node.Name]): String =
    1.89 +    if (initiators.isEmpty) ""
    1.90 +    else "\n(required by " + show_path(initiators.reverse) + ")"
    1.91 +
    1.92 +  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
    1.93 +    thy: (Document.Node.Name, Position.T)): Dependencies =
    1.94 +  {
    1.95 +    val (name, pos) = thy
    1.96 +
    1.97 +    def message: String =
    1.98 +      "The error(s) above occurred for theory " + quote(name.theory) +
    1.99 +        required_by(initiators) + Position.here(pos)
   1.100 +
   1.101 +    val required1 = required + name
   1.102 +    if (required.seen(name)) required
   1.103 +    else if (session_base.loaded_theory(name)) required1
   1.104 +    else {
   1.105 +      try {
   1.106 +        if (initiators.contains(name)) error(cycle_msg(initiators))
   1.107 +        val header =
   1.108 +          try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
   1.109 +          catch { case ERROR(msg) => cat_error(msg, message) }
   1.110 +        Document.Node.Entry(name, header) ::
   1.111 +          require_thys(name :: initiators, required1, header.imports)
   1.112 +      }
   1.113 +      catch {
   1.114 +        case e: Throwable =>
   1.115 +          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
   1.116 +      }
   1.117 +    }
   1.118 +  }
   1.119 +
   1.120 +  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
   1.121 +      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   1.122 +    (required /: thys)(require_thy(initiators, _, _))
   1.123 +
   1.124 +  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   1.125 +    require_thys(Nil, Dependencies.empty, thys)
   1.126  }
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 15:36:50 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 15:55:50 2017 +0100
     2.3 @@ -222,7 +222,7 @@
     2.4              }
     2.5  
     2.6              val thy_deps =
     2.7 -              resources.thy_info.dependencies(
     2.8 +              resources.dependencies(
     2.9                  for { (_, thys) <- info.theories; (thy, pos) <- thys }
    2.10                  yield (resources.import_name(info.name, info.dir.implode, thy), pos))
    2.11  
     3.1 --- a/src/Pure/Thy/thy_info.scala	Tue Oct 31 15:36:50 2017 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,120 +0,0 @@
     3.4 -/*  Title:      Pure/Thy/thy_info.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Theory and file dependencies.
     3.8 -*/
     3.9 -
    3.10 -package isabelle
    3.11 -
    3.12 -
    3.13 -class Thy_Info(resources: Resources)
    3.14 -{
    3.15 -  /* messages */
    3.16 -
    3.17 -  private def show_path(names: List[Document.Node.Name]): String =
    3.18 -    names.map(name => quote(name.theory)).mkString(" via ")
    3.19 -
    3.20 -  private def cycle_msg(names: List[Document.Node.Name]): String =
    3.21 -    "Cyclic dependency of " + show_path(names)
    3.22 -
    3.23 -  private def required_by(initiators: List[Document.Node.Name]): String =
    3.24 -    if (initiators.isEmpty) ""
    3.25 -    else "\n(required by " + show_path(initiators.reverse) + ")"
    3.26 -
    3.27 -
    3.28 -  /* dependencies */
    3.29 -
    3.30 -  object Dependencies
    3.31 -  {
    3.32 -    val empty = new Dependencies(Nil, Set.empty)
    3.33 -  }
    3.34 -
    3.35 -  final class Dependencies private(
    3.36 -    rev_entries: List[Document.Node.Entry],
    3.37 -    val seen: Set[Document.Node.Name])
    3.38 -  {
    3.39 -    def :: (entry: Document.Node.Entry): Dependencies =
    3.40 -      new Dependencies(entry :: rev_entries, seen)
    3.41 -
    3.42 -    def + (name: Document.Node.Name): Dependencies =
    3.43 -      new Dependencies(rev_entries, seen + name)
    3.44 -
    3.45 -    def entries: List[Document.Node.Entry] = rev_entries.reverse
    3.46 -    def names: List[Document.Node.Name] = entries.map(_.name)
    3.47 -
    3.48 -    def errors: List[String] = entries.flatMap(_.header.errors)
    3.49 -
    3.50 -    lazy val loaded_theories: Graph[String, Outer_Syntax] =
    3.51 -      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
    3.52 -        val name = entry.name.theory
    3.53 -        val imports = entry.header.imports.map(p => p._1.theory)
    3.54 -
    3.55 -        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
    3.56 -        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
    3.57 -
    3.58 -        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
    3.59 -        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
    3.60 -        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
    3.61 -
    3.62 -        graph2.map_node(name, _ => syntax)
    3.63 -      })
    3.64 -
    3.65 -    def loaded_files: List[(String, List[Path])] =
    3.66 -    {
    3.67 -      names.map(_.theory) zip
    3.68 -        Par_List.map((e: () => List[Path]) => e(),
    3.69 -          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
    3.70 -    }
    3.71 -
    3.72 -    def imported_files: List[Path] =
    3.73 -    {
    3.74 -      val base = resources.session_base
    3.75 -      val base_theories =
    3.76 -        loaded_theories.all_preds(names.map(_.theory)).
    3.77 -          filter(base.loaded_theories.defined(_))
    3.78 -
    3.79 -      base_theories.map(theory => base.known.theories(theory).path) :::
    3.80 -      base_theories.flatMap(base.known.loaded_files(_))
    3.81 -    }
    3.82 -
    3.83 -    lazy val overall_syntax: Outer_Syntax =
    3.84 -      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
    3.85 -
    3.86 -    override def toString: String = entries.toString
    3.87 -  }
    3.88 -
    3.89 -  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
    3.90 -      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
    3.91 -    (required /: thys)(require_thy(initiators, _, _))
    3.92 -
    3.93 -  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
    3.94 -    thy: (Document.Node.Name, Position.T)): Dependencies =
    3.95 -  {
    3.96 -    val (name, pos) = thy
    3.97 -
    3.98 -    def message: String =
    3.99 -      "The error(s) above occurred for theory " + quote(name.theory) +
   3.100 -        required_by(initiators) + Position.here(pos)
   3.101 -
   3.102 -    val required1 = required + name
   3.103 -    if (required.seen(name)) required
   3.104 -    else if (resources.session_base.loaded_theory(name)) required1
   3.105 -    else {
   3.106 -      try {
   3.107 -        if (initiators.contains(name)) error(cycle_msg(initiators))
   3.108 -        val header =
   3.109 -          try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
   3.110 -          catch { case ERROR(msg) => cat_error(msg, message) }
   3.111 -        Document.Node.Entry(name, header) ::
   3.112 -          require_thys(name :: initiators, required1, header.imports)
   3.113 -      }
   3.114 -      catch {
   3.115 -        case e: Throwable =>
   3.116 -          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
   3.117 -      }
   3.118 -    }
   3.119 -  }
   3.120 -
   3.121 -  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   3.122 -    require_thys(Nil, Dependencies.empty, thys)
   3.123 -}
     4.1 --- a/src/Pure/build-jars	Tue Oct 31 15:36:50 2017 +0100
     4.2 +++ b/src/Pure/build-jars	Tue Oct 31 15:55:50 2017 +0100
     4.3 @@ -129,7 +129,6 @@
     4.4    Thy/present.scala
     4.5    Thy/sessions.scala
     4.6    Thy/thy_header.scala
     4.7 -  Thy/thy_info.scala
     4.8    Thy/thy_syntax.scala
     4.9    Tools/bibtex.scala
    4.10    Tools/build.scala
     5.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Oct 31 15:36:50 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Oct 31 15:55:50 2017 +0100
     5.3 @@ -216,7 +216,7 @@
     5.4            (for ((_, model) <- st.models.iterator if model.is_theory)
     5.5             yield (model.node_name, Position.none)).toList
     5.6  
     5.7 -        val thy_files = thy_info.dependencies(thys).names
     5.8 +        val thy_files = dependencies(thys).names
     5.9  
    5.10  
    5.11          /* auxiliary files */
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Oct 31 15:36:50 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Oct 31 15:55:50 2017 +0100
     6.3 @@ -253,7 +253,7 @@
     6.4                val pending_nodes = for ((node_name, None) <- purged) yield node_name
     6.5                (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
     6.6              }
     6.7 -            val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
     6.8 +            val retain = PIDE.resources.dependencies(imports).names.toSet
     6.9  
    6.10              for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
    6.11                yield edit
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Oct 31 15:36:50 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Oct 31 15:55:50 2017 +0100
     7.3 @@ -126,7 +126,7 @@
     7.4            val thys =
     7.5              (for ((node_name, model) <- models.iterator if model.is_theory)
     7.6                yield (node_name, Position.none)).toList
     7.7 -          val thy_files = resources.thy_info.dependencies(thys).names
     7.8 +          val thy_files = resources.dependencies(thys).names
     7.9  
    7.10            val aux_files =
    7.11              if (options.bool("jedit_auto_resolve")) {