src/Doc/System/Server.thy
changeset 67938 da44f151f716
parent 67937 91eb307511bb
child 67940 b4e80f062fbf
equal deleted inserted replaced
67937:91eb307511bb 67938:da44f151f716
   927   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   927   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   928   ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
   928   ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
   929   specifications may be given, which is occasionally useful for precise error
   929   specifications may be given, which is occasionally useful for precise error
   930   locations.
   930   locations.
   931 
   931 
   932   \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
   932   \<^medskip> The \<open>master_dir\<close> field specifies the master directory of imported
   933   the imported theory. Normally this is determined implicitly from the parent
   933   theories: it acts like the ``current working directory'' for locating theory
   934   directory of the theory file.
   934   files. This may be omitted if all entries of \<open>theories\<close> use a
       
   935   session-qualified theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute
       
   936   path name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
   935 
   937 
   936   \<^medskip>
   938   \<^medskip>
   937   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   939   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
   938   default is suitable for classic console output. Formatting happens at the
   940   default is suitable for classic console output. Formatting happens at the
   939   end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
   941   end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.