Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);
authorwenzelm
Sat, 05 Jun 2021 20:20:25 +0200
changeset 73814 c8b4a4f69068
parent 73813 11f611494766
child 73815 43882e34c038
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);
src/Pure/Admin/components.scala file | annotate | diff | comparison | revisions
src/Pure/Thy/sessions.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/Admin/components.scala	Sat Jun 05 20:15:06 2021 +0200
+++ b/src/Pure/Admin/components.scala	Sat Jun 05 20:20:25 2021 +0200
@@ -152,7 +152,7 @@
   def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit =
   {
     val path = path0.expand.absolute
-    if (!check_dir(path)) error("Bad component directory: " + path)
+    if (!check_dir(path) && !Sessions.is_session_dir(path)) error("Bad component directory: " + path)
 
     val lines1 = read_components()
     val lines2 =
--- a/src/Pure/Thy/sessions.scala	Sat Jun 05 20:15:06 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Jun 05 20:20:25 2021 +0200
@@ -1014,7 +1014,7 @@
 
   /* load sessions from certain directories */
 
-  private def is_session_dir(dir: Path): Boolean =
+  def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   private def check_session_dir(dir: Path): Path =
isabelle