equal
deleted
inserted
replaced
61 imports "$mirabelle_thy" "$mirabelle_theory" |
61 imports "$mirabelle_thy" "$mirabelle_theory" |
62 $tools |
62 $tools |
63 begin |
63 begin |
64 |
64 |
65 setup {* |
65 setup {* |
66 Config.put_thy Mirabelle.logfile "$log_file" #> |
66 Config.put_global Mirabelle.logfile "$log_file" #> |
67 Config.put_thy Mirabelle.timeout $timeout #> |
67 Config.put_global Mirabelle.timeout $timeout #> |
68 Config.put_thy Mirabelle.start_line $start_line #> |
68 Config.put_global Mirabelle.start_line $start_line #> |
69 Config.put_thy Mirabelle.end_line $end_line |
69 Config.put_global Mirabelle.end_line $end_line |
70 *} |
70 *} |
71 |
71 |
72 END |
72 END |
73 |
73 |
74 foreach (split(/:/, $actions)) { |
74 foreach (split(/:/, $actions)) { |