equal
deleted
inserted
replaced
1616 - Naming of auxiliary rules necessary? |
1616 - Naming of auxiliary rules necessary? |
1617 *) |
1617 *) |
1618 |
1618 |
1619 (* values_timeout configuration *) |
1619 (* values_timeout configuration *) |
1620 |
1620 |
1621 val default_values_timeout = if ML_System.is_smlnj then 600.0 else 20.0 |
1621 val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0 |
1622 |
1622 |
1623 val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout) |
1623 val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout) |
1624 |
1624 |
1625 val setup = PredData.put (Graph.empty) #> |
1625 val setup = PredData.put (Graph.empty) #> |
1626 Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro) |
1626 Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro) |