src/Doc/System/Server.thy
changeset 67940 b4e80f062fbf
parent 67938 da44f151f716
child 67941 49a34b2fa788
     1.1 --- a/src/Doc/System/Server.thy	Fri Mar 23 22:44:43 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Fri Mar 23 22:53:32 2018 +0100
     1.3 @@ -877,13 +877,9 @@
     1.4    \end{tabular}
     1.5  
     1.6    \begin{tabular}{ll}
     1.7 -  \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
     1.8 -  \end{tabular}
     1.9 -
    1.10 -  \begin{tabular}{ll}
    1.11    \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
    1.12    \quad\<open>{session_id: uuid,\<close> \\
    1.13 -  \quad~~\<open>theories: [theory_name],\<close> \\
    1.14 +  \quad~~\<open>theories: [string],\<close> \\
    1.15    \quad~~\<open>master_dir?: string,\<close> \\
    1.16    \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
    1.17    \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
    1.18 @@ -925,9 +921,7 @@
    1.19  
    1.20    \<^medskip>
    1.21    The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
    1.22 -  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
    1.23 -  specifications may be given, which is occasionally useful for precise error
    1.24 -  locations.
    1.25 +  ROOT \<^bold>\<open>theories\<close>.
    1.26  
    1.27    \<^medskip> The \<open>master_dir\<close> field specifies the master directory of imported
    1.28    theories: it acts like the ``current working directory'' for locating theory