author wenzelm Wed, 11 Jun 2014 22:28:24 +0200 changeset 57323 3c66ca9b425b parent 57322 88d7e3eca84b child 57324 8c0322732f3e
more on "Auxiliary files";
 src/Doc/JEdit/JEdit.thy file | annotate | diff | comparison | revisions
--- a/src/Doc/JEdit/JEdit.thy	Wed Jun 11 14:01:04 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 11 22:28:24 2014 +0200
@@ -739,7 +739,52 @@
subsection {* Auxiliary files \label{sec:aux-files} *}

text {*
-  FIXME
+  Special load commands like @{command ML_file} and @{command SML_file}
+  \cite{isabelle-isar-ref} refer to auxiliary files within some theory.
+  Conceptually, the file argument of the command extends the theory source by
+  the content of the file, but its editor buffer may be loaded~/ changed~/
+  saved separately. The PIDE document model propagates changes of auxiliary
+  file content to the corresponding load command in the theory, to update and
+  process it accordingly: changes of auxiliary file content are treated as
+  changes of the corresponding load command.
+
+  \medskip As a concession to the massive amount of ML files in Isabelle/HOL
+  itself, the content of auxiliary files is only added to the PIDE
+  document-model on demand, the first time when opened explicitly in the
+  editor. There are further special tricks to manage markup of ML files, such
+  that Isabelle/HOL may be edited conveniently in the Prover IDE on small
+  machines with only 4--8\,GB of main memory. Using @{verbatim Pure} as logic
+  session image, the exploration may start at the top @{file
+  "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file + "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
+
+  Initially, before an auxiliary file is opened in the editor, the prover
+  reads its content from the physical file-system. After the file is opened
+  for the first time in the editor, e.g.\ by following the hyperlink
+  (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command
+  ML_file} command, the content is taken from the jEdit buffer.
+
+  The change of responsibility from prover to editor counts as an update of
+  the document content, so subsequent theory sources need to be re-checked.
+  When the buffer is closed, the responsibility remains to the editor, though:
+  the file may be opened again without causing another document update.
+
+  A file that is opened in the editor, but its theory with the load command is
+  not, is presently inactive in the document model. A file that is loaded via
+  multiple load commands is associated to an arbitrary one: this situation is
+  morally unsupported and might lead to confusion.
+
+  \medskip Output that refers to an auxiliary file is combined with that of
+  the corresponding load command, and shown whenever the file or the command