Proper component setup.

NOTES.thy

@@ -0,0 +1,87 @@
+chapter \<open>Notes on Isabelle/DOF for Isabelle2021-1\<close>
+
+theory NOTES
+  imports Main
+begin
+
+section \<open>Isabelle/DOF component setup\<close>
+
+subsection \<open>Terminology\<close>
+
+text \<open>
+  \<^item> The concept of \<^emph>\<open>Isabelle system component\<close> is explained in \<^doc>\<open>system\<close>
+  section 1.1.1; see also \<^tool>\<open>components\<close> explained in section 7.3.
+
+    For example:
+
+      \<^verbatim>\<open>isabelle components -l\<close>
+
+  \<^item> In the private terminology of Burkhart, the word "component" has a
+  different meaning: a tool implemented in Isabelle/ML that happens to
+  declare context data (many ML tools do that, it is not very special,
+  similar to defining a \<^verbatim>\<open>datatype\<close> or \<^verbatim>\<open>structure\<close> in ML).
+\<close>
+
+
+subsection \<open>Isabelle/DOF as component\<close>
+
+text \<open>
+  Formal Isabelle/DOF component setup happens here:
+
+  \<^item> \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>
+
+    \<^item> A suitable directory entry in the file registers our component to
+    existing Isabelle installation; it also activates the session
+    directory tree starting at \<^file>\<open>$ISABELLE_DOF_HOME/ROOTS\<close>.
+
+    \<^item> Alternative: use \<^path>\<open>$ISABELLE_HOME/Admin/build_release\<close> with
+    option \<^verbatim>\<open>-c\<close> to produce a derived Isabelle distribution that bundles
+    our component for end-users (maybe even with AFP entries).
+
+  \<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/settings\<close>
+
+    \<^item> This provides a pervasive Bash process environment (variables,
+    shell functions etc.). It may refer to \<^verbatim>\<open>$COMPONENT\<close> for the
+    component root, e.g. to retain it in variable \<^dir>\<open>$ISABELLE_DOF_HOME\<close>.
+
+    \<^item> Historically, it used to be the main configuration area, but today
+    we see more and more alternatives, e.g. system options or services in
+    Isabelle/Scala (see below).
+
+  \<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/options\<close>
+
+    \<^item> options declared as \<^verbatim>\<open>public\<close> appear in the Isabelle/jEdit dialog
+    \<^action>\<open>plugin-options\<close> (according to their \<^verbatim>\<open>section\<close>)
+
+    \<^item> all options (public and non-public) are available for command-line
+    usage, e.g. \<^verbatim>\<open>isabelle build -o dof_url="..."\<close>
+
+    \<^item> access to options in Isabelle/ML:
+
+      \<^item> implicit (for the running ML session)
+        \<^ML>\<open>Options.default_string \<^system_option>\<open>dof_url\<close>\<close>
+
+      \<^item> explicit (e.g. for each theories section in
+      \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/build.ML\<close>):
+        \<^ML>\<open>fn options => Options.string options \<^system_option>\<open>dof_url\<close>\<close>
+
+    \<^item> access in Isabelle/Scala is always explicit; the initial options
+      should be created only once and passed around as explicit argument:
+
+      \<^scala>\<open>{
+        val options = isabelle.Options.init();
+        options.string("dof_url");
+      }\<close>
+
+      Note: there are no antiquotations in Isabelle/Scala, so the literal
+      string \<^scala>\<open>"dof_url"\<close> is unchecked.
+\<close>
+
+
+section \<open>Isabelle/ML\<close>
+
+section \<open>Isabelle/Scala\<close>
+
+end
+
+(* :maxLineLen=75: *)

etc/options

@@ -0,0 +1,12 @@
+(* :mode=isabelle-options: *)
+
+section "Isabelle/DOF"
+
+public option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+  -- "Isabelle/DOF source repository"
+
+option dof_artifact_dir : string = "releases/Isabelle_DOF/Isabelle_DOF"
+  -- "Isabelle/DOF release artifacts"
+
+option dof_artifact_host : string = "artifacts.logicalhacking.com"
+

etc/settings

@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_DOF_HOME="$COMPONENT"