equal
deleted
inserted
replaced
371 |
371 |
372 val default_learn_prover_timeout = 2.0 |
372 val default_learn_prover_timeout = 2.0 |
373 |
373 |
374 fun hammer_away override_params subcommand opt_i fact_override state = |
374 fun hammer_away override_params subcommand opt_i fact_override state = |
375 let |
375 let |
|
376 (* this is necessary to avoid errors in jedit *) |
|
377 val state = state |> Proof.map_context (Config.put show_markup false) |
376 val ctxt = Proof.context_of state |
378 val ctxt = Proof.context_of state |
377 val override_params = override_params |> map (normalize_raw_param ctxt) |
379 val override_params = override_params |> map (normalize_raw_param ctxt) |
378 val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP")) |
380 val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP")) |
379 in |
381 in |
380 if subcommand = runN then |
382 if subcommand = runN then |