clarified build of standard heaps;
authorwenzelm
Wed, 10 Apr 2019 15:10:43 +0200
changeset 70291 eadd87383e30
parent 70290 e6b7729453bf
child 70292 55220f2d09d2
clarified build of standard heaps;
NEWS
src/Pure/Admin/isabelle_devel.scala
src/Tools/jEdit/src/jedit_sessions.scala
--- a/NEWS	Wed Apr 10 14:43:29 2019 +0200
+++ b/NEWS	Wed Apr 10 15:10:43 2019 +0200
@@ -90,6 +90,16 @@
 storage directory for "isabelle build". Option "-n" is now clearly
 separated from option "-s".
 
+* The Isabelle/jEdit desktop application uses the same options as
+"isabelle jedit" for its internal "isabelle build" process: the implicit
+option "-o system_heaps" (or "-s") has been discontinued. This reduces
+the potential for surprise wrt. command-line tools.
+
+* The official download of the Isabelle/jEdit application already
+contains heap images for Isabelle/HOL within its main directory: thus
+the first encounter becomes faster and more robust (e.g. when run from a
+read-only directory).
+
 * Isabelle DejaVu fonts are available with hinting by default, which is
 relevant for low-resolution displays. This may be disabled via system
 option "isabelle_fonts_hinted = false" in
--- a/src/Pure/Admin/isabelle_devel.scala	Wed Apr 10 14:43:29 2019 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Wed Apr 10 15:10:43 2019 +0200
@@ -61,7 +61,9 @@
         Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
           website_dir =>
             Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev,
-              parallel_jobs = parallel_jobs, website = Some(website_dir)))
+              parallel_jobs = parallel_jobs,
+              build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
+              website = Some(website_dir)))
       })
   }
 
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Apr 10 14:43:29 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Apr 10 15:10:43 2019 +0200
@@ -29,7 +29,7 @@
     val options1 =
       Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
         case "default" => options
-        case mode => options.bool.update("system_heaps", mode == "" | mode == "system")
+        case mode => options.bool.update("system_heaps", mode == "system")
       }
 
     val options2 =