make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
authorsmolkas
Tue Jun 11 16:13:19 2013 -0400 (2013-06-11 ago)
changeset 52366ff89424b5094
parent 52365 95186e6e4bf4
child 52367 2f5e6ad6e91f
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 21:07:53 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jun 11 16:13:19 2013 -0400
     1.3 @@ -34,19 +34,6 @@
     1.4  fun post_fold_term_type f s t =
     1.5    post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
     1.6  
     1.7 -local
     1.8 -fun natify_numeral' (t as Const (s, T)) =
     1.9 -    (case s of
    1.10 -      "Groups.zero_class.zero" => Const (s, @{typ "nat"})
    1.11 -    | "Groups.one_class.one" => Const (s, @{typ "nat"})
    1.12 -    | "Num.numeral_class.numeral" => Const(s, @{typ "num"} --> @{typ "nat"})
    1.13 -    | "Num.numeral_class.neg_numeral" => Const(s, @{typ "num"} --> @{typ "nat"})
    1.14 -    | _ => t)
    1.15 -  | natify_numeral' t = t
    1.16 -in
    1.17 -val natify_numerals = Term.map_aterms natify_numeral'
    1.18 -end
    1.19 -
    1.20  (* Data structures, orders *)
    1.21  val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
    1.22  structure Var_Set_Tab = Table(
    1.23 @@ -157,9 +144,7 @@
    1.24          else (Type.constraint T t, (cp + 1, annots'))
    1.25        | post2 t _ x = (t, x)
    1.26    in
    1.27 -    t |> natify_numerals (* typing all numerals as "nat"s prevents the pretty
    1.28 -         printer from inserting additional, unwanted type annotations *)
    1.29 -      |> post_traverse_term_type post2 (0, rev annots)
    1.30 +    t |> post_traverse_term_type post2 (0, rev annots)
    1.31        |> fst
    1.32    end
    1.33  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 11 21:07:53 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 11 16:13:19 2013 -0400
     2.3 @@ -369,8 +369,6 @@
     2.4  
     2.5  fun hammer_away override_params subcommand opt_i fact_override state =
     2.6    let
     2.7 -    (* necessary to avoid problems in jedit *)
     2.8 -    val state = state |> Proof.map_context (Config.put show_markup false)
     2.9      val ctxt = Proof.context_of state
    2.10      val override_params = override_params |> map (normalize_raw_param ctxt)
    2.11      val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 21:07:53 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jun 11 16:13:19 2013 -0400
     3.3 @@ -433,6 +433,14 @@
     3.4  
     3.5  fun string_of_proof ctxt type_enc lam_trans i n proof =
     3.6    let
     3.7 +    val ctxt =
     3.8 +      (* make sure type constraint are actually printed *)
     3.9 +      ctxt |> Config.put show_markup false
    3.10 +      (* make sure only type constraints inserted by sh_annotate are printed *)
    3.11 +           |> Config.put Printer.show_type_emphasis false
    3.12 +           |> Config.put show_types false
    3.13 +           |> Config.put show_sorts false
    3.14 +           |> Config.put show_consts false
    3.15      val register_fixes = map Free #> fold Variable.auto_fixes
    3.16      fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
    3.17      fun of_indent ind = replicate_string (ind * indent_size) " "