# HG changeset patch # User smolkas # Date 1357909071 -3600 # Node ID 0583db8030663990c8aaa7ea45a0a4996661530e # Parent 5adc528be033efb93b389e8b6ed386597ba79a6e set show_markup to false in order to avoid problems in jedit diff -r 5adc528be033 -r 0583db803066 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 11 13:24:49 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 11 13:57:51 2013 +0100 @@ -373,6 +373,8 @@ fun hammer_away override_params subcommand opt_i fact_override state = let + (* this is necessary to avoid errors in jedit *) + val state = state |> Proof.map_context (Config.put show_markup false) val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))