116 } |
116 } |
117 \isamarkuptrue% |
117 \isamarkuptrue% |
118 % |
118 % |
119 \begin{isamarkuptext}% |
119 \begin{isamarkuptext}% |
120 \begin{mldecls} |
120 \begin{mldecls} |
121 \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\ |
121 \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\ |
122 \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\ |
122 \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\ |
123 \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\ |
123 \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Unsynchronized.ref| & default \verb|false| \\ |
124 \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\ |
124 \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\ |
125 \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\ |
125 \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\ |
126 \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\ |
126 \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\ |
127 \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\ |
127 \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\ |
128 \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\ |
128 \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Unsynchronized.ref| & default \verb|true| \\ |
129 \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\ |
129 \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int Unsynchronized.ref| & default \verb|10| \\ |
130 \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\ |
130 \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\ |
131 \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\ |
131 \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\ |
132 \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\ |
132 \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\ |
133 \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\ |
133 \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\ |
134 \end{mldecls} |
134 \end{mldecls} |
135 |
135 |
136 These global ML variables control the detail of information that is |
136 These global ML variables control the detail of information that is |
137 displayed for types, terms, theorems, goals etc. |
137 displayed for types, terms, theorems, goals etc. |
138 |
138 |