1008 @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\ |
1008 @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\ |
1009 @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\ |
1009 @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\ |
1010 @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
1010 @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
1011 @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\ |
1011 @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\ |
1012 \end{matharray} |
1012 \end{matharray} |
|
1013 \begin{tabular}{rcll} |
|
1014 @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ |
|
1015 @{attribute_def ML_source_trace} & : & @{text attribute} & default @{text false} \\ |
|
1016 @{attribute_def ML_exception_trace} & : & @{text attribute} & default @{text false} \\ |
|
1017 \end{tabular} |
1013 |
1018 |
1014 @{rail \<open> |
1019 @{rail \<open> |
1015 (@@{command SML_file} | @@{command ML_file}) @{syntax name} |
1020 (@@{command SML_file} | @@{command ML_file}) @{syntax name} |
1016 ; |
1021 ; |
1017 (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | |
1022 (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | |
1088 Attrib.thms >> (fn ths => |
1093 Attrib.thms >> (fn ths => |
1089 Thm.declaration_attribute |
1094 Thm.declaration_attribute |
1090 (fn th: thm => fn context: Context.generic => |
1095 (fn th: thm => fn context: Context.generic => |
1091 let val context' = context |
1096 let val context' = context |
1092 in context' end)) *} |
1097 in context' end)) *} |
|
1098 |
|
1099 text {* |
|
1100 \begin{description} |
|
1101 |
|
1102 \item @{attribute ML_print_depth} controls the printing depth of the ML |
|
1103 toplevel pretty printer; the precise effect depends on the ML compiler and |
|
1104 run-time system. Typically the limit should be less than 10. Bigger values |
|
1105 such as 100--1000 are occasionally useful for debugging. |
|
1106 |
|
1107 \item @{attribute ML_source_trace} indicates whether the source text that |
|
1108 is given to the ML compiler should be output: it shows the raw Standard ML |
|
1109 after expansion of Isabelle/ML antiquotations. |
|
1110 |
|
1111 \item @{attribute ML_exception_trace} indicates whether the ML run-time |
|
1112 system should print a detailed stack trace on exceptions. The result is |
|
1113 dependent on the particular ML compiler version. Note that after Poly/ML |
|
1114 5.3 some optimizations in the run-time systems may hinder exception |
|
1115 traces. |
|
1116 |
|
1117 The boundary for the exception trace is the current Isar command |
|
1118 transactions. It is occasionally better to insert the combinator @{ML |
|
1119 Runtime.exn_trace} into ML code for debugging |
|
1120 \cite{isabelle-implementation}, closer to the point where it actually |
|
1121 happens. |
|
1122 |
|
1123 \end{description} |
|
1124 *} |
1093 |
1125 |
1094 |
1126 |
1095 section {* Primitive specification elements *} |
1127 section {* Primitive specification elements *} |
1096 |
1128 |
1097 subsection {* Sorts *} |
1129 subsection {* Sorts *} |