--- a/NEWS Wed Mar 16 14:05:30 2016 +0000
+++ b/NEWS Wed Mar 16 22:42:15 2016 +0100
@@ -58,16 +58,16 @@
- Logical representation:
* 0 is instantiated to the ASCII zero character.
- * All other characters are represented as »Char n«
+ * All other characters are represented as "Char n"
with n being a raw numeral expression less than 256.
- * Expressions of the form »Char n« with n greater than 255
+ * Expressions of the form "Char n" with n greater than 255
are non-canonical.
- Printing and parsing:
- * Printable characters are printed and parsed as »CHR ''…''«
+ * Printable characters are printed and parsed as "CHR ''\<dots>''"
(as before).
- * The ASCII zero character is printed and parsed as »0«.
- * All other canonical characters are printed as »CHAR 0xXX«
- with XX being the hexadecimal character code. »CHAR n«
+ * The ASCII zero character is printed and parsed as "0".
+ * All other canonical characters are printed as "CHAR 0xXX"
+ with XX being the hexadecimal character code. "CHAR n"
is parsable for every numeral expression n.
* Non-canonical characters have no special syntax and are
printed as their logical representation.
@@ -281,6 +281,9 @@
* SML/NJ and old versions of Poly/ML are no longer supported.
+* Poly/ML heaps now follow the hierarchy of sessions, and thus require
+much less disk space.
+
New in Isabelle2016 (February 2016)
--- a/src/Doc/ROOT Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Doc/ROOT Wed Mar 16 22:42:15 2016 +0100
@@ -357,7 +357,7 @@
session System (doc) in "System" = Pure +
options [document_variants = "system", thy_output_source]
theories
- Basics
+ Environment
Sessions
Presentation
Scala
--- a/src/Doc/System/Basics.thy Wed Mar 16 14:05:30 2016 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,438 +0,0 @@
-(*:maxLineLen=78:*)
-
-theory Basics
-imports Base
-begin
-
-chapter \<open>The Isabelle system environment\<close>
-
-text \<open>
- This manual describes Isabelle together with related tools as seen from a
- system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
- "isabelle-isar-ref"} for the actual Isabelle input language and related
- concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
- "isabelle-implementation"} for the main concepts of the underlying
- implementation in Isabelle/ML.
-\<close>
-
-
-section \<open>Isabelle settings \label{sec:settings}\<close>
-
-text \<open>
- Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
- process environment. This is a statically scoped collection of environment
- variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
- ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
- shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
- explained below.
-\<close>
-
-
-subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
-
-text \<open>
- Isabelle executables need to be run within a proper settings environment.
- This is bootstrapped as described below, on the first invocation of one of
- the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
- only once for each process tree, i.e.\ the environment is passed to
- subprocesses according to regular Unix conventions.
-
- \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
- automatically from the location of the binary that has been run.
-
- You should not try to set @{setting ISABELLE_HOME} manually. Also note
- that the Isabelle executables either have to be run from their original
- location in the distribution directory, or via the executable objects
- created by the @{tool install} tool. Symbolic links are admissible, but a
- plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
-
- \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
- @{executable_ref bash} shell script with the auto-export option for
- variables enabled.
-
- This file holds a rather long list of shell variable assignments, thus
- providing the site-wide default settings. The Isabelle distribution
- already contains a global settings file with sensible defaults for most
- variables. When installing the system, only a few of these may have to be
- adapted (probably @{setting ML_SYSTEM} etc.).
-
- \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
- exists) is run in the same way as the site default settings. Note that the
- variable @{setting ISABELLE_HOME_USER} has already been set before ---
- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
-
- Thus individual users may override the site-wide defaults. Typically, a
- user settings file contains only a few lines, with some assignments that
- are actually changed. Never copy the central @{file
- "$ISABELLE_HOME/etc/settings"} file!
-
- Since settings files are regular GNU @{executable_def bash} scripts, one may
- use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
- variables depending on the system architecture or other environment
- variables. Such advanced features should be added only with great care,
- though. In particular, external environment references should be kept at a
- minimum.
-
- \<^medskip>
- A few variables are somewhat special:
-
- \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
- name of the @{executable isabelle} executables.
-
- \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
- distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
- @{setting ML_IDENTIFIER}) appended automatically to its value.
-
- \<^medskip>
- Note that the settings environment may be inspected with the @{tool getenv}
- tool. This might help to figure out the effect of complex settings scripts.
-\<close>
-
-
-subsection \<open>Common variables\<close>
-
-text \<open>
- This is a reference of common Isabelle settings variables. Note that the
- list is somewhat open-ended. Third-party utilities or interfaces may add
- their own selection. Variables that are special in some sense are marked
- with \<open>\<^sup>*\<close>.
-
- \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
- On Unix systems this is usually the same as @{setting HOME}, but on Windows
- it is the regular home directory of the user, not the one of within the
- Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
- HOME should point to the @{file_unchecked "/home"} directory tree or the
- Windows user home.\<close>
-
- \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
- Isabelle distribution directory. This is automatically determined from the
- Isabelle executable that has been invoked. Do not attempt to set @{setting
- ISABELLE_HOME} yourself from the shell!
-
- \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
- @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
- "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
- global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
- mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
- defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
-
- \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
- general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
- platform-dependent tools usually need to refer to the more specific
- identification according to @{setting ISABELLE_PLATFORM}, @{setting
- ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
-
- \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
- identifier for the underlying hardware and operating system. The Isabelle
- platform identification always refers to the 32 bit variant, even this is a
- 64 bit machine. Note that the ML or Java runtime may have a different idea,
- depending on which binaries are actually run.
-
- \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
- ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
- that supports this; the value is empty for 32 bit. Note that the following
- bash expression (including the quotes) prefers the 64 bit platform, if that
- is available:
-
- @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
-
- \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
- of the @{executable isabelle} executable. Thus other tools and scripts need
- not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
- search path of the shell.
-
- \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
-
- \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
- ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
- specify the underlying ML system to be used for Isabelle. There is only a
- fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
- "$ISABELLE_HOME/etc/settings"} file of the distribution).
-
- The actual compiler binary will be run from the directory @{setting
- ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
- The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
- images, which is useful for cross-platform installations. The value of
- @{setting ML_IDENTIFIER} is automatically obtained by composing the values
- of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
- values.
-
- \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
- Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
- essential for Isabelle/Scala and other JVM-based tools to work properly.
- Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
- Environment), not JDK.
-
- \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
- colons) where Isabelle logic images may reside. When looking up heaps files,
- the value of @{setting ML_IDENTIFIER} is appended to each component
- internally.
-
- \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
- should be stored by default. The ML system and Isabelle version identifier
- is appended here, too.
-
- \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
- browser information is stored as HTML and PDF (see also \secref{sec:info}).
- The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
-
- \<^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>.
-
- \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
- @{tool_ref console} interface.
-
- \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
- @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
- document preparation (see also \secref{sec:tool-latex}).
-
- \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
- that are scanned by @{executable isabelle} for external utility programs
- (see also \secref{sec:isabelle-tool}).
-
- \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
- with documentation files.
-
- \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
- \<^verbatim>\<open>pdf\<close> files.
-
- \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
- \<^verbatim>\<open>dvi\<close> files.
-
- \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
- running Isabelle ML process derives an individual directory for temporary
- files.
-\<close>
-
-
-subsection \<open>Additional components \label{sec:components}\<close>
-
-text \<open>
- Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
- general layout conventions are that of the main Isabelle distribution
- itself, and the following two files (both optional) have a special meaning:
-
- \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
- bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
- usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
- component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
-
- For example, the following setting allows to refer to files within the
- component later on, without having to hardwire absolute paths:
- @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
-
- Components can also add to existing Isabelle settings such as
- @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
- tools that can be invoked by end-users. For example:
- @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
-
- \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
- structure. The directory specifications given here can be either absolute
- (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
-
- The root of component initialization is @{setting ISABELLE_HOME} itself.
- After initializing all of its sub-components recursively, @{setting
- ISABELLE_HOME_USER} is included in the same manner (if that directory
- exists). This allows to install private components via @{file_unchecked
- "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
- to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
- \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
- directory). For example:
- @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
-
- This is tolerant wrt.\ missing component directories, but might produce a
- warning.
-
- \<^medskip>
- More complex situations may be addressed by initializing components listed
- in a given catalog file, relatively to some base directory:
- @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
-
- The component directories listed in the catalog file are treated as relative
- to the given base directory.
-
- See also \secref{sec:tool-components} for some tool-support for resolving
- components that are formally initialized but not installed yet.
-\<close>
-
-
-section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
-
-text \<open>
- The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
- Isabelle related utilities, user interfaces etc. Such tools automatically
- benefit from the settings mechanism. All Isabelle command-line tools are
- invoked via a common wrapper --- @{executable_ref isabelle}:
- @{verbatim [display]
-\<open>Usage: isabelle TOOL [ARGS ...]
-
- Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
-
-Available tools:
- ...\<close>}
-
- In principle, Isabelle tools are ordinary executable scripts that are run
- within the Isabelle settings environment, see \secref{sec:settings}. The set
- of available tools is collected by @{executable isabelle} from the
- directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
- call the scripts directly from the shell. Neither should you add the tool
- directories to your shell's search path!
-\<close>
-
-
-subsubsection \<open>Examples\<close>
-
-text \<open>
- Show the list of available documentation of the Isabelle distribution:
- @{verbatim [display] \<open>isabelle doc\<close>}
-
- View a certain document as follows:
- @{verbatim [display] \<open>isabelle doc system\<close>}
-
- Query the Isabelle settings environment:
- @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
-\<close>
-
-
-section \<open>The raw Isabelle ML process\<close>
-
-subsection \<open>Batch mode \label{sec:tool-process}\<close>
-
-text \<open>
- The @{tool_def process} tool runs the raw ML process in batch mode:
- @{verbatim [display]
-\<open>Usage: isabelle process [OPTIONS] [HEAP]
-
- Options are:
- -e ML_EXPR evaluate ML expression on startup
- -f ML_FILE evaluate ML file on startup
- -m MODE add print mode for output
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-
- Run the raw Isabelle ML process in batch mode, using a given heap image.
-
- If HEAP is a plain name (default ISABELLE_LOGIC), it is searched in
- ISABELLE_PATH; if it contains a slash, it is taken as literal file;
- if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
-
- Heap files without explicit directory specifications are looked up in the
- @{setting ISABELLE_PATH} setting, which may consist of multiple components
- separated by colons --- these are tried in the given order with the value of
- @{setting ML_IDENTIFIER} appended internally.
-\<close>
-
-
-subsubsection \<open>Options\<close>
-
-text \<open>
- Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
- started. The source is either given literally or taken from a file. Multiple
- \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
- premature exit of the ML process with return code 1.
-
- \<^medskip>
- The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
- session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
- mathematical Isabelle symbols.
-
- \<^medskip>
- Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
- see also \secref{sec:system-options}.
-\<close>
-
-
-subsubsection \<open>Example\<close>
-
-text \<open>
- The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
- loader within ML:
- @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
-
- Observe the delicate quoting rules for the Bash shell vs.\ ML. The
- Isabelle/ML and Scala libraries provide functions for that, but here we need
- to do it manually.
-\<close>
-
-
-subsection \<open>Interactive mode\<close>
-
-text \<open>
- The @{tool_def console} tool runs the raw ML process with interactive
- console and line editor:
- @{verbatim [display]
-\<open>Usage: isabelle console [OPTIONS]
-
- Options are:
- -d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC)
- -m MODE add print mode for output
- -n no build of session image on startup
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is RAW_ML_SYSTEM
- -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>}
-
- Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
- checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
- abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
- Isabelle/Pure interactively.
-
- Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
- (\secref{sec:tool-build}).
-
- Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
- (\secref{sec:tool-process}).
-
- \<^medskip>
- The Isabelle/ML process is run through the line editor that is specified via
- the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
- @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
- standard input/output.
-
- The user is connected to the raw ML toplevel loop: this is neither
- Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
- relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
- use_thys}.
-\<close>
-
-
-section \<open>YXML versus XML\<close>
-
-text \<open>
- Isabelle tools often use YXML, which is a simple and efficient syntax for
- untyped XML trees. The YXML format is defined as follows.
-
- \<^enum> The encoding is always UTF-8.
-
- \<^enum> Body text is represented verbatim (no escaping, no special treatment of
- white space, no named entities, no CDATA chunks, no comments).
-
- \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
- and \<open>\<^bold>Y = 6\<close> as follows:
-
- \begin{tabular}{ll}
- XML & YXML \\\hline
- \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
- \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
- \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
- \end{tabular}
-
- There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
- like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
- well-formed XML documents.
-
- Parsing YXML is pretty straight-forward: split the text into chunks
- separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
- Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
- indicates close of an element. Any other non-empty chunk consists of plain
- text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
- "~~/src/Pure/PIDE/yxml.scala"}.
-
- YXML documents may be detected quickly by checking that the first two
- characters are \<open>\<^bold>X\<^bold>Y\<close>.
-\<close>
-
-end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/System/Environment.thy Wed Mar 16 22:42:15 2016 +0100
@@ -0,0 +1,434 @@
+ (*:maxLineLen=78:*)
+
+theory Environment
+imports Base
+begin
+
+chapter \<open>The Isabelle system environment\<close>
+
+text \<open>
+ This manual describes Isabelle together with related tools as seen from a
+ system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
+ "isabelle-isar-ref"} for the actual Isabelle input language and related
+ concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
+ "isabelle-implementation"} for the main concepts of the underlying
+ implementation in Isabelle/ML.
+\<close>
+
+
+section \<open>Isabelle settings \label{sec:settings}\<close>
+
+text \<open>
+ Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
+ process environment. This is a statically scoped collection of environment
+ variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
+ ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
+ shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
+ explained below.
+\<close>
+
+
+subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
+
+text \<open>
+ Isabelle executables need to be run within a proper settings environment.
+ This is bootstrapped as described below, on the first invocation of one of
+ the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
+ only once for each process tree, i.e.\ the environment is passed to
+ subprocesses according to regular Unix conventions.
+
+ \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
+ automatically from the location of the binary that has been run.
+
+ You should not try to set @{setting ISABELLE_HOME} manually. Also note
+ that the Isabelle executables either have to be run from their original
+ location in the distribution directory, or via the executable objects
+ created by the @{tool install} tool. Symbolic links are admissible, but a
+ plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
+
+ \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
+ @{executable_ref bash} shell script with the auto-export option for
+ variables enabled.
+
+ This file holds a rather long list of shell variable assignments, thus
+ providing the site-wide default settings. The Isabelle distribution
+ already contains a global settings file with sensible defaults for most
+ variables. When installing the system, only a few of these may have to be
+ adapted (probably @{setting ML_SYSTEM} etc.).
+
+ \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
+ exists) is run in the same way as the site default settings. Note that the
+ variable @{setting ISABELLE_HOME_USER} has already been set before ---
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
+
+ Thus individual users may override the site-wide defaults. Typically, a
+ user settings file contains only a few lines, with some assignments that
+ are actually changed. Never copy the central @{file
+ "$ISABELLE_HOME/etc/settings"} file!
+
+ Since settings files are regular GNU @{executable_def bash} scripts, one may
+ use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
+ variables depending on the system architecture or other environment
+ variables. Such advanced features should be added only with great care,
+ though. In particular, external environment references should be kept at a
+ minimum.
+
+ \<^medskip>
+ A few variables are somewhat special:
+
+ \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
+ name of the @{executable isabelle} executables.
+
+ \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
+ distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
+ @{setting ML_IDENTIFIER}) appended automatically to its value.
+
+ \<^medskip>
+ Note that the settings environment may be inspected with the @{tool getenv}
+ tool. This might help to figure out the effect of complex settings scripts.
+\<close>
+
+
+subsection \<open>Common variables\<close>
+
+text \<open>
+ This is a reference of common Isabelle settings variables. Note that the
+ list is somewhat open-ended. Third-party utilities or interfaces may add
+ their own selection. Variables that are special in some sense are marked
+ with \<open>\<^sup>*\<close>.
+
+ \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
+ On Unix systems this is usually the same as @{setting HOME}, but on Windows
+ it is the regular home directory of the user, not the one of within the
+ Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
+ HOME should point to the @{file_unchecked "/home"} directory tree or the
+ Windows user home.\<close>
+
+ \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
+ Isabelle distribution directory. This is automatically determined from the
+ Isabelle executable that has been invoked. Do not attempt to set @{setting
+ ISABELLE_HOME} yourself from the shell!
+
+ \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
+ @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
+ "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
+ global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
+ mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
+ defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
+
+ \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
+ general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
+ platform-dependent tools usually need to refer to the more specific
+ identification according to @{setting ISABELLE_PLATFORM}, @{setting
+ ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
+
+ \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
+ identifier for the underlying hardware and operating system. The Isabelle
+ platform identification always refers to the 32 bit variant, even this is a
+ 64 bit machine. Note that the ML or Java runtime may have a different idea,
+ depending on which binaries are actually run.
+
+ \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
+ ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
+ that supports this; the value is empty for 32 bit. Note that the following
+ bash expression (including the quotes) prefers the 64 bit platform, if that
+ is available:
+
+ @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
+
+ \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
+ of the @{executable isabelle} executable. Thus other tools and scripts need
+ not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
+ search path of the shell.
+
+ \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
+
+ \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
+ ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
+ specify the underlying ML system to be used for Isabelle. There is only a
+ fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
+ "$ISABELLE_HOME/etc/settings"} file of the distribution).
+
+ The actual compiler binary will be run from the directory @{setting
+ ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
+ The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
+ images, which is useful for cross-platform installations. The value of
+ @{setting ML_IDENTIFIER} is automatically obtained by composing the values
+ of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
+ values.
+
+ \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
+ Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
+ essential for Isabelle/Scala and other JVM-based tools to work properly.
+ Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
+ Environment), not JDK.
+
+ \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
+ colons) where Isabelle logic images may reside. When looking up heaps files,
+ the value of @{setting ML_IDENTIFIER} is appended to each component
+ internally.
+
+ \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
+ should be stored by default. The ML system and Isabelle version identifier
+ is appended here, too.
+
+ \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
+ browser information is stored as HTML and PDF (see also \secref{sec:info}).
+ The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
+
+ \<^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>.
+
+ \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
+ @{tool_ref console} interface.
+
+ \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
+ @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
+ document preparation (see also \secref{sec:tool-latex}).
+
+ \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
+ that are scanned by @{executable isabelle} for external utility programs
+ (see also \secref{sec:isabelle-tool}).
+
+ \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
+ with documentation files.
+
+ \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
+ \<^verbatim>\<open>pdf\<close> files.
+
+ \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
+ \<^verbatim>\<open>dvi\<close> files.
+
+ \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
+ running Isabelle ML process derives an individual directory for temporary
+ files.
+\<close>
+
+
+subsection \<open>Additional components \label{sec:components}\<close>
+
+text \<open>
+ Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
+ general layout conventions are that of the main Isabelle distribution
+ itself, and the following two files (both optional) have a special meaning:
+
+ \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
+ bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
+ usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
+ component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
+
+ For example, the following setting allows to refer to files within the
+ component later on, without having to hardwire absolute paths:
+ @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
+
+ Components can also add to existing Isabelle settings such as
+ @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
+ tools that can be invoked by end-users. For example:
+ @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
+
+ \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
+ structure. The directory specifications given here can be either absolute
+ (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
+
+ The root of component initialization is @{setting ISABELLE_HOME} itself.
+ After initializing all of its sub-components recursively, @{setting
+ ISABELLE_HOME_USER} is included in the same manner (if that directory
+ exists). This allows to install private components via @{file_unchecked
+ "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
+ to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
+ \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
+ directory). For example:
+ @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
+
+ This is tolerant wrt.\ missing component directories, but might produce a
+ warning.
+
+ \<^medskip>
+ More complex situations may be addressed by initializing components listed
+ in a given catalog file, relatively to some base directory:
+ @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
+
+ The component directories listed in the catalog file are treated as relative
+ to the given base directory.
+
+ See also \secref{sec:tool-components} for some tool-support for resolving
+ components that are formally initialized but not installed yet.
+\<close>
+
+
+section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
+
+text \<open>
+ The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
+ Isabelle related utilities, user interfaces etc. Such tools automatically
+ benefit from the settings mechanism. All Isabelle command-line tools are
+ invoked via a common wrapper --- @{executable_ref isabelle}:
+ @{verbatim [display]
+\<open>Usage: isabelle TOOL [ARGS ...]
+
+ Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+
+Available tools:
+ ...\<close>}
+
+ In principle, Isabelle tools are ordinary executable scripts that are run
+ within the Isabelle settings environment, see \secref{sec:settings}. The set
+ of available tools is collected by @{executable isabelle} from the
+ directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
+ call the scripts directly from the shell. Neither should you add the tool
+ directories to your shell's search path!
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Show the list of available documentation of the Isabelle distribution:
+ @{verbatim [display] \<open>isabelle doc\<close>}
+
+ View a certain document as follows:
+ @{verbatim [display] \<open>isabelle doc system\<close>}
+
+ Query the Isabelle settings environment:
+ @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
+\<close>
+
+
+section \<open>The raw Isabelle ML process\<close>
+
+subsection \<open>Batch mode \label{sec:tool-process}\<close>
+
+text \<open>
+ The @{tool_def process} tool runs the raw ML process in batch mode:
+ @{verbatim [display]
+\<open>Usage: isabelle process [OPTIONS]
+
+ Options are:
+ -d DIR include session directory
+ -e ML_EXPR evaluate ML expression on startup
+ -f ML_FILE evaluate ML file on startup
+ -l NAME logic session name (default ISABELLE_LOGIC="HOL")
+ -m MODE add print mode for output
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+
+ Run the raw Isabelle ML process in batch mode.\<close>}
+
+ \<^medskip>
+ Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
+ started. The source is either given literally or taken from a file. Multiple
+ \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
+ premature exit of the ML process with return code 1.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
+ additional directories for session roots, see also \secref{sec:tool-build}.
+
+ \<^medskip>
+ The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
+ session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
+ mathematical Isabelle symbols.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
+ see also \secref{sec:system-options}.
+\<close>
+
+
+subsubsection \<open>Example\<close>
+
+text \<open>
+ The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
+ loader within ML:
+ @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
+
+ Observe the delicate quoting rules for the Bash shell vs.\ ML. The
+ Isabelle/ML and Scala libraries provide functions for that, but here we need
+ to do it manually.
+\<close>
+
+
+subsection \<open>Interactive mode\<close>
+
+text \<open>
+ The @{tool_def console} tool runs the raw ML process with interactive
+ console and line editor:
+ @{verbatim [display]
+\<open>Usage: isabelle console [OPTIONS]
+
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC)
+ -m MODE add print mode for output
+ -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>}
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
+ checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+
+ Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
+ relevant for Isabelle/Pure development.
+
+ \<^medskip>
+ 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.\
+ @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
+ standard input/output.
+
+ The user is connected to the raw ML toplevel loop: this is neither
+ Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
+ relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
+ use_thys}.
+\<close>
+
+
+section \<open>YXML versus XML\<close>
+
+text \<open>
+ Isabelle tools often use YXML, which is a simple and efficient syntax for
+ untyped XML trees. The YXML format is defined as follows.
+
+ \<^enum> The encoding is always UTF-8.
+
+ \<^enum> Body text is represented verbatim (no escaping, no special treatment of
+ white space, no named entities, no CDATA chunks, no comments).
+
+ \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
+ and \<open>\<^bold>Y = 6\<close> as follows:
+
+ \begin{tabular}{ll}
+ XML & YXML \\\hline
+ \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
+ \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
+ \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
+ \end{tabular}
+
+ There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
+ like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
+ well-formed XML documents.
+
+ Parsing YXML is pretty straight-forward: split the text into chunks
+ separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
+ Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
+ indicates close of an element. Any other non-empty chunk consists of plain
+ text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
+ "~~/src/Pure/PIDE/yxml.scala"}.
+
+ YXML documents may be detected quickly by checking that the first two
+ characters are \<open>\<^bold>X\<^bold>Y\<close>.
+\<close>
+
+end
\ No newline at end of file
--- a/src/Doc/System/document/root.tex Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Doc/System/document/root.tex Wed Mar 16 22:42:15 2016 +0100
@@ -30,7 +30,7 @@
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst
-\input{Basics.tex}
+\input{Environment.tex}
\input{Sessions.tex}
\input{Presentation.tex}
\input{Scala.tex}
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 16 22:42:15 2016 +0100
@@ -159,7 +159,7 @@
my $cmd =
"isabelle process -o quick_and_dirty -o threads=1" .
- " -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
+ " -e 'use_thy \"$path/$new_thy_name\"' -l $mirabelle_logic" . $quiet;
my $result = system "bash", "-c", $cmd;
if ($output_log) {
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Wed Mar 16 22:42:15 2016 +0100
@@ -118,7 +118,7 @@
begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
> $WORKDIR/$LOADER.thy
- isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
+ isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" -l Pure
}
function cleanup_workdir()
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Wed Mar 16 22:42:15 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Wed Mar 16 22:42:15 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Wed Mar 16 22:42:15 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Wed Mar 16 22:42:15 2016 +0100
@@ -30,5 +30,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Wed Mar 16 22:42:15 2016 +0100
@@ -31,5 +31,5 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Wed Mar 16 14:05:30 2016 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Wed Mar 16 22:42:15 2016 +0100
@@ -28,4 +28,4 @@
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
> /tmp/$SCRATCH.thy
-isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
--- a/src/Pure/General/file.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/General/file.scala Wed Mar 16 22:42:15 2016 +0100
@@ -254,4 +254,14 @@
}
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
+
+
+ /* approximative time stamp */
+
+ def time_stamp(path: Path): Option[String] =
+ {
+ val file = path.file
+ if (file.isFile) Some(file.length.toString + " " + file.lastModified.toString)
+ else None
+ }
}
--- a/src/Pure/ML/ml_heap.ML Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/ML/ml_heap.ML Wed Mar 16 22:42:15 2016 +0100
@@ -7,11 +7,9 @@
signature ML_HEAP =
sig
val share_common_data: unit -> unit
- val save_state: string -> unit
end;
structure ML_Heap: ML_HEAP =
struct
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
- val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
end;
--- a/src/Pure/ML/ml_syntax.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/ML/ml_syntax.scala Wed Mar 16 22:42:15 2016 +0100
@@ -31,7 +31,7 @@
def print_string(str: String): String =
quote(Symbol.iterator(str).map(print_char(_)).mkString)
- def print_string_raw(str: String): String =
+ def print_string0(str: String): String =
quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
def print_list[A](f: A => String)(list: List[A]): String =
--- a/src/Pure/PIDE/batch_session.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/PIDE/batch_session.scala Wed Mar 16 22:42:15 2016 +0100
@@ -18,15 +18,14 @@
dirs: List[Path] = Nil,
session: String): Batch_Session =
{
- val (_, session_tree) =
- Build.find_sessions(options, dirs).selection(sessions = List(session))
+ val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session))
val session_info = session_tree(session)
val parent_session =
session_info.parent getOrElse error("No parent session for " + quote(session))
- if (Build.build(options, new Console_Progress(verbose),
+ if (!Build.build(options, new Console_Progress(verbose),
verbose = verbose, build_heap = true,
- dirs = dirs, sessions = List(parent_session)) != 0)
+ dirs = dirs, sessions = List(parent_session)).ok)
new RuntimeException
val deps = Build.dependencies(verbose = verbose, tree = session_tree)
@@ -59,7 +58,7 @@
}
prover_session.start(receiver =>
- Isabelle_Process(options, heap = parent_session, receiver = receiver))
+ Isabelle_Process(options, logic = parent_session, receiver = receiver))
batch_session
}
--- a/src/Pure/ROOT.ML Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/ROOT.ML Wed Mar 16 22:42:15 2016 +0100
@@ -1,4 +1,4 @@
-(*** Isabelle/Pure bootstrap from RAW_ML_SYSTEM ***)
+(*** Isabelle/Pure bootstrap ***)
(** bootstrap phase 0: Poly/ML setup **)
--- a/src/Pure/System/isabelle_process.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/System/isabelle_process.scala Wed Mar 16 22:42:15 2016 +0100
@@ -11,17 +11,18 @@
{
def apply(
options: Options,
- heap: String = "",
+ logic: String = "",
args: List[String] = Nil,
modes: List[String] = Nil,
secure: Boolean = false,
- receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
+ receiver: Prover.Receiver = Console.println(_),
+ store: Sessions.Store = Sessions.store()): Isabelle_Process =
{
val channel = System_Channel()
val process =
try {
- ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
- channel = Some(channel))
+ ML_Process(options, logic = logic, args = args, modes = modes, secure = secure,
+ channel = Some(channel), store = store)
}
catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
process.stdin.close
--- a/src/Pure/System/isabelle_system.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/System/isabelle_system.scala Wed Mar 16 22:42:15 2016 +0100
@@ -325,19 +325,7 @@
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
- /* logic images */
-
- def find_logics_dirs(): List[Path] =
- {
- val ml_ident = Path.explode("$ML_IDENTIFIER").expand
- Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
- }
-
- def find_logics(): List[String] =
- (for {
- dir <- find_logics_dirs()
- files = dir.file.listFiles() if files != null
- file <- files.toList if file.isFile } yield file.getName).sorted
+ /* default logic */
def default_logic(args: String*): String =
{
--- a/src/Pure/Thy/present.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/Thy/present.scala Wed Mar 16 22:42:15 2016 +0100
@@ -96,7 +96,7 @@
progress: Progress,
browser_info: Path,
graph_file: JFile,
- info: Build.Session_Info,
+ info: Sessions.Info,
name: String)
{
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/sessions.scala Wed Mar 16 22:42:15 2016 +0100
@@ -0,0 +1,371 @@
+/* Title: Pure/Thy/sessions.scala
+ Author: Makarius
+
+Session information.
+*/
+
+package isabelle
+
+
+import scala.collection.SortedSet
+import scala.collection.mutable
+
+
+object Sessions
+{
+ /* info */
+
+ val ROOT = Path.explode("ROOT")
+ val ROOTS = Path.explode("ROOTS")
+
+ def is_pure(name: String): Boolean = name == "Pure"
+
+ sealed case class Info(
+ chapter: String,
+ select: Boolean,
+ pos: Position.T,
+ groups: List[String],
+ dir: Path,
+ parent: Option[String],
+ description: String,
+ options: Options,
+ theories: List[(Boolean, Options, List[Path])],
+ files: List[Path],
+ document_files: List[(Path, Path)],
+ meta_digest: SHA1.Digest)
+ {
+ def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
+ }
+
+
+ /* session tree */
+
+ object Tree
+ {
+ def apply(infos: Seq[(String, Info)]): Tree =
+ {
+ val graph1 =
+ (Graph.string[Info] /: infos) {
+ case (graph, (name, info)) =>
+ if (graph.defined(name))
+ error("Duplicate session " + quote(name) + Position.here(info.pos) +
+ Position.here(graph.get_node(name).pos))
+ else graph.new_node(name, info)
+ }
+ val graph2 =
+ (graph1 /: graph1.iterator) {
+ case (graph, (name, (info, _))) =>
+ info.parent match {
+ case None => graph
+ case Some(parent) =>
+ if (!graph.defined(parent))
+ error("Bad parent session " + quote(parent) + " for " +
+ quote(name) + Position.here(info.pos))
+
+ try { graph.add_edge_acyclic(parent, name) }
+ catch {
+ case exn: Graph.Cycles[_] =>
+ error(cat_lines(exn.cycles.map(cycle =>
+ "Cyclic session dependency of " +
+ cycle.map(c => quote(c.toString)).mkString(" via "))) +
+ Position.here(info.pos))
+ }
+ }
+ }
+ new Tree(graph2)
+ }
+ }
+
+ final class Tree private(val graph: Graph[String, Info])
+ extends PartialFunction[String, Info]
+ {
+ def apply(name: String): Info = graph.get_node(name)
+ def isDefinedAt(name: String): Boolean = graph.defined(name)
+
+ def selection(
+ requirements: Boolean = false,
+ all_sessions: Boolean = false,
+ exclude_session_groups: List[String] = Nil,
+ exclude_sessions: List[String] = Nil,
+ session_groups: List[String] = Nil,
+ sessions: List[String] = Nil): (List[String], Tree) =
+ {
+ val bad_sessions =
+ SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
+ if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
+
+ val excluded =
+ {
+ val exclude_group = exclude_session_groups.toSet
+ val exclude_group_sessions =
+ (for {
+ (name, (info, _)) <- graph.iterator
+ if apply(name).groups.exists(exclude_group)
+ } yield name).toList
+ graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
+ }
+
+ val pre_selected =
+ {
+ if (all_sessions) graph.keys
+ else {
+ val select_group = session_groups.toSet
+ val select = sessions.toSet
+ (for {
+ (name, (info, _)) <- graph.iterator
+ if info.select || select(name) || apply(name).groups.exists(select_group)
+ } yield name).toList
+ }
+ }.filterNot(excluded)
+
+ val selected =
+ if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
+ else pre_selected
+
+ val graph1 = graph.restrict(graph.all_preds(selected).toSet)
+ (selected, new Tree(graph1))
+ }
+
+ def ancestors(name: String): List[String] =
+ graph.all_preds(List(name)).tail.reverse
+
+ def topological_order: List[(String, Info)] =
+ graph.topological_order.map(name => (name, apply(name)))
+
+ override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
+ }
+
+
+ /* parser */
+
+ private val CHAPTER = "chapter"
+ private val SESSION = "session"
+ private val IN = "in"
+ private val DESCRIPTION = "description"
+ private val OPTIONS = "options"
+ private val GLOBAL_THEORIES = "global_theories"
+ private val THEORIES = "theories"
+ private val FILES = "files"
+ private val DOCUMENT_FILES = "document_files"
+
+ lazy val root_syntax =
+ Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+ (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
+ IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
+
+ object Parser extends Parse.Parser
+ {
+ private abstract class Entry
+ private sealed case class Chapter(name: String) extends Entry
+ private sealed case class Session_Entry(
+ pos: Position.T,
+ name: String,
+ groups: List[String],
+ path: String,
+ parent: Option[String],
+ description: String,
+ options: List[Options.Spec],
+ theories: List[(Boolean, List[Options.Spec], List[String])],
+ files: List[String],
+ document_files: List[(String, String)]) extends Entry
+
+ private val chapter: Parser[Chapter] =
+ {
+ val chapter_name = atom("chapter name", _.is_name)
+
+ command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
+ }
+
+ private val session_entry: Parser[Session_Entry] =
+ {
+ val session_name = atom("session name", _.is_name)
+
+ val option =
+ name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+ val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
+
+ val theories =
+ ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
+ ((options | success(Nil)) ~ rep(theory_xname)) ^^
+ { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
+
+ val document_files =
+ $$$(DOCUMENT_FILES) ~!
+ (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
+ { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
+ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
+
+ command(SESSION) ~!
+ (position(session_name) ~
+ (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
+ ($$$("=") ~!
+ (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
+ (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+ rep1(theories) ~
+ (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (rep(document_files) ^^ (x => x.flatten))))) ^^
+ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
+ Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
+ }
+
+ def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
+ {
+ def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
+ {
+ try {
+ val name = entry.name
+
+ if (name == "") error("Bad session name")
+ if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+ if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
+
+ val session_options = options ++ entry.options
+
+ val theories =
+ entry.theories.map({ case (global, opts, thys) =>
+ (global, session_options ++ opts, thys.map(Path.explode(_))) })
+ val files = entry.files.map(Path.explode(_))
+ val document_files =
+ entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
+
+ val meta_digest =
+ SHA1.digest((entry_chapter, name, entry.parent, entry.options,
+ entry.theories, entry.files, entry.document_files).toString)
+
+ val info =
+ Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+ entry.parent, entry.description, session_options, theories, files,
+ document_files, meta_digest)
+
+ (name, info)
+ }
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session entry " +
+ quote(entry.name) + Position.here(entry.pos))
+ }
+ }
+
+ val root = dir + ROOT
+ if (root.is_file) {
+ val toks = Token.explode(root_syntax.keywords, File.read(root))
+ val start = Token.Pos.file(root.implode)
+
+ parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
+ case Success(result, _) =>
+ var entry_chapter = "Unsorted"
+ val infos = new mutable.ListBuffer[(String, Info)]
+ result.foreach {
+ case Chapter(name) => entry_chapter = name
+ case entry: Session_Entry => infos += make_info(entry_chapter, entry)
+ }
+ infos.toList
+ case bad => error(bad.toString)
+ }
+ }
+ else Nil
+ }
+ }
+
+
+ /* load sessions from certain directories */
+
+ private def is_session_dir(dir: Path): Boolean =
+ (dir + ROOT).is_file || (dir + ROOTS).is_file
+
+ private def check_session_dir(dir: Path): Path =
+ if (is_session_dir(dir)) dir
+ else error("Bad session root directory: " + dir.toString)
+
+ def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
+ {
+ def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
+ load_root(select, dir) ::: load_roots(select, dir)
+
+ def load_root(select: Boolean, dir: Path): List[(String, Info)] =
+ Parser.parse(options, select, dir)
+
+ def load_roots(select: Boolean, dir: Path): List[(String, Info)] =
+ {
+ val roots = dir + ROOTS
+ if (roots.is_file) {
+ for {
+ line <- split_lines(File.read(roots))
+ if !(line == "" || line.startsWith("#"))
+ dir1 =
+ try { check_session_dir(dir + Path.explode(line)) }
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
+ }
+ info <- load_dir(select, dir1)
+ } yield info
+ }
+ else Nil
+ }
+
+ val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+ dirs.foreach(check_session_dir(_))
+ select_dirs.foreach(check_session_dir(_))
+
+ Tree(
+ for {
+ (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
+ info <- load_dir(select, dir)
+ } yield info)
+ }
+
+
+
+ /** persistent store **/
+
+ def log(name: String): Path = Path.basic("log") + Path.basic(name)
+ def log_gz(name: String): Path = log(name).ext("gz")
+
+ def store(system_mode: Boolean = false): Store = new Store(system_mode)
+
+ class Store private [Sessions](system_mode: Boolean)
+ {
+ /* output */
+
+ val browser_info: Path =
+ if (system_mode) Path.explode("~~/browser_info")
+ else Path.explode("$ISABELLE_BROWSER_INFO")
+
+ val output_dir: Path =
+ if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
+ else Path.explode("$ISABELLE_OUTPUT")
+
+ def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
+
+
+ /* input */
+
+ private val input_dirs =
+ if (system_mode) List(output_dir)
+ else {
+ val ml_ident = Path.explode("$ML_IDENTIFIER").expand
+ output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
+ }
+
+ def find(name: String): Option[(Path, Option[String])] =
+ input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
+ (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
+
+ def find_log(name: String): Option[Path] =
+ input_dirs.map(_ + log(name)).find(_.is_file)
+
+ def find_log_gz(name: String): Option[Path] =
+ input_dirs.map(_ + log_gz(name)).find(_.is_file)
+
+ def find_heap(name: String): Option[Path] =
+ input_dirs.map(_ + Path.basic(name)).find(_.is_file)
+
+ def heap(name: String): Path =
+ find_heap(name) getOrElse
+ error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
+ cat_lines(input_dirs.map(dir => " " + dir.implode)))
+ }
+}
--- a/src/Pure/Tools/build.ML Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/Tools/build.ML Wed Mar 16 22:42:15 2016 +0100
@@ -120,54 +120,52 @@
" (undefined " ^ commas conds ^ ")\n")
end;
-fun build args_file = Command_Line.tool0 (fn () =>
- let
- val _ = SHA1_Samples.test ();
+fun build args_file =
+ let
+ val _ = SHA1_Samples.test ();
- val (symbol_codes, (command_timings, (output, (verbose, (browser_info,
- (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
- File.read (Path.explode args_file) |> YXML.parse_body |>
- let open XML.Decode in
- pair (list (pair string int)) (pair (list properties) (pair string
- (pair bool (pair string (pair (list (pair string string)) (pair string
- (pair string (pair string (pair string
- ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
- end;
- val do_output = output <> "";
+ val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
+ (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
+ File.read (Path.explode args_file) |> YXML.parse_body |>
+ let open XML.Decode in
+ pair (list (pair string int)) (pair (list properties) (pair bool
+ (pair bool (pair string (pair (list (pair string string)) (pair string
+ (pair string (pair string (pair string
+ ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
+ end;
- val symbols = HTML.make_symbols symbol_codes;
- val _ = Isabelle_Process.init_build_options ();
+ val symbols = HTML.make_symbols symbol_codes;
+ val _ = Isabelle_Process.init_build_options ();
- val _ = writeln ("\fSession.name = " ^ name);
- val _ =
- Session.init
- symbols
- do_output
- (Options.default_bool "browser_info")
- (Path.explode browser_info)
- (Options.default_string "document")
- (Options.default_string "document_output")
- (Present.document_variants (Options.default_string "document_variants"))
- (map (apply2 Path.explode) document_files)
- (Path.explode graph_file)
- parent_name (chapter, name)
- verbose;
+ val _ = writeln ("\fSession.name = " ^ name);
+ val _ =
+ Session.init
+ symbols
+ do_output
+ (Options.default_bool "browser_info")
+ (Path.explode browser_info)
+ (Options.default_string "document")
+ (Options.default_string "document_output")
+ (Present.document_variants (Options.default_string "document_variants"))
+ (map (apply2 Path.explode) document_files)
+ (Path.explode graph_file)
+ parent_name (chapter, name)
+ verbose;
- val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
+ val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
- val res1 =
- theories |>
- (List.app (build_theories symbols last_timing Path.current)
- |> session_timing name verbose
- |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
- |> Multithreading.max_threads_setmp (Options.default_int "threads")
- |> Exn.capture);
- val res2 = Exn.capture Session.finish ();
- val _ = Par_Exn.release_all [res1, res2];
+ val res1 =
+ theories |>
+ (List.app (build_theories symbols last_timing Path.current)
+ |> session_timing name verbose
+ |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
+ |> Multithreading.max_threads_setmp (Options.default_int "threads")
+ |> Exn.capture);
+ val res2 = Exn.capture Session.finish ();
+ val _ = Par_Exn.release_all [res1, res2];
- val _ = Options.reset_default ();
- val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else ();
- in () end);
+ val _ = Options.reset_default ();
+ in () end;
(* PIDE protocol *)
--- a/src/Pure/Tools/build.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/Tools/build.scala Wed Mar 16 22:42:15 2016 +0100
@@ -19,321 +19,13 @@
object Build
{
- /** session information **/
-
- // external version
- abstract class Entry
- sealed case class Chapter(name: String) extends Entry
- sealed case class Session_Entry(
- pos: Position.T,
- name: String,
- groups: List[String],
- path: String,
- parent: Option[String],
- description: String,
- options: List[Options.Spec],
- theories: List[(Boolean, List[Options.Spec], List[String])],
- files: List[String],
- document_files: List[(String, String)]) extends Entry
-
- // internal version
- sealed case class Session_Info(
- chapter: String,
- select: Boolean,
- pos: Position.T,
- groups: List[String],
- dir: Path,
- parent: Option[String],
- description: String,
- options: Options,
- theories: List[(Boolean, Options, List[Path])],
- files: List[Path],
- document_files: List[(Path, Path)],
- entry_digest: SHA1.Digest)
- {
- def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
- }
-
- def is_pure(name: String): Boolean = name == "Pure"
-
- def session_info(options: Options, select: Boolean, dir: Path,
- chapter: String, entry: Session_Entry): (String, Session_Info) =
- try {
- val name = entry.name
-
- if (name == "") error("Bad session name")
- if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
- if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
-
- val session_options = options ++ entry.options
-
- val theories =
- entry.theories.map({ case (global, opts, thys) =>
- (global, session_options ++ opts, thys.map(Path.explode(_))) })
- val files = entry.files.map(Path.explode(_))
- val document_files =
- entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
-
- val entry_digest =
- SHA1.digest((chapter, name, entry.parent, entry.options,
- entry.theories, entry.files, entry.document_files).toString)
-
- val info =
- Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
- entry.parent, entry.description, session_options, theories, files,
- document_files, entry_digest)
-
- (name, info)
- }
- catch {
- case ERROR(msg) =>
- error(msg + "\nThe error(s) above occurred in session entry " +
- quote(entry.name) + Position.here(entry.pos))
- }
-
-
- /* session tree */
-
- object Session_Tree
- {
- def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
- {
- val graph1 =
- (Graph.string[Session_Info] /: infos) {
- case (graph, (name, info)) =>
- if (graph.defined(name))
- error("Duplicate session " + quote(name) + Position.here(info.pos) +
- Position.here(graph.get_node(name).pos))
- else graph.new_node(name, info)
- }
- val graph2 =
- (graph1 /: graph1.iterator) {
- case (graph, (name, (info, _))) =>
- info.parent match {
- case None => graph
- case Some(parent) =>
- if (!graph.defined(parent))
- error("Bad parent session " + quote(parent) + " for " +
- quote(name) + Position.here(info.pos))
-
- try { graph.add_edge_acyclic(parent, name) }
- catch {
- case exn: Graph.Cycles[_] =>
- error(cat_lines(exn.cycles.map(cycle =>
- "Cyclic session dependency of " +
- cycle.map(c => quote(c.toString)).mkString(" via "))) +
- Position.here(info.pos))
- }
- }
- }
- new Session_Tree(graph2)
- }
- }
-
- final class Session_Tree private(val graph: Graph[String, Session_Info])
- extends PartialFunction[String, Session_Info]
- {
- def apply(name: String): Session_Info = graph.get_node(name)
- def isDefinedAt(name: String): Boolean = graph.defined(name)
-
- def selection(
- requirements: Boolean = false,
- all_sessions: Boolean = false,
- exclude_session_groups: List[String] = Nil,
- exclude_sessions: List[String] = Nil,
- session_groups: List[String] = Nil,
- sessions: List[String] = Nil): (List[String], Session_Tree) =
- {
- val bad_sessions =
- SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
- if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
-
- val excluded =
- {
- val exclude_group = exclude_session_groups.toSet
- val exclude_group_sessions =
- (for {
- (name, (info, _)) <- graph.iterator
- if apply(name).groups.exists(exclude_group)
- } yield name).toList
- graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
- }
-
- val pre_selected =
- {
- if (all_sessions) graph.keys
- else {
- val select_group = session_groups.toSet
- val select = sessions.toSet
- (for {
- (name, (info, _)) <- graph.iterator
- if info.select || select(name) || apply(name).groups.exists(select_group)
- } yield name).toList
- }
- }.filterNot(excluded)
-
- val selected =
- if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
- else pre_selected
-
- val graph1 = graph.restrict(graph.all_preds(selected).toSet)
- (selected, new Session_Tree(graph1))
- }
-
- def topological_order: List[(String, Session_Info)] =
- graph.topological_order.map(name => (name, apply(name)))
-
- override def toString: String = graph.keys_iterator.mkString("Session_Tree(", ", ", ")")
- }
-
-
- /* parser */
-
- val chapter_default = "Unsorted"
-
- private val CHAPTER = "chapter"
- private val SESSION = "session"
- private val IN = "in"
- private val DESCRIPTION = "description"
- private val OPTIONS = "options"
- private val GLOBAL_THEORIES = "global_theories"
- private val THEORIES = "theories"
- private val FILES = "files"
- private val DOCUMENT_FILES = "document_files"
-
- lazy val root_syntax =
- Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
- (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
- IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
-
- object Parser extends Parse.Parser
- {
- private val chapter: Parser[Chapter] =
- {
- val chapter_name = atom("chapter name", _.is_name)
-
- command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
- }
-
- private val session_entry: Parser[Session_Entry] =
- {
- val session_name = atom("session name", _.is_name)
-
- val option =
- name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
- val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
-
- val theories =
- ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
- ((options | success(Nil)) ~ rep(theory_xname)) ^^
- { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
-
- val document_files =
- $$$(DOCUMENT_FILES) ~!
- (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
- { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
- rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
-
- command(SESSION) ~!
- (position(session_name) ~
- (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
- (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
- ($$$("=") ~!
- (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
- (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
- (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
- rep1(theories) ~
- (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
- (rep(document_files) ^^ (x => x.flatten))))) ^^
- { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
- Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
- }
-
- def parse_entries(root: Path): List[(String, Session_Entry)] =
- {
- val toks = Token.explode(root_syntax.keywords, File.read(root))
- val start = Token.Pos.file(root.implode)
-
- parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
- case Success(result, _) =>
- var chapter = chapter_default
- val entries = new mutable.ListBuffer[(String, Session_Entry)]
- result.foreach {
- case Chapter(name) => chapter = name
- case session_entry: Session_Entry => entries += ((chapter, session_entry))
- }
- entries.toList
- case bad => error(bad.toString)
- }
- }
- }
-
-
- /* find sessions within certain directories */
-
- private val ROOT = Path.explode("ROOT")
- private val ROOTS = Path.explode("ROOTS")
-
- private def is_session_dir(dir: Path): Boolean =
- (dir + ROOT).is_file || (dir + ROOTS).is_file
-
- private def check_session_dir(dir: Path): Path =
- if (is_session_dir(dir)) dir
- else error("Bad session root directory: " + dir.toString)
-
- def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil)
- : Session_Tree =
- {
- def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
- find_root(select, dir) ::: find_roots(select, dir)
-
- def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
- {
- val root = dir + ROOT
- if (root.is_file)
- Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2))
- else Nil
- }
-
- def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
- {
- val roots = dir + ROOTS
- if (roots.is_file) {
- for {
- line <- split_lines(File.read(roots))
- if !(line == "" || line.startsWith("#"))
- dir1 =
- try { check_session_dir(dir + Path.explode(line)) }
- catch {
- case ERROR(msg) =>
- error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
- }
- info <- find_dir(select, dir1)
- } yield info
- }
- else Nil
- }
-
- val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
- dirs.foreach(check_session_dir(_))
- select_dirs.foreach(check_session_dir(_))
-
- Session_Tree(
- for {
- (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
- info <- find_dir(select, dir)
- } yield info)
- }
-
-
-
- /** build **/
+ /** auxiliary **/
/* queue */
- object Queue
+ private object Queue
{
- def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
+ def apply(tree: Sessions.Tree, load_timings: String => (List[Properties.T], Double)): Queue =
{
val graph = tree.graph
val sessions = graph.keys
@@ -375,8 +67,8 @@
}
}
- final class Queue private(
- graph: Graph[String, Session_Info],
+ private final class Queue private(
+ graph: Graph[String, Sessions.Info],
order: SortedSet[String],
val command_timings: String => List[Properties.T])
{
@@ -389,7 +81,7 @@
order - name, // FIXME scala-2.10.0 TreeSet problem!?
command_timings)
- def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
+ def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
{
val it = order.iterator.dropWhile(name =>
skip(name)
@@ -424,7 +116,7 @@
verbose: Boolean = false,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
- tree: Session_Tree): Deps =
+ tree: Sessions.Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
@@ -517,7 +209,7 @@
dirs: List[Path],
sessions: List[String]): Deps =
{
- val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
+ val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = sessions)
dependencies(inlined_files = inlined_files, tree = tree)
}
@@ -536,12 +228,18 @@
/* jobs */
- private class Job(progress: Progress,
- name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean,
- browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
+ private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
+ store: Sessions.Store, do_output: Boolean, verbose: Boolean,
+ session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
{
+ val output = store.output_dir + Path.basic(name)
def output_path: Option[Path] = if (do_output) Some(output) else None
- def output_standard_path: String = if (do_output) File.standard_path(output) else ""
+ def output_save_state: String =
+ if (do_output)
+ "PolyML.SaveState.saveChild (" + ML_Syntax.print_string0(File.platform_path(output)) +
+ ", List.length (PolyML.SaveState.showHierarchy ()))"
+ else ""
+ output.file.delete
private val parent = info.parent.getOrElse("")
@@ -549,8 +247,6 @@
try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
catch { case ERROR(_) => /*error should be exposed in ML*/ }
- output.file.delete
-
private val env =
Isabelle_System.settings() +
("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
@@ -558,13 +254,13 @@
private val future_result: Future[Process_Result] =
Future.thread("build") {
val process =
- if (is_pure(name)) {
+ if (Sessions.is_pure(name)) {
val eval =
"Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
- " Session.shutdown (); ML_Heap.share_common_data ();" +
- " ML_Heap.save_state " + ML_Syntax.print_string_raw(output_standard_path) + "));"
- ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
- cwd = info.dir.file, env = env)
+ " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
+ ML_Process(info.options,
+ raw_ml_system = true, args = List("--use", "ROOT.ML", "--eval", eval),
+ cwd = info.dir.file, env = env, tree = Some(tree), store = store)
}
else {
val args_file = Isabelle_System.tmp_file("build")
@@ -572,19 +268,22 @@
{
val theories = info.theories.map(x => (x._2, x._3))
import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(string, pair(bool,
+ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string,
list(pair(Options.encode, list(Path.encode)))))))))))))(
- (Symbol.codes, (command_timings, (output_standard_path, (verbose,
- (browser_info, (info.document_files, (File.standard_path(graph_file),
+ (Symbol.codes, (command_timings, (do_output, (verbose,
+ (store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name,
theories)))))))))))
}))
- ML_Process(info.options, parent,
- List("--eval",
- "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file))),
- cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
+ val eval =
+ "Command_Line.tool0 (fn () => (" +
+ "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
+ (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
+ else "") + "));"
+ ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
+ env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
}
process.result(
progress_stdout = (line: String) =>
@@ -615,8 +314,8 @@
{
val result = future_result.join
- if (result.ok && !is_pure(name))
- Present.finish(progress, browser_info, graph_file, info, name)
+ if (result.ok && !Sessions.is_pure(name))
+ Present.finish(progress, store.browser_info, graph_file, info, name)
graph_file.delete
timeout_request.foreach(_.cancel)
@@ -646,13 +345,8 @@
/* log files */
- private val LOG = Path.explode("log")
- private def log(name: String): Path = LOG + Path.basic(name)
- private def log_gz(name: String): Path = log(name).ext("gz")
-
private val SESSION_NAME = "\fSession.name = "
-
sealed case class Log_Info(
name: String,
stats: List[Properties.T],
@@ -679,51 +373,59 @@
/* sources and heaps */
+ private val SOURCES = "sources: "
+ private val INPUT_HEAP = "input_heap: "
+ private val OUTPUT_HEAP = "output_heap: "
+ private val LOG_START = "log:"
+ private val line_prefixes = List(SOURCES, INPUT_HEAP, OUTPUT_HEAP, LOG_START)
+
private def sources_stamp(digests: List[SHA1.Digest]): String =
- digests.map(_.toString).sorted.mkString("sources: ", " ", "")
-
- private val no_heap: String = "heap: -"
+ digests.map(_.toString).sorted.mkString(SOURCES, " ", "")
- private def heap_stamp(heap: Option[Path]): String =
- {
- "heap: " +
- (heap match {
- case Some(path) =>
- val file = path.file
- if (file.isFile) file.length.toString + " " + file.lastModified.toString
- else "-"
- case None => "-"
- })
- }
+ private def read_stamps(path: Path): Option[(String, List[String], List[String])] =
+ if (path.is_file) {
+ val stream = new GZIPInputStream(new BufferedInputStream(new FileInputStream(path.file)))
+ val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
+ val lines =
+ {
+ val lines = new mutable.ListBuffer[String]
+ try {
+ var finished = false
+ while (!finished) {
+ val line = reader.readLine
+ if (line != null && line_prefixes.exists(line.startsWith(_)))
+ lines += line
+ else finished = true
+ }
+ }
+ finally { reader.close }
+ lines.toList
+ }
- private def read_stamps(path: Path): Option[(String, String, String)] =
- if (path.is_file) {
- val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
- val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
- val (s, h1, h2) =
- try { (reader.readLine, reader.readLine, reader.readLine) }
- finally { reader.close }
- if (s != null && s.startsWith("sources: ") &&
- h1 != null && h1.startsWith("heap: ") &&
- h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
+ if (!lines.isEmpty && lines.last.startsWith(LOG_START)) {
+ lines.find(_.startsWith(SOURCES)).map(s =>
+ (s, lines.filter(_.startsWith(INPUT_HEAP)), lines.filter(_.startsWith(OUTPUT_HEAP))))
+ }
else None
}
else None
- /* build_results */
- class Build_Results private [Build](results: Map[String, Option[Process_Result]])
+ /** build with results **/
+
+ class Results private [Build](results: Map[String, Option[Process_Result]])
{
def sessions: Set[String] = results.keySet
def cancelled(name: String): Boolean = results(name).isEmpty
def apply(name: String): Process_Result = results(name).getOrElse(Process_Result(1))
val rc = (0 /: results.iterator.map({ case (_, Some(r)) => r.rc case (_, None) => 1 }))(_ max _)
+ def ok: Boolean = rc == 0
override def toString: String = rc.toString
}
- def build_results(
+ def build(
options: Options,
progress: Progress = Ignore_Progress,
requirements: Boolean = false,
@@ -741,36 +443,21 @@
system_mode: Boolean = false,
verbose: Boolean = false,
exclude_sessions: List[String] = Nil,
- sessions: List[String] = Nil): Build_Results =
+ sessions: List[String] = Nil): Results =
{
/* session tree and dependencies */
- val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
+ val full_tree = Sessions.load(options.int("completion_limit") = 0, dirs, select_dirs)
val (selected, selected_tree) =
full_tree.selection(requirements, all_sessions,
exclude_session_groups, exclude_sessions, session_groups, sessions)
val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
- def make_stamp(name: String): String =
- sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
-
-
- /* persistent information */
+ def session_sources_stamp(name: String): String =
+ sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))
- val (input_dirs, output_dir, browser_info) =
- if (system_mode) {
- val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
- (List(output_dir), output_dir, Path.explode("~~/browser_info"))
- }
- else {
- val output_dir = Path.explode("$ISABELLE_OUTPUT")
- (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
- Path.explode("$ISABELLE_BROWSER_INFO"))
- }
-
- def find_log(name: String): Option[(Path, Path)] =
- input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
+ val store = Sessions.store(system_mode)
/* queue with scheduling information */
@@ -778,11 +465,11 @@
def load_timings(name: String): (List[Properties.T], Double) =
{
val (path, text) =
- find_log(name + ".gz") match {
- case Some((_, path)) => (path, File.read_gzip(path))
+ store.find_log_gz(name) match {
+ case Some(path) => (path, File.read_gzip(path))
case None =>
- find_log(name) match {
- case Some((_, path)) => (path, File.read(path))
+ store.find_log(name) match {
+ case Some(path) => (path, File.read(path))
case None => (Path.current, "")
}
}
@@ -810,21 +497,21 @@
/* main build process */
- // prepare log dir
- Isabelle_System.mkdirs(output_dir + LOG)
+ store.prepare_output()
// optional cleanup
if (clean_build) {
for (name <- full_tree.graph.all_succs(selected)) {
val files =
- List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
+ List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)).
+ map(store.output_dir + _).filter(_.is_file)
if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
}
}
// scheduler loop
- case class Result(current: Boolean, heap: String, process: Option[Process_Result])
+ case class Result(current: Boolean, heap_stamp: Option[String], process: Option[Process_Result])
{
def ok: Boolean =
process match {
@@ -841,7 +528,7 @@
@tailrec def loop(
pending: Queue,
- running: Map[String, (String, Job)],
+ running: Map[String, (List[String], Job)],
results: Map[String, Result]): Map[String, Result] =
{
if (pending.is_empty) results
@@ -850,7 +537,7 @@
for ((_, (_, job)) <- running) job.terminate
running.find({ case (_, (_, job)) => job.is_finished }) match {
- case Some((name, (parent_heap, job))) =>
+ case Some((name, (input_heaps, job))) =>
//{{{ finish job
val process_result = job.join
@@ -863,80 +550,88 @@
val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
val tail = job.info.options.int("process_output_tail")
val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
- process_result.copy(out_lines =
- "(see also " + (output_dir + log(name)).file.toString + ")" :: lines1)
+ process_result.copy(
+ out_lines =
+ "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" ::
+ lines1)
}
- val heap =
+ val heap_stamp =
if (process_result.ok) {
- (output_dir + log(name)).file.delete
+ (store.output_dir + Sessions.log(name)).file.delete
+ val heap_stamp =
+ for (path <- job.output_path; stamp <- File.time_stamp(path))
+ yield stamp
- val sources = make_stamp(name)
- val heap = heap_stamp(job.output_path)
- File.write_gzip(output_dir + log_gz(name),
- Library.terminate_lines(sources :: parent_heap :: heap :: process_result.out_lines))
+ File.write_gzip(store.output_dir + Sessions.log_gz(name),
+ Library.terminate_lines(
+ session_sources_stamp(name) ::
+ input_heaps.map(INPUT_HEAP + _) :::
+ heap_stamp.toList.map(OUTPUT_HEAP + _) :::
+ List(LOG_START) ::: process_result.out_lines))
- heap
+ heap_stamp
}
else {
- (output_dir + Path.basic(name)).file.delete
- (output_dir + log_gz(name)).file.delete
+ (store.output_dir + Path.basic(name)).file.delete
+ (store.output_dir + Sessions.log_gz(name)).file.delete
- File.write(output_dir + log(name), Library.terminate_lines(process_result.out_lines))
+ File.write(store.output_dir + Sessions.log(name),
+ Library.terminate_lines(process_result.out_lines))
progress.echo(name + " FAILED")
if (!process_result.interrupted) progress.echo(process_result_tail.out)
- no_heap
+ None
}
loop(pending - name, running - name,
- results + (name -> Result(false, heap, Some(process_result_tail))))
+ results + (name -> Result(false, heap_stamp, Some(process_result_tail))))
//}}}
case None if running.size < (max_jobs max 1) =>
//{{{ check/start next job
pending.dequeue(running.isDefinedAt(_)) match {
case Some((name, info)) =>
- val parent_result =
- info.parent match {
- case None => Result(true, no_heap, Some(Process_Result(0)))
- case Some(parent) => results(parent)
- }
- val output = output_dir + Path.basic(name)
- val do_output = build_heap || is_pure(name) || queue.is_inner(name)
+ val ancestor_results = selected_tree.ancestors(name).map(results(_))
+ val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
- val (current, heap) =
+ val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
+
+ val (current, heap_stamp) =
{
- find_log(name + ".gz") match {
- case Some((dir, path)) =>
- read_stamps(path) match {
- case Some((s, h1, h2)) =>
- val heap = heap_stamp(Some(dir + Path.basic(name)))
- (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
- !(do_output && heap == no_heap), heap)
- case None => (false, no_heap)
+ store.find(name) match {
+ case Some((log_gz, heap_stamp)) =>
+ read_stamps(log_gz) match {
+ case Some((sources, input_heaps, output_heaps)) =>
+ val current =
+ sources == session_sources_stamp(name) &&
+ input_heaps == ancestor_heaps.map(INPUT_HEAP + _) &&
+ output_heaps == heap_stamp.toList.map(OUTPUT_HEAP + _) &&
+ !(do_output && heap_stamp.isEmpty)
+ (current, heap_stamp)
+ case None => (false, None)
}
- case None => (false, no_heap)
+ case None => (false, None)
}
}
- val all_current = current && parent_result.current
+ val all_current = current && ancestor_results.forall(_.current)
if (all_current)
loop(pending - name, running,
- results + (name -> Result(true, heap, Some(Process_Result(0)))))
+ results + (name -> Result(true, heap_stamp, Some(Process_Result(0)))))
else if (no_build) {
if (verbose) progress.echo("Skipping " + name + " ...")
loop(pending - name, running,
- results + (name -> Result(false, heap, Some(Process_Result(1)))))
+ results + (name -> Result(false, heap_stamp, Some(Process_Result(1)))))
}
- else if (parent_result.ok && !progress.stopped) {
+ else if (ancestor_results.forall(_.ok) && !progress.stopped) {
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
val job =
- new Job(progress, name, info, output, do_output, verbose, browser_info,
+ new Job(progress, name, info, selected_tree, store, do_output, verbose,
deps(name).session_graph, queue.command_timings(name))
- loop(pending, running + (name -> (parent_result.heap, job)), results)
+ loop(pending, running + (name -> (ancestor_heaps, job)), results)
}
else {
progress.echo(name + " CANCELLED")
- loop(pending - name, running, results + (name -> Result(false, heap, None)))
+ loop(pending - name, running, results + (name -> Result(false, heap_stamp, None)))
}
case None => sleep(); loop(pending, running, results)
}
@@ -949,62 +644,15 @@
/* build results */
- val results =
+ val results0 =
if (deps.is_empty) {
progress.echo(Output.warning_text("Nothing to build"))
Map.empty[String, Result]
}
else loop(queue, Map.empty, Map.empty)
-
- /* global browser info */
-
- if (!no_build) {
- val browser_chapters =
- (for {
- (name, result) <- results.iterator
- if result.ok && !is_pure(name)
- info = full_tree(name)
- if info.options.bool("browser_info")
- } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
- map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
-
- for ((chapter, entries) <- browser_chapters)
- Present.update_chapter_index(browser_info, chapter, entries)
-
- if (browser_chapters.nonEmpty) Present.make_global_index(browser_info)
- }
-
- new Build_Results((for ((name, result) <- results.iterator) yield (name, result.process)).toMap)
- }
-
-
- /* build */
-
- def build(
- options: Options,
- progress: Progress = Ignore_Progress,
- requirements: Boolean = false,
- all_sessions: Boolean = false,
- build_heap: Boolean = false,
- clean_build: Boolean = false,
- dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
- exclude_session_groups: List[String] = Nil,
- session_groups: List[String] = Nil,
- max_jobs: Int = 1,
- list_files: Boolean = false,
- check_keywords: Set[String] = Set.empty,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- verbose: Boolean = false,
- exclude_sessions: List[String] = Nil,
- sessions: List[String] = Nil): Int =
- {
val results =
- build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
- dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
- check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
+ new Results((for ((name, result) <- results0.iterator) yield (name, result.process)).toMap)
if (results.rc != 0 && (verbose || !no_build)) {
val unfinished =
@@ -1015,7 +663,26 @@
progress.echo("Unfinished session(s): " + commas(unfinished))
}
- results.rc
+
+ /* global browser info */
+
+ if (!no_build) {
+ val browser_chapters =
+ (for {
+ (name, result) <- results0.iterator
+ if result.ok && !Sessions.is_pure(name)
+ info = full_tree(name)
+ if info.options.bool("browser_info")
+ } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
+ map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
+
+ for ((chapter, entries) <- browser_chapters)
+ Present.update_chapter_index(store.browser_info, chapter, entries)
+
+ if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
+ }
+
+ results
}
@@ -1111,7 +778,7 @@
val start_time = Time.now()
val results =
progress.interrupt_handler {
- build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
+ build(options, progress, requirements, all_sessions, build_heap, clean_build,
dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
}
--- a/src/Pure/Tools/build_doc.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/Tools/build_doc.scala Wed Mar 16 22:42:15 2016 +0100
@@ -24,7 +24,7 @@
{
val selection =
for {
- (name, info) <- Build.find_sessions(options).topological_order
+ (name, info) <- Sessions.load(options).topological_order
if info.groups.contains("doc")
doc = info.options.string("document_variants")
if all_docs || docs.contains(doc)
@@ -40,30 +40,30 @@
progress.echo("Build started for documentation " + commas_quote(selected_docs))
- val rc1 =
+ val res1 =
Build.build(options, progress, requirements = true, build_heap = true,
max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
- if (rc1 == 0) {
+ if (res1.ok) {
Isabelle_System.with_tmp_dir("document_output")(output =>
{
- val rc2 =
+ val res2 =
Build.build(
options.bool.update("browser_info", false).
string.update("document", "pdf").
string.update("document_output", File.standard_path(output)),
progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
sessions = sessions)
- if (rc2 == 0) {
+ if (res2.ok) {
val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
for (doc <- selected_docs) {
val name = doc + ".pdf"
File.copy(new JFile(output, name), new JFile(doc_dir, name))
}
}
- rc2
+ res2.rc
})
}
- else rc1
+ else res1.rc
}
--- a/src/Pure/Tools/ml_console.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/Tools/ml_console.scala Wed Mar 16 22:42:15 2016 +0100
@@ -22,6 +22,7 @@
var modes: List[String] = Nil
var no_build = false
var options = Options.init()
+ var raw_ml_system = false
var system_mode = false
val getopts = Getopts("""
@@ -33,7 +34,7 @@
-m MODE add print mode for output
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r logic session is "RAW_ML_SYSTEM"
+ -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
@@ -45,7 +46,7 @@
"m:" -> (arg => modes = arg :: modes),
"n" -> (arg => no_build = true),
"o:" -> (arg => options = options + arg),
- "r" -> (_ => logic = "RAW_ML_SYSTEM"),
+ "r" -> (_ => raw_ml_system = true),
"s" -> (_ => system_mode = true))
val more_args = getopts(args)
@@ -53,24 +54,25 @@
// build
- if (!no_build && logic != "RAW_ML_SYSTEM" &&
- Build.build(options = options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(logic)) != 0)
+ if (!no_build && !raw_ml_system &&
+ !Build.build(options = options, build_heap = true, no_build = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
{
val progress = new Console_Progress
progress.echo("Build started for Isabelle/" + logic + " ...")
progress.interrupt_handler {
- val rc =
+ val res =
Build.build(options = options, progress = progress, build_heap = true,
dirs = dirs, system_mode = system_mode, sessions = List(logic))
- if (rc != 0) sys.exit(rc)
+ if (!res.ok) sys.exit(res.rc)
}
}
// process loop
val process =
- ML_Process(options, heap = logic, args = List("-i"),
- modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
+ ML_Process(options, logic = logic, args = List("-i"),
+ modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
+ raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
val process_output = Future.thread[Unit]("process_output") {
try {
var result = new StringBuilder(100)
--- a/src/Pure/Tools/ml_process.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/Tools/ml_process.scala Wed Mar 16 22:42:15 2016 +0100
@@ -13,45 +13,32 @@
object ML_Process
{
def apply(options: Options,
- heap: String = "",
+ logic: String = "",
args: List[String] = Nil,
+ dirs: List[Path] = Nil,
modes: List[String] = Nil,
+ raw_ml_system: Boolean = false,
secure: Boolean = false,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
- channel: Option[System_Channel] = None): Bash.Process =
+ channel: Option[System_Channel] = None,
+ tree: Option[Sessions.Tree] = None,
+ store: Sessions.Store = Sessions.store()): Bash.Process =
{
- val load_heaps =
- {
- if (heap == "RAW_ML_SYSTEM") Nil
- else if (heap.iterator.contains('/')) {
- val heap_path = Path.explode(heap)
- if (!heap_path.is_file) error("Bad heap file: " + heap_path)
- List(heap_path)
- }
+ val logic_name = Isabelle_System.default_logic(logic)
+ val heaps: List[String] =
+ if (raw_ml_system) Nil
else {
- val dirs = Isabelle_System.find_logics_dirs()
- val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
- dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
- case Some(heap_path) => List(heap_path)
- case None =>
- error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
- cat_lines(dirs.map(dir => " " + dir.implode)))
- }
+ val (_, session_tree) =
+ tree.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
+ (session_tree.ancestors(logic_name) ::: List(logic_name)).
+ map(a => File.platform_path(store.heap(a)))
}
- }
- val eval_heaps =
- load_heaps.map(load_heap =>
- "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
- "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
- ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
- "); OS.Process.exit OS.Process.failure)")
-
- val eval_initial =
- if (load_heaps.isEmpty) {
+ val eval_init =
+ if (heaps.isEmpty) {
List(
if (Platform.is_windows)
"fun exit 0 = OS.Process.exit OS.Process.success" +
@@ -59,25 +46,31 @@
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
else
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
- "PolyML.Compiler.prompt1 := \"ML> \"",
- "PolyML.Compiler.prompt2 := \"ML# \"")
+ "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
+ "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
}
- else Nil
+ else
+ List(
+ "(PolyML.SaveState.loadHierarchy " +
+ ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
+ "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
+ ML_Syntax.print_string0(": " + logic_name + "\n") +
+ "); OS.Process.exit OS.Process.failure)")
val eval_modes =
if (modes.isEmpty) Nil
- else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
+ else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
// options
val isabelle_process_options = Isabelle_System.tmp_file("options")
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
- val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
+ val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
val eval_process =
- if (load_heaps.isEmpty)
+ if (heaps.isEmpty)
List("PolyML.print_depth 10")
else
channel match {
@@ -85,7 +78,7 @@
List("(default_print_depth 10; Isabelle_Process.init_options ())")
case Some(ch) =>
List("(default_print_depth 10; Isabelle_Process.init_protocol " +
- ML_Syntax.print_string_raw(ch.server_name) + ")")
+ ML_Syntax.print_string0(ch.server_name) + ")")
}
// ISABELLE_TMP
@@ -95,7 +88,7 @@
// bash
val bash_args =
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
- (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
+ (eval_init ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
map(eval => List("--eval", eval)).flatten ::: args
Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
@@ -118,40 +111,36 @@
def main(args: Array[String])
{
Command_Line.tool {
+ var dirs: List[Path] = Nil
var eval_args: List[String] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var modes: List[String] = Nil
var options = Options.init()
val getopts = Getopts("""
-Usage: isabelle process [OPTIONS] [HEAP]
+Usage: isabelle process [OPTIONS]
Options are:
+ -d DIR include session directory
-e ML_EXPR evaluate ML expression on startup
-f ML_FILE evaluate ML file on startup
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- Run the raw Isabelle ML process in batch mode, using a given heap image.
-
- If HEAP is a plain name (default ISABELLE_LOGIC=""" +
- quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in
- ISABELLE_PATH; if it contains a slash, it is taken as literal file;
- if it is "RAW_ML_SYSTEM", the initial ML heap is used.
+ Run the raw Isabelle ML process in batch mode.
""",
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+ "l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"o:" -> (arg => options = options + arg))
- if (args.isEmpty) getopts.usage()
- val heap =
- getopts(args) match {
- case Nil => ""
- case List(heap) => heap
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ if (args.isEmpty || !more_args.isEmpty) getopts.usage()
- ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
+ ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
result().print_stdout.rc
}
}
--- a/src/Pure/build-jars Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Pure/build-jars Wed Mar 16 22:42:15 2016 +0100
@@ -90,6 +90,7 @@
System/utf8.scala
Thy/html.scala
Thy/present.scala
+ Thy/sessions.scala
Thy/thy_header.scala
Thy/thy_info.scala
Thy/thy_syntax.scala
--- a/src/Tools/Code/code_ml.ML Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Tools/Code/code_ml.ML Wed Mar 16 22:42:15 2016 +0100
@@ -871,7 +871,7 @@
check = { env_var = "ISABELLE_TOOL",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
+ "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
#> Code_Target.add_language
(target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
check = { env_var = "ISABELLE_OCAML",
--- a/src/Tools/jEdit/src/isabelle.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Mar 16 22:42:15 2016 +0100
@@ -51,7 +51,7 @@
mode match {
case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
case "isabelle-options" => Some(Options.options_syntax)
- case "isabelle-root" => Some(Build.root_syntax)
+ case "isabelle-root" => Some(Sessions.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
case "isabelle-news" => Some(news_syntax)
case "isabelle-output" => None
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 16 14:05:30 2016 +0000
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 16 22:42:15 2016 +0100
@@ -66,7 +66,7 @@
Build.build(options = PIDE.options.value, progress = progress,
build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
- dirs = session_dirs(), sessions = List(session_name()))
+ dirs = session_dirs(), sessions = List(session_name())).rc
}
def session_start()
@@ -76,14 +76,15 @@
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
PIDE.session.start(receiver =>
Isabelle_Process(
- PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver))
+ PIDE.options.value, logic = session_name(), modes = modes, receiver = receiver,
+ store = Sessions.store(session_build_mode() == "system")))
}
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
def session_list(): List[String] =
{
- val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs())
+ val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
val (main_sessions, other_sessions) =
session_tree.topological_order.partition(p => p._2.groups.contains("main"))
main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted