system option "system_heaps" supersedes various command-line options for "system build mode";
authorwenzelm
Fri Mar 01 21:29:59 2019 +0100 (3 months ago ago)
changeset 70035cc0b3e177b49
parent 70034 f7c9a1be333f
child 70036 60b924cda764
system option "system_heaps" supersedes various command-line options for "system build mode";
clarified "isabelle jedit" options -n, -s, -u;
NEWS
etc/options
src/Doc/JEdit/JEdit.thy
src/Doc/System/Environment.thy
src/Doc/System/Server.thy
src/Doc/System/Sessions.thy
src/Pure/Admin/build_doc.scala
src/Pure/Admin/ci_profile.scala
src/Pure/ML/ml_console.scala
src/Pure/Thy/export.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/server_commands.scala
src/Pure/Tools/update.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_build.scala
     1.1 --- a/NEWS	Fri Mar 01 20:16:26 2019 +0100
     1.2 +++ b/NEWS	Fri Mar 01 21:29:59 2019 +0100
     1.3 @@ -75,6 +75,11 @@
     1.4  the shell function "isabelle_file_format" in etc/settings (e.g. of an
     1.5  Isabelle component).
     1.6  
     1.7 +* Command-line options "-s" and "-u" of "isabelle jedit" override the
     1.8 +default for system option "system_heaps" that determines the heap
     1.9 +storage directory for "isabelle build". Option "-n" is now clearly
    1.10 +separated from option "-s".
    1.11 +
    1.12  
    1.13  *** Isar ***
    1.14  
    1.15 @@ -232,6 +237,11 @@
    1.16  
    1.17  *** System ***
    1.18  
    1.19 +* The system option "system_heaps" determines where to store the session
    1.20 +image of "isabelle build" (and other tools using that internally).
    1.21 +Former option "-s" is superseded by option "-o system_heaps".
    1.22 +INCOMPATIBILITY in command-line syntax.
    1.23 +
    1.24  * The command-line tool "isabelle update" uses Isabelle/PIDE in
    1.25  batch-mode to update theory sources based on semantic markup produced in
    1.26  Isabelle/ML. Actual updates depend on system options that may be enabled
     2.1 --- a/etc/options	Fri Mar 01 20:16:26 2019 +0100
     2.2 +++ b/etc/options	Fri Mar 01 21:29:59 2019 +0100
     2.3 @@ -116,6 +116,9 @@
     2.4  option profiling : string = ""
     2.5    -- "ML profiling (possible values: time, allocations)"
     2.6  
     2.7 +option system_heaps : bool = false
     2.8 +  -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
     2.9 +
    2.10  
    2.11  section "ML System"
    2.12  
     3.1 --- a/src/Doc/JEdit/JEdit.thy	Fri Mar 01 20:16:26 2019 +0100
     3.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Mar 01 21:29:59 2019 +0100
     3.3 @@ -243,7 +243,8 @@
     3.4      -m MODE      add print mode for output
     3.5      -n           no build of session image on startup
     3.6      -p CMD       ML process command prefix (process policy)
     3.7 -    -s           system build mode for session image
     3.8 +    -s           system build mode for session image (system_heaps=true)
     3.9 +    -u           user build mode for session image (system_heaps=false)
    3.10  
    3.11    Start jEdit with Isabelle plugin setup and open FILES
    3.12    (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
    3.13 @@ -252,9 +253,10 @@
    3.14    for proof processing. Additional session root directories may be included
    3.15    via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
    3.16    "isabelle-system"}). By default, the specified image is checked and built on
    3.17 -  demand. The \<^verbatim>\<open>-s\<close> option determines where to store the result session image
    3.18 -  of @{tool build}. The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for
    3.19 -  the selected session image.
    3.20 +  demand, but option \<^verbatim>\<open>-n\<close> bypasses the implicit build process for the
    3.21 +  selected session image. Options \<^verbatim>\<open>-s\<close> and \<^verbatim>\<open>-u\<close> override the default system
    3.22 +  option @{system_option system_heaps}: this determines where to store the
    3.23 +  session image of @{tool build}.
    3.24  
    3.25    The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from
    3.26    other sessions that are not already present in its parent; it also opens the
     4.1 --- a/src/Doc/System/Environment.thy	Fri Mar 01 20:16:26 2019 +0100
     4.2 +++ b/src/Doc/System/Environment.thy	Fri Mar 01 21:29:59 2019 +0100
     4.3 @@ -181,9 +181,10 @@
     4.4    used instead; its default is \<^path>\<open>$ISABELLE_HOME/browser_info\<close>.
     4.5  
     4.6    \<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images,
     4.7 -  log files, and build databases are stored; its default is \<^path>\<open>$ISABELLE_HOME_USER/heaps\<close>. For ``system build mode'' (see
     4.8 -  \secref{sec:tool-build}), @{setting_def ISABELLE_HEAPS_SYSTEM} is used
     4.9 -  instead; its default is \<^path>\<open>$ISABELLE_HOME/heaps\<close>.
    4.10 +  log files, and build databases are stored; its default is
    4.11 +  \<^path>\<open>$ISABELLE_HOME_USER/heaps\<close>. If @{system_option system_heaps} is
    4.12 +  \<^verbatim>\<open>true\<close>, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default
    4.13 +  is \<^path>\<open>$ISABELLE_HOME/heaps\<close>. See also \secref{sec:tool-build}.
    4.14  
    4.15    \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
    4.16    is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
    4.17 @@ -410,7 +411,6 @@
    4.18      -n           no build of session image on startup
    4.19      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    4.20      -r           bootstrap from raw Poly/ML
    4.21 -    -s           system build mode for session image
    4.22  
    4.23    Build a logic session image and run the raw Isabelle ML process
    4.24    in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
    4.25 @@ -429,9 +429,6 @@
    4.26    Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
    4.27    (\secref{sec:tool-process}).
    4.28  
    4.29 -  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
    4.30 -  (\secref{sec:tool-build}).
    4.31 -
    4.32    \<^medskip>
    4.33    The Isabelle/ML process is run through the line editor that is specified via
    4.34    the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
     5.1 --- a/src/Doc/System/Server.thy	Fri Mar 01 20:16:26 2019 +0100
     5.2 +++ b/src/Doc/System/Server.thy	Fri Mar 01 21:29:59 2019 +0100
     5.3 @@ -655,7 +655,6 @@
     5.4    \quad~~\<open>options?: [string],\<close> \\
     5.5    \quad~~\<open>dirs?: [string],\<close> \\
     5.6    \quad~~\<open>include_sessions: [string],\<close> \\
     5.7 -  \quad~~\<open>system_mode?: bool,\<close> \\
     5.8    \quad~~\<open>verbose?: bool}\<close> \\[2ex]
     5.9    \end{tabular}
    5.10  
    5.11 @@ -724,10 +723,6 @@
    5.12    in a robust manner, instead of relying on directory locations.
    5.13  
    5.14    \<^medskip>
    5.15 -  If \<open>system_mode\<close> is \<^verbatim>\<open>true\<close>, session images are stored in \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> instead of \<^path>\<open>$ISABELLE_HEAPS\<close>. See also
    5.16 -  option \<^verbatim>\<open>-s\<close> in @{tool build} (\secref{sec:tool-build}).
    5.17 -
    5.18 -  \<^medskip>
    5.19    The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
    5.20    similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
    5.21  \<close>
     6.1 --- a/src/Doc/System/Sessions.thy	Fri Mar 01 20:16:26 2019 +0100
     6.2 +++ b/src/Doc/System/Sessions.thy	Fri Mar 01 21:29:59 2019 +0100
     6.3 @@ -238,6 +238,13 @@
     6.4      \<^ML>\<open>profile_time\<close> and \<^verbatim>\<open>allocations\<close> for \<^ML>\<open>profile_allocations\<close>.
     6.5      Results appear near the bottom of the session log file.
     6.6  
     6.7 +    \<^item> @{system_option_def "system_heaps"} determines the directories for
     6.8 +    session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and
     6.9 +    \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> the system directory (usually within the
    6.10 +    Isabelle application). For \<^verbatim>\<open>system_heaps=false\<close>, heaps are stored in the
    6.11 +    user directory and may be loaded from both directories. For
    6.12 +    \<^verbatim>\<open>system_heaps=true\<close>, store and load happens only in the system directory.
    6.13 +
    6.14    The @{tool_def options} tool prints Isabelle system options. Its
    6.15    command-line usage is:
    6.16    @{verbatim [display]
    6.17 @@ -297,7 +304,6 @@
    6.18      -l           list session source files
    6.19      -n           no build -- test dependencies only
    6.20      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    6.21 -    -s           system build mode: produce output in ISABELLE_HOME
    6.22      -v           verbose
    6.23      -x NAME      exclude session NAME and all descendants
    6.24  
    6.25 @@ -403,10 +409,6 @@
    6.26    performance tuning on Linux servers with separate CPU/memory modules.
    6.27  
    6.28    \<^medskip>
    6.29 -  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that session images are
    6.30 -  stored in \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> instead of \<^path>\<open>$ISABELLE_HEAPS\<close>.
    6.31 -
    6.32 -  \<^medskip>
    6.33    Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
    6.34    the source files that contribute to a session.
    6.35  
    6.36 @@ -572,7 +574,6 @@
    6.37      -n           no build of session
    6.38      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    6.39      -p NUM       prune path of exported files by NUM elements
    6.40 -    -s           system build mode for session image
    6.41      -x PATTERN   extract files matching pattern (e.g.\ "*:**" for all)
    6.42  
    6.43    List or export theory exports for SESSION: named blobs produced by
    6.44 @@ -584,9 +585,9 @@
    6.45  
    6.46    \<^medskip>
    6.47    The specified session is updated via @{tool build}
    6.48 -  (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close>. The
    6.49 -  option \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a
    6.50 -  potentially outdated session database is used!
    6.51 +  (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>. The option
    6.52 +  \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a potentially
    6.53 +  outdated session database is used!
    6.54  
    6.55    \<^medskip>
    6.56    Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names
    6.57 @@ -630,7 +631,6 @@
    6.58      -g NAME      select session group NAME
    6.59      -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
    6.60      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    6.61 -    -s           system build mode for logic image
    6.62      -v           verbose
    6.63      -x NAME      exclude session NAME and all descendants
    6.64  
    6.65 @@ -645,8 +645,7 @@
    6.66  
    6.67    \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
    6.68    its theories are not processed again, and their PIDE session database is
    6.69 -  excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
    6.70 -  the logic image (\secref{sec:tool-build}).
    6.71 +  excluded from the dump.
    6.72  
    6.73    \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
    6.74    (\secref{sec:tool-build}).
    6.75 @@ -708,7 +707,6 @@
    6.76      -g NAME      select session group NAME
    6.77      -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
    6.78      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    6.79 -    -s           system build mode for logic image
    6.80      -u OPT       overide update option: shortcut for "-o update_OPT"
    6.81      -v           verbose
    6.82      -x NAME      exclude session NAME and all descendants
    6.83 @@ -719,8 +717,7 @@
    6.84    remaining command-line arguments specify sessions as in @{tool build}
    6.85    (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
    6.86  
    6.87 -  \<^medskip> Options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-s\<close> specify the underlying logic image is in @{tool
    6.88 -  dump} (\secref{sec:tool-dump}).
    6.89 +  \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies the underlying logic image.
    6.90  
    6.91    \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
    6.92  
     7.1 --- a/src/Pure/Admin/build_doc.scala	Fri Mar 01 20:16:26 2019 +0100
     7.2 +++ b/src/Pure/Admin/build_doc.scala	Fri Mar 01 21:29:59 2019 +0100
     7.3 @@ -19,7 +19,6 @@
     7.4      progress: Progress = No_Progress,
     7.5      all_docs: Boolean = false,
     7.6      max_jobs: Int = 1,
     7.7 -    system_mode: Boolean = false,
     7.8      docs: List[String] = Nil): Int =
     7.9    {
    7.10      val sessions_structure = Sessions.load_structure(options)
    7.11 @@ -44,7 +43,7 @@
    7.12  
    7.13      val res1 =
    7.14        Build.build(options, progress, requirements = true, build_heap = true,
    7.15 -        max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
    7.16 +        max_jobs = max_jobs, sessions = sessions)
    7.17      if (res1.ok) {
    7.18        Isabelle_System.with_tmp_dir("document_output")(output =>
    7.19          {
    7.20 @@ -53,8 +52,7 @@
    7.21                options.bool.update("browser_info", false).
    7.22                  string.update("document", "pdf").
    7.23                  string.update("document_output", output.implode),
    7.24 -              progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
    7.25 -              sessions = sessions)
    7.26 +              progress, clean_build = true, max_jobs = max_jobs, sessions = sessions)
    7.27            if (res2.ok) {
    7.28              val doc_dir = Path.explode("~~/doc")
    7.29              for (doc <- selected_docs) {
    7.30 @@ -76,7 +74,7 @@
    7.31      {
    7.32        var all_docs = false
    7.33        var max_jobs = 1
    7.34 -      var system_mode = false
    7.35 +      var options = Options.init()
    7.36  
    7.37        val getopts =
    7.38          Getopts("""
    7.39 @@ -85,24 +83,23 @@
    7.40    Options are:
    7.41      -a           select all documentation sessions
    7.42      -j INT       maximum number of parallel jobs (default 1)
    7.43 -    -s           system build mode
    7.44 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    7.45  
    7.46    Build Isabelle documentation from documentation sessions with
    7.47    suitable document_variants entry.
    7.48  """,
    7.49            "a" -> (_ => all_docs = true),
    7.50            "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    7.51 -          "s" -> (_ => system_mode = true))
    7.52 +          "o:" -> (arg => options = options + arg))
    7.53  
    7.54        val docs = getopts(args)
    7.55  
    7.56        if (!all_docs && docs.isEmpty) getopts.usage()
    7.57  
    7.58 -      val options = Options.init()
    7.59        val progress = new Console_Progress()
    7.60        val rc =
    7.61          progress.interrupt_handler {
    7.62 -          build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
    7.63 +          build_doc(options, progress, all_docs, max_jobs, docs)
    7.64          }
    7.65        sys.exit(rc)
    7.66      })
     8.1 --- a/src/Pure/Admin/ci_profile.scala	Fri Mar 01 20:16:26 2019 +0100
     8.2 +++ b/src/Pure/Admin/ci_profile.scala	Fri Mar 01 21:29:59 2019 +0100
     8.3 @@ -20,7 +20,7 @@
     8.4      val start_time = Time.now()
     8.5      val results = progress.interrupt_handler {
     8.6        Build.build(
     8.7 -        options = options,
     8.8 +        options = options + "system_heaps",
     8.9          progress = progress,
    8.10          clean_build = clean,
    8.11          verbose = true,
    8.12 @@ -28,7 +28,6 @@
    8.13          max_jobs = jobs,
    8.14          dirs = include,
    8.15          select_dirs = select,
    8.16 -        system_mode = true,
    8.17          selection = selection)
    8.18      }
    8.19      val end_time = Time.now()
     9.1 --- a/src/Pure/ML/ml_console.scala	Fri Mar 01 20:16:26 2019 +0100
     9.2 +++ b/src/Pure/ML/ml_console.scala	Fri Mar 01 21:29:59 2019 +0100
     9.3 @@ -21,7 +21,6 @@
     9.4        var no_build = false
     9.5        var options = Options.init()
     9.6        var raw_ml_system = false
     9.7 -      var system_mode = false
     9.8  
     9.9        val getopts = Getopts("""
    9.10  Usage: isabelle console [OPTIONS]
    9.11 @@ -34,7 +33,6 @@
    9.12      -n           no build of session image on startup
    9.13      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    9.14      -r           bootstrap from raw Poly/ML
    9.15 -    -s           system build mode for session image
    9.16  
    9.17    Build a logic session image and run the raw Isabelle ML process
    9.18    in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
    9.19 @@ -46,8 +44,7 @@
    9.20          "m:" -> (arg => modes = arg :: modes),
    9.21          "n" -> (arg => no_build = true),
    9.22          "o:" -> (arg => options = options + arg),
    9.23 -        "r" -> (_ => raw_ml_system = true),
    9.24 -        "s" -> (_ => system_mode = true))
    9.25 +        "r" -> (_ => raw_ml_system = true))
    9.26  
    9.27        val more_args = getopts(args)
    9.28        if (!more_args.isEmpty) getopts.usage()
    9.29 @@ -58,8 +55,7 @@
    9.30          val progress = new Console_Progress()
    9.31          val rc =
    9.32            progress.interrupt_handler {
    9.33 -            Build.build_logic(options, logic, build_heap = true, progress = progress,
    9.34 -              dirs = dirs, system_mode = system_mode)
    9.35 +            Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
    9.36            }
    9.37          if (rc != 0) sys.exit(rc)
    9.38        }
    9.39 @@ -69,7 +65,7 @@
    9.40          ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
    9.41            modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
    9.42            raw_ml_system = raw_ml_system,
    9.43 -          store = Some(Sessions.store(options, system_mode)),
    9.44 +          store = Some(Sessions.store(options)),
    9.45            session_base =
    9.46              if (raw_ml_system) None
    9.47              else Some(Sessions.base_info(
    10.1 --- a/src/Pure/Thy/export.scala	Fri Mar 01 20:16:26 2019 +0100
    10.2 +++ b/src/Pure/Thy/export.scala	Fri Mar 01 21:29:59 2019 +0100
    10.3 @@ -322,7 +322,6 @@
    10.4      var no_build = false
    10.5      var options = Options.init()
    10.6      var export_prune = 0
    10.7 -    var system_mode = false
    10.8      var export_patterns: List[String] = Nil
    10.9  
   10.10      val getopts = Getopts("""
   10.11 @@ -335,7 +334,6 @@
   10.12      -n           no build of session
   10.13      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   10.14      -p NUM       prune path of exported files by NUM elements
   10.15 -    -s           system build mode for session image
   10.16      -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
   10.17  
   10.18    List or export theory exports for SESSION: named blobs produced by
   10.19 @@ -351,7 +349,6 @@
   10.20        "n" -> (_ => no_build = true),
   10.21        "o:" -> (arg => options = options + arg),
   10.22        "p:" -> (arg => export_prune = Value.Int.parse(arg)),
   10.23 -      "s" -> (_ => system_mode = true),
   10.24        "x:" -> (arg => export_patterns ::= arg))
   10.25  
   10.26      val more_args = getopts(args)
   10.27 @@ -369,8 +366,7 @@
   10.28      if (!no_build) {
   10.29        val rc =
   10.30          progress.interrupt_handler {
   10.31 -          Build.build_logic(options, session_name, progress = progress,
   10.32 -            dirs = dirs, system_mode = system_mode)
   10.33 +          Build.build_logic(options, session_name, progress = progress, dirs = dirs)
   10.34          }
   10.35        if (rc != 0) sys.exit(rc)
   10.36      }
   10.37 @@ -378,7 +374,7 @@
   10.38  
   10.39      /* export files */
   10.40  
   10.41 -    val store = Sessions.store(options, system_mode)
   10.42 +    val store = Sessions.store(options)
   10.43      export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
   10.44        export_list = export_list, export_patterns = export_patterns)
   10.45    })
    11.1 --- a/src/Pure/Thy/sessions.scala	Fri Mar 01 20:16:26 2019 +0100
    11.2 +++ b/src/Pure/Thy/sessions.scala	Fri Mar 01 21:29:59 2019 +0100
    11.3 @@ -1079,10 +1079,9 @@
    11.4      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    11.5    }
    11.6  
    11.7 -  def store(options: Options, system_mode: Boolean = false): Store =
    11.8 -    new Store(options, system_mode)
    11.9 +  def store(options: Options): Store = new Store(options)
   11.10  
   11.11 -  class Store private[Sessions](val options: Options, val system_mode: Boolean)
   11.12 +  class Store private[Sessions](val options: Options)
   11.13    {
   11.14      override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
   11.15  
   11.16 @@ -1092,15 +1091,17 @@
   11.17      val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
   11.18      val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
   11.19  
   11.20 +    def system_heaps: Boolean = options.bool("system_heaps")
   11.21 +
   11.22      val output_dir: Path =
   11.23 -      if (system_mode) system_output_dir else user_output_dir
   11.24 +      if (system_heaps) system_output_dir else user_output_dir
   11.25  
   11.26      val input_dirs: List[Path] =
   11.27 -      if (system_mode) List(system_output_dir)
   11.28 +      if (system_heaps) List(system_output_dir)
   11.29        else List(user_output_dir, system_output_dir)
   11.30  
   11.31      val browser_info: Path =
   11.32 -      if (system_mode) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
   11.33 +      if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
   11.34        else Path.explode("$ISABELLE_BROWSER_INFO")
   11.35  
   11.36  
   11.37 @@ -1184,7 +1185,8 @@
   11.38  
   11.39        val del =
   11.40          for {
   11.41 -          dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
   11.42 +          dir <-
   11.43 +            (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
   11.44            file <- List(heap(name), database(name), log(name), log_gz(name))
   11.45            path = dir + file if path.is_file
   11.46          } yield path.file.delete
    12.1 --- a/src/Pure/Tools/build.scala	Fri Mar 01 20:16:26 2019 +0100
    12.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 01 21:29:59 2019 +0100
    12.3 @@ -395,7 +395,6 @@
    12.4      fresh_build: Boolean = false,
    12.5      no_build: Boolean = false,
    12.6      soft_build: Boolean = false,
    12.7 -    system_mode: Boolean = false,
    12.8      verbose: Boolean = false,
    12.9      export_files: Boolean = false,
   12.10      pide: Boolean = false,
   12.11 @@ -410,7 +409,7 @@
   12.12    {
   12.13      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   12.14  
   12.15 -    val store = Sessions.store(build_options, system_mode)
   12.16 +    val store = Sessions.store(build_options)
   12.17  
   12.18      Isabelle_Fonts.init()
   12.19  
   12.20 @@ -737,7 +736,6 @@
   12.21      var list_files = false
   12.22      var no_build = false
   12.23      var options = Options.init(opts = build_options)
   12.24 -    var system_mode = false
   12.25      var verbose = false
   12.26      var exclude_sessions: List[String] = Nil
   12.27  
   12.28 @@ -764,7 +762,6 @@
   12.29      -l           list session source files
   12.30      -n           no build -- test dependencies only
   12.31      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   12.32 -    -s           system build mode: produce output in ISABELLE_HOME
   12.33      -v           verbose
   12.34      -x NAME      exclude session NAME and all descendants
   12.35  
   12.36 @@ -790,7 +787,6 @@
   12.37        "l" -> (_ => list_files = true),
   12.38        "n" -> (_ => no_build = true),
   12.39        "o:" -> (arg => options = options + arg),
   12.40 -      "s" -> (_ => system_mode = true),
   12.41        "v" -> (_ => verbose = true),
   12.42        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   12.43  
   12.44 @@ -823,7 +819,6 @@
   12.45            fresh_build = fresh_build,
   12.46            no_build = no_build,
   12.47            soft_build = soft_build,
   12.48 -          system_mode = system_mode,
   12.49            verbose = verbose,
   12.50            export_files = export_files,
   12.51            pide = pide,
   12.52 @@ -857,16 +852,15 @@
   12.53      progress: Progress = No_Progress,
   12.54      build_heap: Boolean = false,
   12.55      dirs: List[Path] = Nil,
   12.56 -    system_mode: Boolean = false,
   12.57      strict: Boolean = false): Int =
   12.58    {
   12.59      val rc =
   12.60        if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
   12.61 -          system_mode = system_mode, sessions = List(logic)).ok) 0
   12.62 +          sessions = List(logic)).ok) 0
   12.63        else {
   12.64          progress.echo("Build started for Isabelle/" + logic + " ...")
   12.65          Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
   12.66 -          system_mode = system_mode, sessions = List(logic)).rc
   12.67 +          sessions = List(logic)).rc
   12.68        }
   12.69  
   12.70      if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
    13.1 --- a/src/Pure/Tools/dump.scala	Fri Mar 01 20:16:26 2019 +0100
    13.2 +++ b/src/Pure/Tools/dump.scala	Fri Mar 01 21:29:59 2019 +0100
    13.3 @@ -209,11 +209,10 @@
    13.4      dirs: List[Path] = Nil,
    13.5      select_dirs: List[Path] = Nil,
    13.6      output_dir: Path = default_output_dir,
    13.7 -    system_mode: Boolean = false,
    13.8      selection: Sessions.Selection = Sessions.Selection.empty)
    13.9    {
   13.10      Build.build_logic(options, logic, build_heap = true, progress = progress,
   13.11 -      dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
   13.12 +      dirs = dirs ::: select_dirs, strict = true)
   13.13  
   13.14      val dump_options = make_options(options, aspects)
   13.15  
   13.16 @@ -254,7 +253,6 @@
   13.17        var session_groups: List[String] = Nil
   13.18        var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   13.19        var options = Options.init()
   13.20 -      var system_mode = false
   13.21        var verbose = false
   13.22        var exclude_sessions: List[String] = Nil
   13.23  
   13.24 @@ -273,7 +271,6 @@
   13.25      -g NAME      select session group NAME
   13.26      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   13.27      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   13.28 -    -s           system build mode for logic image
   13.29      -v           verbose
   13.30      -x NAME      exclude session NAME and all descendants
   13.31  
   13.32 @@ -291,7 +288,6 @@
   13.33        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   13.34        "l:" -> (arg => logic = arg),
   13.35        "o:" -> (arg => options = options + arg),
   13.36 -      "s" -> (_ => system_mode = true),
   13.37        "v" -> (_ => verbose = true),
   13.38        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   13.39  
    14.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 01 20:16:26 2019 +0100
    14.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 01 21:29:59 2019 +0100
    14.3 @@ -29,7 +29,6 @@
    14.4        options: List[String] = Nil,
    14.5        dirs: List[String] = Nil,
    14.6        include_sessions: List[String] = Nil,
    14.7 -      system_mode: Boolean = false,
    14.8        verbose: Boolean = false)
    14.9  
   14.10      def unapply(json: JSON.T): Option[Args] =
   14.11 @@ -39,12 +38,11 @@
   14.12          options <- JSON.strings_default(json, "options")
   14.13          dirs <- JSON.strings_default(json, "dirs")
   14.14          include_sessions <- JSON.strings_default(json, "include_sessions")
   14.15 -        system_mode <- JSON.bool_default(json, "system_mode")
   14.16          verbose <- JSON.bool_default(json, "verbose")
   14.17        }
   14.18        yield {
   14.19          Args(session, preferences = preferences, options = options, dirs = dirs,
   14.20 -          include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
   14.21 +          include_sessions = include_sessions, verbose = verbose)
   14.22        }
   14.23  
   14.24      def command(args: Args, progress: Progress = No_Progress)
   14.25 @@ -62,7 +60,6 @@
   14.26          Build.build(options,
   14.27            progress = progress,
   14.28            build_heap = true,
   14.29 -          system_mode = args.system_mode,
   14.30            dirs = dirs,
   14.31            infos = base_info.infos,
   14.32            verbose = args.verbose,
    15.1 --- a/src/Pure/Tools/update.scala	Fri Mar 01 20:16:26 2019 +0100
    15.2 +++ b/src/Pure/Tools/update.scala	Fri Mar 01 21:29:59 2019 +0100
    15.3 @@ -14,11 +14,10 @@
    15.4      log: Logger = No_Logger,
    15.5      dirs: List[Path] = Nil,
    15.6      select_dirs: List[Path] = Nil,
    15.7 -    system_mode: Boolean = false,
    15.8      selection: Sessions.Selection = Sessions.Selection.empty)
    15.9    {
   15.10      Build.build_logic(options, logic, build_heap = true, progress = progress,
   15.11 -      dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
   15.12 +      dirs = dirs ::: select_dirs, strict = true)
   15.13  
   15.14      val dump_options = Dump.make_options(options)
   15.15  
   15.16 @@ -82,7 +81,6 @@
   15.17        var session_groups: List[String] = Nil
   15.18        var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   15.19        var options = Options.init()
   15.20 -      var system_mode = false
   15.21        var verbose = false
   15.22        var exclude_sessions: List[String] = Nil
   15.23  
   15.24 @@ -99,7 +97,6 @@
   15.25      -g NAME      select session group NAME
   15.26      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   15.27      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   15.28 -    -s           system build mode for logic image
   15.29      -u OPT       overide update option: shortcut for "-o update_OPT"
   15.30      -v           verbose
   15.31      -x NAME      exclude session NAME and all descendants
   15.32 @@ -115,7 +112,6 @@
   15.33        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   15.34        "l:" -> (arg => logic = arg),
   15.35        "o:" -> (arg => options = options + arg),
   15.36 -      "s" -> (_ => system_mode = true),
   15.37        "u:" -> (arg => options = options + ("update_" + arg)),
   15.38        "v" -> (_ => verbose = true),
   15.39        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    16.1 --- a/src/Tools/VSCode/src/server.scala	Fri Mar 01 20:16:26 2019 +0100
    16.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Mar 01 21:29:59 2019 +0100
    16.3 @@ -40,7 +40,6 @@
    16.4        var logic = default_logic
    16.5        var modes: List[String] = Nil
    16.6        var options = Options.init()
    16.7 -      var system_mode = false
    16.8        var verbose = false
    16.9  
   16.10        val getopts = Getopts("""
   16.11 @@ -56,7 +55,6 @@
   16.12      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   16.13      -m MODE      add print mode for output
   16.14      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   16.15 -    -s           system build mode for session image
   16.16      -v           verbose logging
   16.17  
   16.18    Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
   16.19 @@ -70,7 +68,6 @@
   16.20          "l:" -> (arg => logic = arg),
   16.21          "m:" -> (arg => modes = arg :: modes),
   16.22          "o:" -> (arg => options = options + arg),
   16.23 -        "s" -> (_ => system_mode = true),
   16.24          "v" -> (_ => verbose = true))
   16.25  
   16.26        val more_args = getopts(args)
   16.27 @@ -82,7 +79,7 @@
   16.28          new Server(channel, options, session_name = logic, session_dirs = dirs,
   16.29            include_sessions = include_sessions, session_ancestor = logic_ancestor,
   16.30            session_requirements = logic_requirements, session_focus = logic_focus,
   16.31 -          all_known = !logic_focus, modes = modes, system_mode = system_mode, log = log)
   16.32 +          all_known = !logic_focus, modes = modes, log = log)
   16.33  
   16.34        // prevent spurious garbage on the main protocol channel
   16.35        val orig_out = System.out
   16.36 @@ -112,7 +109,6 @@
   16.37    session_focus: Boolean = false,
   16.38    all_known: Boolean = false,
   16.39    modes: List[String] = Nil,
   16.40 -  system_mode: Boolean = false,
   16.41    log: Logger = No_Logger)
   16.42  {
   16.43    server =>
   16.44 @@ -279,8 +275,8 @@
   16.45          val session_base = base_info.check_base
   16.46  
   16.47          def build(no_build: Boolean = false): Build.Results =
   16.48 -          Build.build(options, build_heap = true, no_build = no_build, system_mode = system_mode,
   16.49 -            dirs = session_dirs, infos = base_info.infos, sessions = List(base_info.session))
   16.50 +          Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs,
   16.51 +            infos = base_info.infos, sessions = List(base_info.session))
   16.52  
   16.53          if (!build(no_build = true).ok) {
   16.54            val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
    17.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Mar 01 20:16:26 2019 +0100
    17.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Mar 01 21:29:59 2019 +0100
    17.3 @@ -116,7 +116,8 @@
    17.4    echo "    -m MODE      add print mode for output"
    17.5    echo "    -n           no build of session image on startup"
    17.6    echo "    -p CMD       ML process command prefix (process policy)"
    17.7 -  echo "    -s           system build mode for session image"
    17.8 +  echo "    -s           system build mode for session image (system_heaps=true)"
    17.9 +  echo "    -u           user build mode for session image (system_heaps=false)"
   17.10    echo
   17.11    echo "  Start jEdit with Isabelle plugin setup and open FILES"
   17.12    echo "  (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
   17.13 @@ -150,12 +151,13 @@
   17.14  JEDIT_SESSION_DIRS=""
   17.15  JEDIT_LOGIC=""
   17.16  JEDIT_PRINT_MODE=""
   17.17 -JEDIT_BUILD_MODE="normal"
   17.18 +JEDIT_NO_BUILD=""
   17.19 +JEDIT_BUILD_MODE="default"
   17.20  
   17.21  function getoptions()
   17.22  {
   17.23    OPTIND=1
   17.24 -  while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
   17.25 +  while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:su" OPT
   17.26    do
   17.27      case "$OPT" in
   17.28        A)
   17.29 @@ -210,7 +212,7 @@
   17.30          fi
   17.31          ;;
   17.32        n)
   17.33 -        JEDIT_BUILD_MODE="none"
   17.34 +        JEDIT_NO_BUILD="true"
   17.35          ;;
   17.36        p)
   17.37          ML_PROCESS_POLICY="$OPTARG"
   17.38 @@ -218,6 +220,9 @@
   17.39        s)
   17.40          JEDIT_BUILD_MODE="system"
   17.41          ;;
   17.42 +      u)
   17.43 +        JEDIT_BUILD_MODE="user"
   17.44 +        ;;
   17.45        \?)
   17.46          usage
   17.47          ;;
   17.48 @@ -425,7 +430,7 @@
   17.49  if [ "$BUILD_ONLY" = false ]
   17.50  then
   17.51    export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
   17.52 -    JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   17.53 +    JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
   17.54    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   17.55    classpath "$JEDIT_HOME/dist/jedit.jar"
   17.56    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
    18.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 01 20:16:26 2019 +0100
    18.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 01 21:29:59 2019 +0100
    18.3 @@ -18,19 +18,28 @@
    18.4  {
    18.5    /* session options */
    18.6  
    18.7 -  def session_options(options: Options): Options =
    18.8 -    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
    18.9 -      case "" => options
   18.10 -      case s => options.string.update("ML_process_policy", s)
   18.11 -    }
   18.12 -
   18.13    def session_dirs(): List[Path] =
   18.14      Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
   18.15  
   18.16 -  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
   18.17 +  def session_no_build(): Boolean =
   18.18 +    Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
   18.19  
   18.20 -  def session_system_mode(): Boolean =
   18.21 -    session_build_mode() match { case "" | "system" => true case _ => false }
   18.22 +  def session_options(options: Options): Options =
   18.23 +  {
   18.24 +    val options1 =
   18.25 +      Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
   18.26 +        case "default" => options
   18.27 +        case mode => options.bool.update("system_heaps", mode == "" | mode == "system")
   18.28 +      }
   18.29 +
   18.30 +    val options2 =
   18.31 +      Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
   18.32 +        case "" => options1
   18.33 +        case s => options1.string.update("ML_process_policy", s)
   18.34 +      }
   18.35 +
   18.36 +    options2
   18.37 +  }
   18.38  
   18.39    def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
   18.40      Sessions.load_structure(session_options(options), dirs = dirs)
   18.41 @@ -123,17 +132,18 @@
   18.42      options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
   18.43    {
   18.44      Build.build(session_options(options), progress = progress, build_heap = true,
   18.45 -      no_build = no_build, system_mode = session_system_mode(),
   18.46 -      dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
   18.47 +      no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
   18.48        sessions = List(PIDE.resources.session_name)).rc
   18.49    }
   18.50  
   18.51 -  def session_start(options: Options)
   18.52 +  def session_start(options0: Options)
   18.53    {
   18.54 -    Isabelle_Process.start(PIDE.session, session_options(options),
   18.55 +    val options = session_options(options0)
   18.56 +
   18.57 +    Isabelle_Process.start(PIDE.session, options,
   18.58        sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
   18.59        logic = PIDE.resources.session_name,
   18.60 -      store = Some(Sessions.store(options, session_system_mode())),
   18.61 +      store = Some(Sessions.store(options)),
   18.62        modes =
   18.63          (space_explode(',', options.string("jedit_print_mode")) :::
   18.64           space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
    19.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Mar 01 20:16:26 2019 +0100
    19.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 01 21:29:59 2019 +0100
    19.3 @@ -65,7 +65,8 @@
    19.4    /* options */
    19.5  
    19.6    private var _options: JEdit_Options = null
    19.7 -  private def init_options(): Unit = _options = new JEdit_Options(Options.init())
    19.8 +  private def init_options(): Unit =
    19.9 +    _options = new JEdit_Options(Options.init())
   19.10    def options: JEdit_Options = _options
   19.11  
   19.12  
    20.1 --- a/src/Tools/jEdit/src/session_build.scala	Fri Mar 01 20:16:26 2019 +0100
    20.2 +++ b/src/Tools/jEdit/src/session_build.scala	Fri Mar 01 21:29:59 2019 +0100
    20.3 @@ -27,7 +27,7 @@
    20.4  
    20.5      val options = PIDE.options.value
    20.6      try {
    20.7 -      if (JEdit_Sessions.session_build_mode() == "none" ||
    20.8 +      if (JEdit_Sessions.session_no_build ||
    20.9            JEdit_Sessions.session_build(options, no_build = true) == 0)
   20.10              JEdit_Sessions.session_start(options)
   20.11        else new Dialog(view)