tuned;
authorwenzelm
Sat Mar 24 20:47:54 2018 +0100 (14 months ago)
changeset 67944cb2b1a75ff59
parent 67943 b45f0c0ea14f
child 67945 984c3dc46cc0
tuned;
src/Doc/System/Server.thy
     1.1 --- a/src/Doc/System/Server.thy	Sat Mar 24 20:45:30 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Sat Mar 24 20:47:54 2018 +0100
     1.3 @@ -890,17 +890,11 @@
     1.4    \quad~~\<open>master_dir?: string,\<close> \\
     1.5    \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
     1.6    \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
     1.7 -  \end{tabular}
     1.8 -
     1.9 -  \begin{tabular}{ll}
    1.10 -  \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
    1.11 -  \quad\<open>{status: node_status,\<close> \\
    1.12 -  \quad~~\<open>messages: [message]}\<close> \\[2ex]
    1.13  
    1.14    \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
    1.15    \quad\<open>{ok: bool,\<close> \\
    1.16    \quad~~\<open>errors: [message],\<close> \\
    1.17 -  \quad~~\<open>nodes: [node \<oplus> node_result]}\<close> \\[2ex]
    1.18 +  \quad~~\<open>nodes: [node \<oplus> {status: node_status, messages: [message]}]}\<close> \\
    1.19    \end{tabular}
    1.20  
    1.21    \<^medskip>