avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
authorblanchet
Mon Nov 12 12:06:56 2012 +0100 (2012-11-12 ago)
changeset 50049dd6a4655cd72
parent 50048 fb024bbf4b65
child 50051 87be91e6d486
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:52:37 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 12:06:56 2012 +0100
     1.3 @@ -232,7 +232,7 @@
     1.4    end
     1.5  
     1.6  fun hackish_string_for_term ctxt =
     1.7 -  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> repair_printed_term
     1.8 +  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
     1.9  
    1.10  (* This is a terrible hack. Free variables are sometimes coded as "M__" when
    1.11     they are displayed as "M" and we want to avoid clashes with these. But
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 11:52:37 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 12:06:56 2012 +0100
     2.3 @@ -628,7 +628,7 @@
     2.4      fun do_indent ind = replicate_string (ind * indent_size) " "
     2.5      fun do_free (s, T) =
     2.6        maybe_quote s ^ " :: " ^
     2.7 -      maybe_quote (repair_printed_term (with_vanilla_print_mode
     2.8 +      maybe_quote (simplify_spaces (with_vanilla_print_mode
     2.9          (Syntax.string_of_typ ctxt) T))
    2.10      fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
    2.11      fun do_have qs =
    2.12 @@ -641,7 +641,7 @@
    2.13      val do_term =
    2.14        annotate_types ctxt
    2.15        #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
    2.16 -      #> repair_printed_term
    2.17 +      #> simplify_spaces
    2.18        #> maybe_quote
    2.19      val reconstr = Metis (type_enc, lam_trans)
    2.20      fun do_facts ind (ls, ss) =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 11:52:37 2012 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 12:06:56 2012 +0100
     3.3 @@ -19,7 +19,6 @@
     3.4    val reserved_isar_keyword_table : unit -> unit Symtab.table
     3.5    val thms_in_proof : unit Symtab.table option -> thm -> string list
     3.6    val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
     3.7 -  val repair_printed_term : string -> string
     3.8  end;
     3.9  
    3.10  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    3.11 @@ -107,8 +106,4 @@
    3.12    Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    3.13                             (print_mode_value ())) f x
    3.14  
    3.15 -val repair_printed_term =
    3.16 -  String.translate (fn c => if Char.isPrint c then str c else "")
    3.17 -  #> simplify_spaces
    3.18 -
    3.19  end;