33 |
33 |
34 |
34 |
35 section \<open>Isabelle settings \label{sec:settings}\<close> |
35 section \<open>Isabelle settings \label{sec:settings}\<close> |
36 |
36 |
37 text \<open> |
37 text \<open> |
38 The Isabelle system heavily depends on the \<^emph>\<open>settings |
38 The Isabelle system heavily depends on the \<^emph>\<open>settings mechanism\<close>. |
39 mechanism\<close>\indexbold{settings}. Essentially, this is a statically scoped |
39 Essentially, this is a statically scoped collection of environment |
40 collection of environment variables, such as @{setting ISABELLE_HOME}, |
40 variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting |
41 @{setting ML_SYSTEM}, @{setting ML_HOME}. These variables are \<^emph>\<open>not\<close> |
41 ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the |
42 intended to be set directly from the shell, though. Isabelle employs a |
42 shell, though. Isabelle employs a somewhat more sophisticated scheme of |
43 somewhat more sophisticated scheme of \<^emph>\<open>settings files\<close> --- one for |
43 \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for additional |
44 site-wide defaults, another for additional user-specific modifications. With |
44 user-specific modifications. With all configuration variables in clearly |
45 all configuration variables in clearly defined places, this scheme is more |
45 defined places, this scheme is more maintainable and user-friendly than |
46 maintainable and user-friendly than global shell environment variables. |
46 global shell environment variables. |
47 |
47 |
48 In particular, we avoid the typical situation where prospective users of a |
48 In particular, we avoid the typical situation where prospective users of a |
49 software package are told to put several things into their shell startup |
49 software package are told to put several things into their shell startup |
50 scripts, before being able to actually run the program. Isabelle requires |
50 scripts, before being able to actually run the program. Isabelle requires |
51 none such administrative chores of its end-users --- the executables can be |
51 none such administrative chores of its end-users --- the executables can be |
207 \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files |
207 \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files |
208 should be stored by default. The ML system and Isabelle version identifier |
208 should be stored by default. The ML system and Isabelle version identifier |
209 is appended here, too. |
209 is appended here, too. |
210 |
210 |
211 \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory |
211 \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory |
212 browser information (HTML text, graph data, and printable documents) is |
212 browser information is stored as HTML and PDF (see also \secref{sec:info}). |
213 stored (see also \secref{sec:info}). The default value is @{file_unchecked |
213 The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}. |
214 "$ISABELLE_HOME_USER/browser_info"}. |
|
215 |
214 |
216 \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
215 \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
217 is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
216 is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
218 |
217 |
219 \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the |
218 \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the |