set show_markup to false in order to avoid problems in jedit
authorsmolkas
Fri, 11 Jan 2013 13:57:51 +0100
changeset 50823 0583db803066
parent 50822 5adc528be033
child 50824 a991d603aac6
set show_markup to false in order to avoid problems in jedit
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"))