src/Doc/System/Server.thy
changeset 68947 ea804c814693
parent 68908 abc338d25640
child 68957 eef4e983fd9d
equal deleted inserted replaced
68946:6dd1460f6920 68947:ea804c814693
   907   \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   907   \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   908   \quad~~\<open>unicode_symbols?: bool,\<close> \\
   908   \quad~~\<open>unicode_symbols?: bool,\<close> \\
   909   \quad~~\<open>export_pattern?: string,\<close> \\
   909   \quad~~\<open>export_pattern?: string,\<close> \\
   910   \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
   910   \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
   911   \quad~~\<open>check_limit?: int,\<close> \\
   911   \quad~~\<open>check_limit?: int,\<close> \\
   912   \quad~~\<open>watchdog_timeout?: double,\<close> \\
   912   \quad~~\<open>watchdog_timeout?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>600.0\<close> \\
   913   \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
   913   \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
   914   \end{tabular}
   914   \end{tabular}
   915 
   915 
   916   \begin{tabular}{ll}
   916   \begin{tabular}{ll}
   917   \<^bold>\<open>type\<close> \<open>export =\<close> \\
   917   \<^bold>\<open>type\<close> \<open>export =\<close> \\