tuned signature;
authorwenzelm
Fri Sep 29 17:28:44 2017 +0200 (20 months ago)
changeset 667149fc4e144693c
parent 66713 afba7ffd6492
child 66715 6bced18e2b91
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
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/document.scala	Fri Sep 29 17:03:33 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Sep 29 17:28:44 2017 +0200
     1.3 @@ -126,6 +126,11 @@
     1.4        def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     1.5      }
     1.6  
     1.7 +    sealed case class Entry(name: Node.Name, header: Node.Header)
     1.8 +    {
     1.9 +      override def toString: String = name.toString
    1.10 +    }
    1.11 +
    1.12  
    1.13      /* node overlays */
    1.14  
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:03:33 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:28:44 2017 +0200
     2.3 @@ -205,7 +205,7 @@
     2.4  
     2.5              val syntax = thy_deps.syntax
     2.6  
     2.7 -            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
     2.8 +            val theory_files = thy_deps.entries.map(entry => Path.explode(entry.name.node))
     2.9              val loaded_files =
    2.10                if (inlined_files) {
    2.11                  if (Sessions.is_pure(info.name)) {
    2.12 @@ -251,18 +251,18 @@
    2.13                        val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
    2.14                        ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    2.15  
    2.16 -              (graph0 /: thy_deps.deps)(
    2.17 -                { case (g, dep) =>
    2.18 -                    val a = node(dep.name)
    2.19 +              (graph0 /: thy_deps.entries)(
    2.20 +                { case (g, entry) =>
    2.21 +                    val a = node(entry.name)
    2.22                      val bs =
    2.23 -                      dep.header.imports.map({ case (name, _) => node(name) }).
    2.24 +                      entry.header.imports.map({ case (name, _) => node(name) }).
    2.25                          filterNot(_ == a)
    2.26                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    2.27              }
    2.28  
    2.29              val known =
    2.30                Known.make(info.dir, List(imports_base),
    2.31 -                theories = thy_deps.deps.map(_.name),
    2.32 +                theories = thy_deps.entries.map(_.name),
    2.33                  loaded_files = loaded_files)
    2.34  
    2.35              val sources =
     3.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:03:33 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:28:44 2017 +0200
     3.3 @@ -7,18 +7,6 @@
     3.4  package isabelle
     3.5  
     3.6  
     3.7 -object Thy_Info
     3.8 -{
     3.9 -  /* dependencies */
    3.10 -
    3.11 -  sealed case class Dep(
    3.12 -    name: Document.Node.Name,
    3.13 -    header: Document.Node.Header)
    3.14 -  {
    3.15 -    override def toString: String = name.toString
    3.16 -  }
    3.17 -}
    3.18 -
    3.19  class Thy_Info(resources: Resources)
    3.20  {
    3.21    /* messages */
    3.22 @@ -42,36 +30,39 @@
    3.23    }
    3.24  
    3.25    final class Dependencies private(
    3.26 -    rev_deps: List[Thy_Info.Dep],
    3.27 +    rev_entries: List[Document.Node.Entry],
    3.28      val keywords: Thy_Header.Keywords,
    3.29      val abbrevs: Thy_Header.Abbrevs,
    3.30      val seen: Set[Document.Node.Name])
    3.31    {
    3.32 -    def :: (dep: Thy_Info.Dep): Dependencies =
    3.33 +    def :: (entry: Document.Node.Entry): Dependencies =
    3.34        new Dependencies(
    3.35 -        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs, seen)
    3.36 +        entry :: rev_entries,
    3.37 +        entry.header.keywords ::: keywords,
    3.38 +        entry.header.abbrevs ::: abbrevs,
    3.39 +        seen)
    3.40  
    3.41      def + (name: Document.Node.Name): Dependencies =
    3.42 -      new Dependencies(rev_deps, keywords, abbrevs, seen + name)
    3.43 +      new Dependencies(rev_entries, keywords, abbrevs, seen + name)
    3.44  
    3.45 -    def deps: List[Thy_Info.Dep] = rev_deps.reverse
    3.46 +    def entries: List[Document.Node.Entry] = rev_entries.reverse
    3.47  
    3.48 -    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
    3.49 +    def errors: List[String] = entries.flatMap(_.header.errors)
    3.50  
    3.51      lazy val syntax: Outer_Syntax =
    3.52        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    3.53  
    3.54      def loaded_theories: Set[String] =
    3.55 -      resources.session_base.loaded_theories ++ rev_deps.map(dep => dep.name.theory)
    3.56 +      resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory)
    3.57  
    3.58      def loaded_files: List[(String, List[Path])] =
    3.59      {
    3.60 -      val names = deps.map(_.name)
    3.61 +      val names = entries.map(_.name)
    3.62        names.map(_.theory) zip
    3.63          Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
    3.64      }
    3.65  
    3.66 -    override def toString: String = deps.toString
    3.67 +    override def toString: String = entries.toString
    3.68    }
    3.69  
    3.70    private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
    3.71 @@ -96,11 +87,12 @@
    3.72          val header =
    3.73            try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
    3.74            catch { case ERROR(msg) => cat_error(msg, message) }
    3.75 -        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
    3.76 +        Document.Node.Entry(name, header) ::
    3.77 +          require_thys(name :: initiators, required1, header.imports)
    3.78        }
    3.79        catch {
    3.80          case e: Throwable =>
    3.81 -          Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
    3.82 +          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
    3.83        }
    3.84      }
    3.85    }
     4.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 17:03:33 2017 +0200
     4.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 17:28:44 2017 +0200
     4.3 @@ -216,7 +216,7 @@
     4.4            (for ((_, model) <- st.models.iterator if model.is_theory)
     4.5             yield (model.node_name, Position.none)).toList
     4.6  
     4.7 -        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
     4.8 +        val thy_files = thy_info.dependencies(thys).entries.map(_.name)
     4.9  
    4.10  
    4.11          /* auxiliary files */
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 17:03:33 2017 +0200
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 17:28:44 2017 +0200
     5.3 @@ -253,7 +253,7 @@
     5.4                val pending_nodes = for ((node_name, None) <- purged) yield node_name
     5.5                (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
     5.6              }
     5.7 -            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
     5.8 +            val retain = PIDE.resources.thy_info.dependencies(imports).entries.map(_.name).toSet
     5.9  
    5.10              for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
    5.11                yield edit
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 17:03:33 2017 +0200
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 17:28:44 2017 +0200
     6.3 @@ -126,7 +126,7 @@
     6.4            val thys =
     6.5              (for ((node_name, model) <- models.iterator if model.is_theory)
     6.6                yield (node_name, Position.none)).toList
     6.7 -          val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
     6.8 +          val thy_files = resources.thy_info.dependencies(thys).entries.map(_.name)
     6.9  
    6.10            val aux_files =
    6.11              if (options.bool("jedit_auto_resolve")) {