equal
deleted
inserted
replaced
7 (*configuration*) |
7 (*configuration*) |
8 val logfile : string Config.T |
8 val logfile : string Config.T |
9 val timeout : int Config.T |
9 val timeout : int Config.T |
10 val start_line : int Config.T |
10 val start_line : int Config.T |
11 val end_line : int Config.T |
11 val end_line : int Config.T |
12 val setup : theory -> theory |
|
13 |
12 |
14 (*core*) |
13 (*core*) |
15 type init_action = int -> theory -> theory |
14 type init_action = int -> theory -> theory |
16 type done_args = {last: Toplevel.state, log: string -> unit} |
15 type done_args = {last: Toplevel.state, log: string -> unit} |
17 type done_action = int -> done_args -> unit |
16 type done_action = int -> done_args -> unit |
41 structure Mirabelle : MIRABELLE = |
40 structure Mirabelle : MIRABELLE = |
42 struct |
41 struct |
43 |
42 |
44 (* Mirabelle configuration *) |
43 (* Mirabelle configuration *) |
45 |
44 |
46 val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" (K "") |
45 val logfile = Attrib.setup_config_string @{binding mirabelle_logfile} (K "") |
47 val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" (K 30) |
46 val timeout = Attrib.setup_config_int @{binding mirabelle_timeout} (K 30) |
48 val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" (K 0) |
47 val start_line = Attrib.setup_config_int @{binding mirabelle_start_line} (K 0) |
49 val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" (K ~1) |
48 val end_line = Attrib.setup_config_int @{binding mirabelle_end_line} (K ~1) |
50 |
|
51 val setup = setup1 #> setup2 #> setup3 #> setup4 |
|
52 |
49 |
53 |
50 |
54 (* Mirabelle core *) |
51 (* Mirabelle core *) |
55 |
52 |
56 type init_action = int -> theory -> theory |
53 type init_action = int -> theory -> theory |