44 Isabelle_System.mkdir (Path.explode prefix) |
44 Isabelle_System.mkdir (Path.explode prefix) |
45 else |
45 else |
46 () |
46 () |
47 *} |
47 *} |
48 |
48 |
49 ML {* Options.put_default @{system_option MaSh} "nb" *} |
|
50 |
|
51 ML {* |
49 ML {* |
52 if do_it then |
50 if do_it then |
53 generate_mash_suggestions @{context} params (range, step) thys max_suggestions |
51 generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions |
54 (prefix ^ "mash_nb_suggestions") |
52 (prefix ^ "mash_nb_suggestions") |
55 else |
53 else |
56 () |
54 () |
57 *} |
55 *} |
58 |
56 |
59 ML {* Options.put_default @{system_option MaSh} "knn" *} |
|
60 |
|
61 ML {* |
57 ML {* |
62 if do_it then |
58 if do_it then |
63 generate_mash_suggestions @{context} params (range, step) thys max_suggestions |
59 generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions |
64 (prefix ^ "mash_knn_suggestions") |
60 (prefix ^ "mash_knn_suggestions") |
65 else |
61 else |
66 () |
62 () |
67 *} |
63 *} |
68 |
64 |
69 ML {* Options.put_default @{system_option MaSh} "py" *} |
65 ML {* |
|
66 if do_it then |
|
67 generate_mepo_suggestions @{context} params (range, step) thys max_suggestions |
|
68 (prefix ^ "mepo_suggestions") |
|
69 else |
|
70 () |
|
71 *} |
70 |
72 |
71 ML {* |
73 ML {* |
72 if do_it then |
74 if do_it then |
73 generate_mash_suggestions @{context} params (range, step) thys max_suggestions |
75 generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions") |
74 (prefix ^ "mash_py_suggestions") |
76 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions") |
|
77 else |
|
78 () |
|
79 *} |
|
80 |
|
81 ML {* |
|
82 if do_it then |
|
83 generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions") |
|
84 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions") |
|
85 else |
|
86 () |
|
87 *} |
|
88 |
|
89 ML {* |
|
90 if do_it then |
|
91 generate_prover_dependencies @{context} params range thys |
|
92 (prefix ^ "mash_nb_prover_dependencies") |
|
93 else |
|
94 () |
|
95 *} |
|
96 |
|
97 ML {* |
|
98 if do_it then |
|
99 generate_prover_dependencies @{context} params range thys |
|
100 (prefix ^ "mash_knn_prover_dependencies") |
|
101 else |
|
102 () |
|
103 *} |
|
104 |
|
105 ML {* |
|
106 if do_it then |
|
107 generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions") |
|
108 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions") |
|
109 else |
|
110 () |
|
111 *} |
|
112 |
|
113 ML {* |
|
114 if do_it then |
|
115 generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions") |
|
116 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions") |
75 else |
117 else |
76 () |
118 () |
77 *} |
119 *} |
78 |
120 |
79 ML {* |
121 ML {* |
105 () |
147 () |
106 *} |
148 *} |
107 |
149 |
108 ML {* |
150 ML {* |
109 if do_it then |
151 if do_it then |
110 generate_mepo_suggestions @{context} params (range, step) thys max_suggestions |
|
111 (prefix ^ "mepo_suggestions") |
|
112 else |
|
113 () |
|
114 *} |
|
115 |
|
116 ML {* |
|
117 if do_it then |
|
118 generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions") |
|
119 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions") |
|
120 else |
|
121 () |
|
122 *} |
|
123 |
|
124 ML {* |
|
125 if do_it then |
|
126 generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies") |
|
127 else |
|
128 () |
|
129 *} |
|
130 |
|
131 ML {* |
|
132 if do_it then |
|
133 generate_prover_commands @{context} params (range, step) thys max_suggestions |
152 generate_prover_commands @{context} params (range, step) thys max_suggestions |
134 (prefix ^ "mash_prover_commands") |
153 (prefix ^ "mash_prover_commands") |
135 else |
154 else |
136 () |
155 () |
137 *} |
156 *} |
138 |
157 |
139 ML {* |
|
140 if do_it then |
|
141 generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions") |
|
142 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions") |
|
143 else |
|
144 () |
|
145 *} |
|
146 |
|
147 end |
158 end |