# HG changeset patch
# User wenzelm
# Date 1184951351 -7200
# Node ID e8a3b98995fede29e6bbc9f5fa80698015872277
# Parent  f40fba467384a3ffbf741fd4ffa43bf3b76c4931
added ISABELLE_FILE_IDENT;

diff -r f40fba467384 -r e8a3b98995fe doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Fri Jul 20 17:54:17 2007 +0200
+++ b/doc-src/System/basics.tex	Fri Jul 20 19:09:11 2007 +0200
@@ -175,6 +175,12 @@
   \S\ref{sec:tool-usedir}). This typically contains compilation options for
   object-logics --- \texttt{usedir} is the basic utility for managing logic
   sessions (cf.\ the \texttt{IsaMakefile}s in the distribution).
+
+\item[\settdx{ISABELLE_FILE_IDENT}] specifies a shell command for
+  producing a source file identification, based on the actual content
+  instead of the full physical path and date stamp (which is the
+  default). A typical identification would produce a ``digest'' of the
+  text, using a cryptographic hash function like SHA-1, for example.
   
 \item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX},
   \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related