system option "system_heaps" supersedes various command-line options for "system build mode";
clarified "isabelle jedit" options -n, -s, -u;
--- a/NEWS Fri Mar 01 20:16:26 2019 +0100
+++ b/NEWS Fri Mar 01 21:29:59 2019 +0100
@@ -75,6 +75,11 @@
the shell function "isabelle_file_format" in etc/settings (e.g. of an
Isabelle component).
+* Command-line options "-s" and "-u" of "isabelle jedit" override the
+default for system option "system_heaps" that determines the heap
+storage directory for "isabelle build". Option "-n" is now clearly
+separated from option "-s".
+
*** Isar ***
@@ -232,6 +237,11 @@
*** System ***
+* The system option "system_heaps" determines where to store the session
+image of "isabelle build" (and other tools using that internally).
+Former option "-s" is superseded by option "-o system_heaps".
+INCOMPATIBILITY in command-line syntax.
+
* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
--- a/etc/options Fri Mar 01 20:16:26 2019 +0100
+++ b/etc/options Fri Mar 01 21:29:59 2019 +0100
@@ -116,6 +116,9 @@
option profiling : string = ""
-- "ML profiling (possible values: time, allocations)"
+option system_heaps : bool = false
+ -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
+
section "ML System"
--- a/src/Doc/JEdit/JEdit.thy Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Mar 01 21:29:59 2019 +0100
@@ -243,7 +243,8 @@
-m MODE add print mode for output
-n no build of session image on startup
-p CMD ML process command prefix (process policy)
- -s system build mode for session image
+ -s system build mode for session image (system_heaps=true)
+ -u user build mode for session image (system_heaps=false)
Start jEdit with Isabelle plugin setup and open FILES
(default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
@@ -252,9 +253,10 @@
for proof processing. Additional session root directories may be included
via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
"isabelle-system"}). By default, the specified image is checked and built on
- demand. The \<^verbatim>\<open>-s\<close> option determines where to store the result session image
- of @{tool build}. The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for
- the selected session image.
+ demand, but option \<^verbatim>\<open>-n\<close> bypasses the implicit build process for the
+ selected session image. Options \<^verbatim>\<open>-s\<close> and \<^verbatim>\<open>-u\<close> override the default system
+ option @{system_option system_heaps}: this determines where to store the
+ session image of @{tool build}.
The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from
other sessions that are not already present in its parent; it also opens the
--- a/src/Doc/System/Environment.thy Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Doc/System/Environment.thy Fri Mar 01 21:29:59 2019 +0100
@@ -181,9 +181,10 @@
used instead; its default is \<^path>\<open>$ISABELLE_HOME/browser_info\<close>.
\<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images,
- log files, and build databases are stored; its default is \<^path>\<open>$ISABELLE_HOME_USER/heaps\<close>. For ``system build mode'' (see
- \secref{sec:tool-build}), @{setting_def ISABELLE_HEAPS_SYSTEM} is used
- instead; its default is \<^path>\<open>$ISABELLE_HOME/heaps\<close>.
+ log files, and build databases are stored; its default is
+ \<^path>\<open>$ISABELLE_HOME_USER/heaps\<close>. If @{system_option system_heaps} is
+ \<^verbatim>\<open>true\<close>, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default
+ is \<^path>\<open>$ISABELLE_HOME/heaps\<close>. See also \secref{sec:tool-build}.
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
@@ -410,7 +411,6 @@
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-r bootstrap from raw Poly/ML
- -s system build mode for session image
Build a logic session image and run the raw Isabelle ML process
in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
@@ -429,9 +429,6 @@
Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
(\secref{sec:tool-process}).
- Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
- (\secref{sec:tool-build}).
-
\<^medskip>
The Isabelle/ML process is run through the line editor that is specified via
the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
--- a/src/Doc/System/Server.thy Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Doc/System/Server.thy Fri Mar 01 21:29:59 2019 +0100
@@ -655,7 +655,6 @@
\quad~~\<open>options?: [string],\<close> \\
\quad~~\<open>dirs?: [string],\<close> \\
\quad~~\<open>include_sessions: [string],\<close> \\
- \quad~~\<open>system_mode?: bool,\<close> \\
\quad~~\<open>verbose?: bool}\<close> \\[2ex]
\end{tabular}
@@ -724,10 +723,6 @@
in a robust manner, instead of relying on directory locations.
\<^medskip>
- 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
- option \<^verbatim>\<open>-s\<close> in @{tool build} (\secref{sec:tool-build}).
-
- \<^medskip>
The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
\<close>
--- a/src/Doc/System/Sessions.thy Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Doc/System/Sessions.thy Fri Mar 01 21:29:59 2019 +0100
@@ -238,6 +238,13 @@
\<^ML>\<open>profile_time\<close> and \<^verbatim>\<open>allocations\<close> for \<^ML>\<open>profile_allocations\<close>.
Results appear near the bottom of the session log file.
+ \<^item> @{system_option_def "system_heaps"} determines the directories for
+ session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and
+ \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> the system directory (usually within the
+ Isabelle application). For \<^verbatim>\<open>system_heaps=false\<close>, heaps are stored in the
+ user directory and may be loaded from both directories. For
+ \<^verbatim>\<open>system_heaps=true\<close>, store and load happens only in the system directory.
+
The @{tool_def options} tool prints Isabelle system options. Its
command-line usage is:
@{verbatim [display]
@@ -297,7 +304,6 @@
-l list session source files
-n no build -- test dependencies only
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode: produce output in ISABELLE_HOME
-v verbose
-x NAME exclude session NAME and all descendants
@@ -403,10 +409,6 @@
performance tuning on Linux servers with separate CPU/memory modules.
\<^medskip>
- Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that session images are
- stored in \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> instead of \<^path>\<open>$ISABELLE_HEAPS\<close>.
-
- \<^medskip>
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
the source files that contribute to a session.
@@ -572,7 +574,6 @@
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NUM prune path of exported files by NUM elements
- -s system build mode for session image
-x PATTERN extract files matching pattern (e.g.\ "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
@@ -584,9 +585,9 @@
\<^medskip>
The specified session is updated via @{tool build}
- (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close>. The
- option \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a
- potentially outdated session database is used!
+ (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>. The option
+ \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a potentially
+ outdated session database is used!
\<^medskip>
Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names
@@ -630,7 +631,6 @@
-g NAME select session group NAME
-l NAME logic session name (default ISABELLE_LOGIC="HOL")
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode for logic image
-v verbose
-x NAME exclude session NAME and all descendants
@@ -645,8 +645,7 @@
\<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
its theories are not processed again, and their PIDE session database is
- excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
- the logic image (\secref{sec:tool-build}).
+ excluded from the dump.
\<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
(\secref{sec:tool-build}).
@@ -708,7 +707,6 @@
-g NAME select session group NAME
-l NAME logic session name (default ISABELLE_LOGIC="HOL")
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode for logic image
-u OPT overide update option: shortcut for "-o update_OPT"
-v verbose
-x NAME exclude session NAME and all descendants
@@ -719,8 +717,7 @@
remaining command-line arguments specify sessions as in @{tool build}
(\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
- \<^medskip> Options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-s\<close> specify the underlying logic image is in @{tool
- dump} (\secref{sec:tool-dump}).
+ \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies the underlying logic image.
\<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
--- a/src/Pure/Admin/build_doc.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Admin/build_doc.scala Fri Mar 01 21:29:59 2019 +0100
@@ -19,7 +19,6 @@
progress: Progress = No_Progress,
all_docs: Boolean = false,
max_jobs: Int = 1,
- system_mode: Boolean = false,
docs: List[String] = Nil): Int =
{
val sessions_structure = Sessions.load_structure(options)
@@ -44,7 +43,7 @@
val res1 =
Build.build(options, progress, requirements = true, build_heap = true,
- max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
+ max_jobs = max_jobs, sessions = sessions)
if (res1.ok) {
Isabelle_System.with_tmp_dir("document_output")(output =>
{
@@ -53,8 +52,7 @@
options.bool.update("browser_info", false).
string.update("document", "pdf").
string.update("document_output", output.implode),
- progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
- sessions = sessions)
+ progress, clean_build = true, max_jobs = max_jobs, sessions = sessions)
if (res2.ok) {
val doc_dir = Path.explode("~~/doc")
for (doc <- selected_docs) {
@@ -76,7 +74,7 @@
{
var all_docs = false
var max_jobs = 1
- var system_mode = false
+ var options = Options.init()
val getopts =
Getopts("""
@@ -85,24 +83,23 @@
Options are:
-a select all documentation sessions
-j INT maximum number of parallel jobs (default 1)
- -s system build mode
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
Build Isabelle documentation from documentation sessions with
suitable document_variants entry.
""",
"a" -> (_ => all_docs = true),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
- "s" -> (_ => system_mode = true))
+ "o:" -> (arg => options = options + arg))
val docs = getopts(args)
if (!all_docs && docs.isEmpty) getopts.usage()
- val options = Options.init()
val progress = new Console_Progress()
val rc =
progress.interrupt_handler {
- build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
+ build_doc(options, progress, all_docs, max_jobs, docs)
}
sys.exit(rc)
})
--- a/src/Pure/Admin/ci_profile.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Admin/ci_profile.scala Fri Mar 01 21:29:59 2019 +0100
@@ -20,7 +20,7 @@
val start_time = Time.now()
val results = progress.interrupt_handler {
Build.build(
- options = options,
+ options = options + "system_heaps",
progress = progress,
clean_build = clean,
verbose = true,
@@ -28,7 +28,6 @@
max_jobs = jobs,
dirs = include,
select_dirs = select,
- system_mode = true,
selection = selection)
}
val end_time = Time.now()
--- a/src/Pure/ML/ml_console.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Mar 01 21:29:59 2019 +0100
@@ -21,7 +21,6 @@
var no_build = false
var options = Options.init()
var raw_ml_system = false
- var system_mode = false
val getopts = Getopts("""
Usage: isabelle console [OPTIONS]
@@ -34,7 +33,6 @@
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-r bootstrap from raw Poly/ML
- -s system build mode for session image
Build a logic session image and run the raw Isabelle ML process
in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
@@ -46,8 +44,7 @@
"m:" -> (arg => modes = arg :: modes),
"n" -> (arg => no_build = true),
"o:" -> (arg => options = options + arg),
- "r" -> (_ => raw_ml_system = true),
- "s" -> (_ => system_mode = true))
+ "r" -> (_ => raw_ml_system = true))
val more_args = getopts(args)
if (!more_args.isEmpty) getopts.usage()
@@ -58,8 +55,7 @@
val progress = new Console_Progress()
val rc =
progress.interrupt_handler {
- Build.build_logic(options, logic, build_heap = true, progress = progress,
- dirs = dirs, system_mode = system_mode)
+ Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
}
if (rc != 0) sys.exit(rc)
}
@@ -69,7 +65,7 @@
ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system,
- store = Some(Sessions.store(options, system_mode)),
+ store = Some(Sessions.store(options)),
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(
--- a/src/Pure/Thy/export.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Thy/export.scala Fri Mar 01 21:29:59 2019 +0100
@@ -322,7 +322,6 @@
var no_build = false
var options = Options.init()
var export_prune = 0
- var system_mode = false
var export_patterns: List[String] = Nil
val getopts = Getopts("""
@@ -335,7 +334,6 @@
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NUM prune path of exported files by NUM elements
- -s system build mode for session image
-x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
@@ -351,7 +349,6 @@
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => export_prune = Value.Int.parse(arg)),
- "s" -> (_ => system_mode = true),
"x:" -> (arg => export_patterns ::= arg))
val more_args = getopts(args)
@@ -369,8 +366,7 @@
if (!no_build) {
val rc =
progress.interrupt_handler {
- Build.build_logic(options, session_name, progress = progress,
- dirs = dirs, system_mode = system_mode)
+ Build.build_logic(options, session_name, progress = progress, dirs = dirs)
}
if (rc != 0) sys.exit(rc)
}
@@ -378,7 +374,7 @@
/* export files */
- val store = Sessions.store(options, system_mode)
+ val store = Sessions.store(options)
export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
export_list = export_list, export_patterns = export_patterns)
})
--- a/src/Pure/Thy/sessions.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Mar 01 21:29:59 2019 +0100
@@ -1079,10 +1079,9 @@
val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
}
- def store(options: Options, system_mode: Boolean = false): Store =
- new Store(options, system_mode)
+ def store(options: Options): Store = new Store(options)
- class Store private[Sessions](val options: Options, val system_mode: Boolean)
+ class Store private[Sessions](val options: Options)
{
override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
@@ -1092,15 +1091,17 @@
val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
+ def system_heaps: Boolean = options.bool("system_heaps")
+
val output_dir: Path =
- if (system_mode) system_output_dir else user_output_dir
+ if (system_heaps) system_output_dir else user_output_dir
val input_dirs: List[Path] =
- if (system_mode) List(system_output_dir)
+ if (system_heaps) List(system_output_dir)
else List(user_output_dir, system_output_dir)
val browser_info: Path =
- if (system_mode) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
+ if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
else Path.explode("$ISABELLE_BROWSER_INFO")
@@ -1184,7 +1185,8 @@
val del =
for {
- dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
+ dir <-
+ (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
file <- List(heap(name), database(name), log(name), log_gz(name))
path = dir + file if path.is_file
} yield path.file.delete
--- a/src/Pure/Tools/build.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Tools/build.scala Fri Mar 01 21:29:59 2019 +0100
@@ -395,7 +395,6 @@
fresh_build: Boolean = false,
no_build: Boolean = false,
soft_build: Boolean = false,
- system_mode: Boolean = false,
verbose: Boolean = false,
export_files: Boolean = false,
pide: Boolean = false,
@@ -410,7 +409,7 @@
{
val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
- val store = Sessions.store(build_options, system_mode)
+ val store = Sessions.store(build_options)
Isabelle_Fonts.init()
@@ -737,7 +736,6 @@
var list_files = false
var no_build = false
var options = Options.init(opts = build_options)
- var system_mode = false
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -764,7 +762,6 @@
-l list session source files
-n no build -- test dependencies only
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode: produce output in ISABELLE_HOME
-v verbose
-x NAME exclude session NAME and all descendants
@@ -790,7 +787,6 @@
"l" -> (_ => list_files = true),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
- "s" -> (_ => system_mode = true),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
@@ -823,7 +819,6 @@
fresh_build = fresh_build,
no_build = no_build,
soft_build = soft_build,
- system_mode = system_mode,
verbose = verbose,
export_files = export_files,
pide = pide,
@@ -857,16 +852,15 @@
progress: Progress = No_Progress,
build_heap: Boolean = false,
dirs: List[Path] = Nil,
- system_mode: Boolean = false,
strict: Boolean = false): Int =
{
val rc =
if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
- system_mode = system_mode, sessions = List(logic)).ok) 0
+ sessions = List(logic)).ok) 0
else {
progress.echo("Build started for Isabelle/" + logic + " ...")
Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
- system_mode = system_mode, sessions = List(logic)).rc
+ sessions = List(logic)).rc
}
if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
--- a/src/Pure/Tools/dump.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Tools/dump.scala Fri Mar 01 21:29:59 2019 +0100
@@ -209,11 +209,10 @@
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
- system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty)
{
Build.build_logic(options, logic, build_heap = true, progress = progress,
- dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
+ dirs = dirs ::: select_dirs, strict = true)
val dump_options = make_options(options, aspects)
@@ -254,7 +253,6 @@
var session_groups: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var options = Options.init()
- var system_mode = false
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -273,7 +271,6 @@
-g NAME select session group NAME
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode for logic image
-v verbose
-x NAME exclude session NAME and all descendants
@@ -291,7 +288,6 @@
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"l:" -> (arg => logic = arg),
"o:" -> (arg => options = options + arg),
- "s" -> (_ => system_mode = true),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
--- a/src/Pure/Tools/server_commands.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Mar 01 21:29:59 2019 +0100
@@ -29,7 +29,6 @@
options: List[String] = Nil,
dirs: List[String] = Nil,
include_sessions: List[String] = Nil,
- system_mode: Boolean = false,
verbose: Boolean = false)
def unapply(json: JSON.T): Option[Args] =
@@ -39,12 +38,11 @@
options <- JSON.strings_default(json, "options")
dirs <- JSON.strings_default(json, "dirs")
include_sessions <- JSON.strings_default(json, "include_sessions")
- system_mode <- JSON.bool_default(json, "system_mode")
verbose <- JSON.bool_default(json, "verbose")
}
yield {
Args(session, preferences = preferences, options = options, dirs = dirs,
- include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
+ include_sessions = include_sessions, verbose = verbose)
}
def command(args: Args, progress: Progress = No_Progress)
@@ -62,7 +60,6 @@
Build.build(options,
progress = progress,
build_heap = true,
- system_mode = args.system_mode,
dirs = dirs,
infos = base_info.infos,
verbose = args.verbose,
--- a/src/Pure/Tools/update.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Pure/Tools/update.scala Fri Mar 01 21:29:59 2019 +0100
@@ -14,11 +14,10 @@
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
- system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty)
{
Build.build_logic(options, logic, build_heap = true, progress = progress,
- dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
+ dirs = dirs ::: select_dirs, strict = true)
val dump_options = Dump.make_options(options)
@@ -82,7 +81,6 @@
var session_groups: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var options = Options.init()
- var system_mode = false
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -99,7 +97,6 @@
-g NAME select session group NAME
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode for logic image
-u OPT overide update option: shortcut for "-o update_OPT"
-v verbose
-x NAME exclude session NAME and all descendants
@@ -115,7 +112,6 @@
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"l:" -> (arg => logic = arg),
"o:" -> (arg => options = options + arg),
- "s" -> (_ => system_mode = true),
"u:" -> (arg => options = options + ("update_" + arg)),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
--- a/src/Tools/VSCode/src/server.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Tools/VSCode/src/server.scala Fri Mar 01 21:29:59 2019 +0100
@@ -40,7 +40,6 @@
var logic = default_logic
var modes: List[String] = Nil
var options = Options.init()
- var system_mode = false
var verbose = false
val getopts = Getopts("""
@@ -56,7 +55,6 @@
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s system build mode for session image
-v verbose logging
Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
@@ -70,7 +68,6 @@
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"o:" -> (arg => options = options + arg),
- "s" -> (_ => system_mode = true),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -82,7 +79,7 @@
new Server(channel, options, session_name = logic, session_dirs = dirs,
include_sessions = include_sessions, session_ancestor = logic_ancestor,
session_requirements = logic_requirements, session_focus = logic_focus,
- all_known = !logic_focus, modes = modes, system_mode = system_mode, log = log)
+ all_known = !logic_focus, modes = modes, log = log)
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
@@ -112,7 +109,6 @@
session_focus: Boolean = false,
all_known: Boolean = false,
modes: List[String] = Nil,
- system_mode: Boolean = false,
log: Logger = No_Logger)
{
server =>
@@ -279,8 +275,8 @@
val session_base = base_info.check_base
def build(no_build: Boolean = false): Build.Results =
- Build.build(options, build_heap = true, no_build = no_build, system_mode = system_mode,
- dirs = session_dirs, infos = base_info.infos, sessions = List(base_info.session))
+ Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs,
+ infos = base_info.infos, sessions = List(base_info.session))
if (!build(no_build = true).ok) {
val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Mar 01 21:29:59 2019 +0100
@@ -116,7 +116,8 @@
echo " -m MODE add print mode for output"
echo " -n no build of session image on startup"
echo " -p CMD ML process command prefix (process policy)"
- echo " -s system build mode for session image"
+ echo " -s system build mode for session image (system_heaps=true)"
+ echo " -u user build mode for session image (system_heaps=false)"
echo
echo " Start jEdit with Isabelle plugin setup and open FILES"
echo " (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
@@ -150,12 +151,13 @@
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
-JEDIT_BUILD_MODE="normal"
+JEDIT_NO_BUILD=""
+JEDIT_BUILD_MODE="default"
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
+ while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:su" OPT
do
case "$OPT" in
A)
@@ -210,7 +212,7 @@
fi
;;
n)
- JEDIT_BUILD_MODE="none"
+ JEDIT_NO_BUILD="true"
;;
p)
ML_PROCESS_POLICY="$OPTARG"
@@ -218,6 +220,9 @@
s)
JEDIT_BUILD_MODE="system"
;;
+ u)
+ JEDIT_BUILD_MODE="user"
+ ;;
\?)
usage
;;
@@ -425,7 +430,7 @@
if [ "$BUILD_ONLY" = false ]
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
- JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 01 21:29:59 2019 +0100
@@ -18,19 +18,28 @@
{
/* session options */
- def session_options(options: Options): Options =
- Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
- case "" => options
- case s => options.string.update("ML_process_policy", s)
- }
-
def session_dirs(): List[Path] =
Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
- def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+ def session_no_build(): Boolean =
+ Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
- def session_system_mode(): Boolean =
- session_build_mode() match { case "" | "system" => true case _ => false }
+ def session_options(options: Options): Options =
+ {
+ val options1 =
+ Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
+ case "default" => options
+ case mode => options.bool.update("system_heaps", mode == "" | mode == "system")
+ }
+
+ val options2 =
+ Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
+ case "" => options1
+ case s => options1.string.update("ML_process_policy", s)
+ }
+
+ options2
+ }
def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
Sessions.load_structure(session_options(options), dirs = dirs)
@@ -123,17 +132,18 @@
options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
{
Build.build(session_options(options), progress = progress, build_heap = true,
- no_build = no_build, system_mode = session_system_mode(),
- dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
+ no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
sessions = List(PIDE.resources.session_name)).rc
}
- def session_start(options: Options)
+ def session_start(options0: Options)
{
- Isabelle_Process.start(PIDE.session, session_options(options),
+ val options = session_options(options0)
+
+ Isabelle_Process.start(PIDE.session, options,
sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
logic = PIDE.resources.session_name,
- store = Some(Sessions.store(options, session_system_mode())),
+ store = Some(Sessions.store(options)),
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
--- a/src/Tools/jEdit/src/plugin.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Mar 01 21:29:59 2019 +0100
@@ -65,7 +65,8 @@
/* options */
private var _options: JEdit_Options = null
- private def init_options(): Unit = _options = new JEdit_Options(Options.init())
+ private def init_options(): Unit =
+ _options = new JEdit_Options(Options.init())
def options: JEdit_Options = _options
--- a/src/Tools/jEdit/src/session_build.scala Fri Mar 01 20:16:26 2019 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Fri Mar 01 21:29:59 2019 +0100
@@ -27,7 +27,7 @@
val options = PIDE.options.value
try {
- if (JEdit_Sessions.session_build_mode() == "none" ||
+ if (JEdit_Sessions.session_no_build ||
JEdit_Sessions.session_build(options, no_build = true) == 0)
JEdit_Sessions.session_start(options)
else new Dialog(view)